#[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.