Crate mirai_annotations

Macros

assume	Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
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.
assume_unreachable	Equivalent to unreachable! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume that the annotation statement cannot be reached.
assumed_postcondition	Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
checked_assume	Equivalent to the standard assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
checked_assume_eq	Equivalent to the standard assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
checked_assume_ne	Equivalent to the standard assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
checked_postcondition	Equivalent to the standard assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
checked_postcondition_eq	Equivalent to the standard assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
checked_postcondition_ne	Equivalent to the standard assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
checked_precondition	Equivalent to the standard assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
checked_precondition_eq	Equivalent to the standard assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
checked_precondition_ne	Equivalent to the standard assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
checked_verify	Equivalent to the standard assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
checked_verify_eq	Equivalent to the standard assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
checked_verify_ne	Equivalent to the standard assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
debug_checked_assume	Equivalent to the standard debug_assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
debug_checked_assume_eq	Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
debug_checked_assume_ne	Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to assume the condition unless it can prove it to be false.
debug_checked_postcondition	Equivalent to the standard debug_assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
debug_checked_postcondition_eq	Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
debug_checked_postcondition_ne	Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
debug_checked_precondition	Equivalent to the standard debug_assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
debug_checked_precondition_eq	Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
debug_checked_precondition_ne	Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
debug_checked_verify	Equivalent to the standard debug_assert! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
debug_checked_verify_eq	Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
debug_checked_verify_ne	Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
get_model_field	Retrieves the value of the specified model field, or the given default value if the model field is not set. This function has no meaning outside of a verification condition and should not be used with checked or debug_checked conditions. For example: precondition!(get_model_field!(x, f) > 1).
postcondition	Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify the condition at the point where it appears in a function, but to also add it a postcondition that can be assumed by the caller of the function.
precondition	Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI 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.
result	Provides a way to refer to the result value of an abstract or contract function without specifying an actual value anywhere. This macro expands to unimplemented!() unless the program is compiled with MIRAI. It result should therefore not be assigned to a variable unless the assignment is contained inside a specification macro argument list. It may, however, be the return value of the function, which should never be called and therefore unimplemented!() is the right behavior for it at runtime.
set_model_field	Sets the value of the specified model field. A model field does not exist at runtime and is invisible to the Rust compiler. This macro expands to nothing unless the program is compiled with MIRAI.
verify	Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to check the condition and emit a diagnostic unless it can prove it to be true.
verify_unreachable	Equivalent to unreachable! when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to verify that the annotation statement cannot be reached.