Attribute Macro kani::requires

Expand description

Add a precondition to this function.

This is part of the function contract API, for more general information see the module-level documentation.

The contents of the attribute is a condition over the input values to the annotated function. All Rust syntax is supported, even calling other functions, but the computations must be side effect free, e.g. it cannot perform I/O or use mutable memory.

Kani requires each function that uses a contract (this attribute or ensures) to have at least one designated proof_for_contract harness for checking the contract.