Attribute Macro kani::proof_for_contract

#[proof_for_contract]

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.