Crate prusti_specs

Modules

• specifications

Macros

• parse_quote_spanned
  Same as parse_quote!, but applies a given span to all tokens originating within the macro invocation.

Enums

• ExternSpecKind
• SpecAttributeKind
  This type identifies one of the procedural macro attributes of Prusti

Constants

• SPECS_VERSION

Functions

• body_invariant
• body_variant
• closure
• extern_spec
• ghost
• invariant
• predicate
• print_counterexample
• prusti_assertion
• prusti_assume
• prusti_refutation
• refine_trait_spec
• rewrite_prusti_attributes
  Rewrite an item as required by all its specification attributes.
• rewrite_prusti_attributes_for_types
• trusted
• type_model