Macro kani::cover

macro_rules! cover {
    () => { ... };
    ($cond:expr $(,)?) => { ... };
    ($cond:expr, $msg:literal) => { ... };
}

A macro to check if a condition is satisfiable at a specific location in the code.

Example 1:

let mut set: BTreeSet<i32> = BTreeSet::new();
set.insert(kani::any());
set.insert(kani::any());
// check if the set can end up with a single element (if both elements
// inserted were the same)
kani::cover!(set.len() == 1);

The macro can also be called without any arguments to check if a location is reachable.

Example 2:

match e {
    MyEnum::A => { /* .. */ }
    MyEnum::B => {
        // make sure the `MyEnum::B` variant is possible
        kani::cover!();
        // ..
    }
}

A custom message can also be passed to the macro.

Example 3:

kani::cover!(x > y, "x can be greater than y")