Attribute Macro kani::stub_verified

#[stub_verified]

stub_verified(TARGET) is a harness attribute (to be used on proof or proof_for_contract function) that replaces all occurrences of TARGET reachable from this harness with a stub generated from the contract on TARGET.

The target of stub_verified must have a contract. More information about how to specify a contract for your function can be found here.

You may use multiple stub_verified attributes on a single harness.

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