Rust requires that all values have to be valid when assigned to or read from a place, passed to a function/primitive operation or returned from a function/primitive operation. It is UB to produce an invalid bit-pattern of a given type. We do not currently have any checks for this in Kani.

Likelihood:

If code contains this bug, Kani will not detect it. We do not have any data as to how often this occurs in practice.

Mitigation:

Warn users that this class of UB is outside the current scope of Kani.

Path to soundness:

Add a check for this.

Documentation: