Function kani::cover

source ·
pub const fn cover(_cond: bool, _msg: &'static str)
Expand description

Creates a cover property with the specified condition and message.


kani::cover(slice.len() == 0, "The slice may have a length of 0");

A cover property checks if there is at least one execution that satisfies the specified condition at the location in which the function is called.

Cover properties are reported as:

  • SATISFIED: if Kani found an execution that satisfies the condition
  • UNSATISFIABLE: if Kani proved that the condition cannot be satisfied
  • UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE)

This function is called by the cover! macro. The macro is more convenient to use.