Attribute Macro creusot_contracts::macros::terminates

#[terminates]
Expand description

Indicate that the function terminates: fulfilling the requires clauses ensures that this function will not loop forever.