Re-exports§
pub use arbitrary::Arbitrary;
pub use futures::block_on;
pub use futures::block_on_with_spawn;
pub use futures::spawn;
pub use futures::yield_now;
pub use futures::RoundRobin;
Modules§
- This module introduces the Arbitrary trait as well as implementation for primitive types and other std containers.
- Kani implementation of function contracts.
- This module contains functions to work with futures (and async/.await) in Kani.
- This module contains functions useful for checking unsafe memory access.
- Support for arbitrary tuples where each element implements
kani::Arbitrary
. Tuples of size up to 12 are supported in this file.
Macros§
- A macro to check if a condition is satisfiable at a specific location in the code.
implies!(premise => conclusion)
means that if thepremise
is true, so must be theconclusion
.
Functions§
- This creates an symbolic valid value of type
T
. You can assign the return value of this function to a variable that you want to make symbolic. - 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 assertion of the specified condition and message.
- 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.
- NOP
concrete_playback
for type checking during verification mode. - Creates a cover property with the specified condition and message.
Attribute Macros§
- Add a postcondition to this function.
- Declaration of an explicit write-set for the annotated function.
- Marks a Kani proof harness
- Designates this function as a harness to check a function contract.
- Add a precondition to this function.
- Specifies that a proof harness is expected to panic.**
- Select the SAT solver to use with CBMC for this harness
- Specify a function/method stub pair to use for proof harness
stub_verified(TARGET)
is a harness attribute (to be used onproof
orproof_for_contract
function) that replaces all occurrences ofTARGET
reachable from this harness with a stub generated from the contract onTARGET
.- 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.
Derive Macros§
- Allow users to auto generate Arbitrary implementations by using
#[derive(Arbitrary)]
macro.