Crate kani

Source

Re-exports§

pub use invariant::Invariant;
pub use futures::RoundRobin;
pub use futures::block_on;
pub use futures::block_on_with_spawn;
pub use futures::spawn;
pub use futures::yield_now;

Modules§

arbitrary
This module introduces the Arbitrary trait as well as implementation for primitive types and other std containers.
contracts
Kani implementation of function contracts.
float
This module contains functions useful for float-related checks
futures
This module contains functions to work with futures (and async/.await) in Kani.
invariant
This module introduces the Invariant trait as well as its implementation for primitive types.
mem
This module contains functions useful for checking unsafe memory access.
shadow
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.
slice
vec

Macros§

arbitrary_tuple
This macro implements kani::Arbitrary on a tuple whose elements already implement kani::Arbitrary by running kani::any() on each index of the tuple.
cover
generate_arbitrary
generate_float
generate_models
implies
implies!(premise => conclusion) means that if the premise is true, so must be the conclusion.
kani_intrinsics
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.
kani_lib
Users should only need to invoke this.
kani_mem
kani_mem_init
ptr_generator
ptr_generator_fn
slice_generator

Structs§

ArbitraryPointer
Holds information about a pointer that is generated non-deterministically.
PointerGenerator
Pointer generator that can be used to generate arbitrary pointers.

Enums§

AllocationStatus
Enumeration with the cases currently covered by the pointer generator.

Traits§

Arbitrary

Functions§

any
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.
any_where
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.
assert
Creates an assertion of the specified condition and message.
assume
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.
concrete_playback_run
NOP concrete_playback for type checking during verification mode.
cover
Creates a cover property with the specified condition and message.
pointer_generator
Create a pointer generator that fits at least N elements of type T.

Attribute Macros§

ensures
Add a postcondition to this function.
loop_invariant
Add a loop invariant to this loop.
modifies
Declaration of an explicit write-set for the annotated function.
proof
Marks a Kani proof harness
proof_for_contract
Designates this function as a harness to check a function contract.
recursion
Specifies that a function contains recursion for contract instrumentation.**
requires
Add a precondition to this function.
should_panic
Specifies that a proof harness is expected to panic.**
solver
Select the SAT solver to use with CBMC for this harness
stub
Specify a function/method stub pair to use for proof harness
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.
unwind
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§

Arbitrary
Allow users to auto generate Arbitrary implementations by using #[derive(Arbitrary)] macro.
Invariant
Allow users to auto generate Invariant implementations by using #[derive(Invariant)] macro.