Function kani::cover

pub const fn cover(_cond: bool, _msg: &'static str)

Creates a cover property with the specified condition and message.

Example:

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.