Macro mirai_annotations::assume_preconditions

macro_rules! assume_preconditions {
    () => { ... };
}

Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume that the preconditions of the next function call have been met. This is to be used when the precondition has been inferred and involves private state that cannot be constrained by a normal assumption. Note that it is bad style for an API to rely on preconditions that cannot be checked by the caller, so this is only here for supporting legacy APIs.