FAQs

This section collects frequently asked questions about Kani. Please consider opening an issue if you have a question that would like to see here.

Questions

Kani doesn't fail after kani::assume(false). Why?

kani::assume(false) (or kani::assume(cond) where cond is a condition that results in false in the context of the program), won't cause errors in Kani. Instead, such an assumption has the effect of blocking all the symbolic execution paths from the assumption. Therefore, all checks after the assumption should appear as UNREACHABLE. That's the expected behavior for kani::assume(false) in Kani.

If you didn't expect certain checks in a harness to be UNREACHABLE, we recommend using the kani::cover macro to determine what conditions are possible in case you've over-constrained the harness.

I implemented the kani::Arbitrary trait for a type that's not from my crate, and got the error only traits defined in the current crate can be implemented for types defined outside of the crate. What does this mean? What can I do?

This error is due to a violation of Rust's orphan rules for trait implementations, which are explained here. In that case, you'll need to write a function that builds an object from non-deterministic variables. Inside this function you would simply return an arbitrary value by generating arbitrary values for its components.

For example, let's assume the type you're working with is this enum:

#[derive(Copy, Clone)]
pub enum Rating {
    One,
    Two,
    Three,
}

Then, you can match on a non-deterministic integer (supplied by kani::any) to return non-deterministic Rating variants:

    pub fn any_rating() -> Rating {
        match kani::any() {
            0 => Rating::One,
            1 => Rating::Two,
            _ => Rating::Three,
        }
    }

More details about this option, which also useful in other cases, can be found here.

If the type comes from std (Rust's standard library), you can open a request for adding Arbitrary implementations to the Kani library. Otherwise, there are more involved options to consider:

  1. Importing a copy of the external crate that defines the type, then implement Arbitrary there.
  2. Contributing the Arbitrary implementation to the external crate that defines the type.