Attribute Macro kani::ensures

#[ensures]
Expand description

Add a postcondition 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 and its return value, accessible as a variable called result. 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 requires) to have at least one designated proof_for_contract harness for checking the contract.