#[modifies]Expand description
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.