[−][src]Crate mirai_annotations
Macros
abstract_value | Provides a way to specify a value that should be treated abstractly by the verifier. The concrete argument provides type information to the verifier and a meaning for the expression when compiled by the rust compiler. |
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. |