Macro mirai_annotations::checked_precondition

macro_rules! checked_precondition {
    ($condition:expr) => { ... };
    ($condition:expr, $message:literal) => { ... };
    ($condition:expr, $($arg:tt)*) => { ... };
}

Equivalent to the standard assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes the compiler to assume the condition at the point where it appears in a function, but to also add it a precondition that must be verified by the caller of the function.