Crate mirai_annotations[−][src]
Macros
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.
Equivalent to a no op when used with an unmodified Rust compiler. When compiled with MIRAI, this causes MIRAI to associate (tag) the value with the given type. Typically the type will be private to a scope so that only privileged code can add the tag. Once added, a tag cannot be removed and the tagged value may not be modified. To determine if a value has been tagged, use the has_tag! macro.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Provides a way to check if a value has not been tagged with a type using add_tag!. When compiled with an unmodified Rust compiler, this results in true. When compiled with MIRAI, this will be true if none data flows into the argument of this call has gone via a call to add_tag!.
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).
Provides a way to check if a value has been tagged with a type, using the add_tag! macro. When compiled with an unmodified Rust compiler, this results in true. When compiled with MIRAI, this will be true if all data flows into the argument of this call has gone via a call to add_tag!.
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.
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.
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.
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.
Provide a way to create tag propagation sets. It is equivalent to bitwise-or of all its arguments.
Terminates the program with a panic that is tagged as being an unrecoverable error. Use this for errors that arise in correct programs due to external factors. For example, if a file that is essential for running cannot be found for some reason.
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.
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.
Enums
An enum type of controllable operations for MIRAI tag types. In general, the result of the operation corresponding to an enum value will get tagged with all of the tags of the operands.
Constants
A tag propagation set indicating a tag is propagated by all operations.
Type Definitions
A type used to specify how tag types transfer over operations. The type is an alias of u128.
Each bit of the bit vector controls the transfer function for an operation.
If a bit is set to one, the corresponding operation will propagate the tag.
If a bit is set to zero, the corresponding operation will block the tag.