Attribute Macro kani::contracts::proof_for_contract
#[proof_for_contract]
Expand description
Designates this function as a harness to check a function contract.
The argument to this macro is the relative path (e.g. foo
or
super::some_mod::foo
or crate::SomeStruct::foo
) to the function, the
contract of which should be checked.
This is part of the function contract API, for more general information see the module-level documentation.