#[recursion]Expand description
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.