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.