Attribute Macro modifies

#[modifies]

Declaration of an explicit write-set for the annotated 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 series of comma-separated expressions referencing the arguments of the function. Each expression is expected to return a pointer type, i.e. *const T, *mut T, &T or &mut T. The pointed-to type must implement Arbitrary.

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 to have at least one designated proof_for_contract harness for checking the contract.