This module contains an API for shadow memory.
Shadow memory is a mechanism by which we can store metadata on memory
locations, e.g. whether a memory location is initialized.
Kani intrinsics contains the public APIs used by users to verify their harnesses.
This macro is a part of kani_core as that allows us to verify even libraries that are no_core
such as core in rust’s std library itself.
This creates a symbolic valid value of type T.
The value is constrained to be a value accepted by the predicate passed to the filter.
You can assign the return value of this function to a variable that you want to make symbolic.
Creates an assumption that will be valid after this statement run. Note that the assumption
will only be applied for paths that follow the assumption. If the assumption doesn’t hold, the
program will exit successfully.
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.
Set Loop unwind limit for proof harnesses
The attribute #[kani::unwind(arg)] can only be called alongside #[kani::proof].
arg - Takes in a integer value (u32) that represents the unwind value for the harness.