Crate prusti_contracts Copy item path Source body_invariant A macro for writing a loop body invariant. body_variant A macro to annotate body variant of a loop to prove termination closure A macro for defining a closure with a specification.
Note: this is a declarative macro defined in this crate
because declarative macros can’t be exported from
the prusti-contracts-proc-macros proc-macro crate.
See https://github.com/rust-lang/rust/issues/40090 . ghost A macro for defining ghost blocks which will be left in for verification
but omitted during compilation. predicate A macro for defining a predicate using prusti expression syntax instead
of just Rust expressions. prusti_assert A macro for writing assertions using the full prusti specifications prusti_assert_eq prusti_assert_ne prusti_assume A macro for writing assumptions using prusti syntax prusti_refute A macro for writing refutations using prusti syntax Ghost Int a mathematical (unbounded) integer type
it should not be constructed from running rust code, hence the private unit inside Map A map type Seq A sequence type before_expiry This function is used to evaluate an expression in the context just
before the borrows expires. exists Existential quantifier. forall Universal quantifier. old This function is used to evaluate an expression in the “old”
context, that is at the beginning of the method call. snap Creates an owned copy of a reference. This should only be used from within
ghost code, as it circumvents the borrow checker. snapshot_equality Snapshot, “logical”, or “mathematical” equality. Compares the in-memory
representation of two instances of the same type, even if there is no
PartialEq nor Copy implementation. The in-memory representation is
constructed recursively: references are followed, unsafe pointers and cells
are not. Importantly, addresses are not taken into consideration. after_expiry A macro for writing a pledge on a function. assert_on_expiry A macro for writing a two-state pledge on a function. ensures A macro for writing a postcondition on a function. extern_spec A macro for specifying external functions. invariant A macro for type invariants. model Macro for creating type models. print_counterexample A macro to customize how a struct or enum should be printed in a counterexample pure A macro for marking a function as pure. refine_spec A macro to add trait bounds on a generic type parameter and specifications
which are active only when these bounds are satisfied for a call. refine_trait_spec A macro for impl blocks that refine trait specifications. requires A macro for writing a precondition on a function. terminates A macro to annotate termination of a function trusted A macro for marking a function as trusted. verified A macro for marking a function as opted into verification.