Attribute Macro recursion

#[recursion]

Specifies that a function contains recursion for contract instrumentation.**

This attribute is only used for function-contract instrumentation. Kani uses this annotation to identify recursive functions and properly instantiate kani::any_modifies to check such functions using induction.