MIRAI Annotations

This crate provides a set of macros that can be used in the place of the standard RUST assert and debug_assert macros. They add value by allowing MIRAI to:

• distinguish between path conditions and verification conditions
• distinguish between conditions that it should assume as true and conditions that it should verify
• check conditions at compile time that should not be checked at runtime because they are too expensive

From this it follows that we have three families of macros:

• assume macros
• precondition macros (like assume where defined and like verify for callers)
• verify macros

Each of these has three kinds

• only checked at compile time ('macro' with macro among {assume, precondition, verify})
• always checked at runtime ('checked_macro')
• checked at runtime only for debug builds ('debug_checked_macro')

Additionally, the runtime checked kinds provides eq and ne varieties, leaving us with:

• assume!
• checked_assume!
• checked_assume_eq!
• checked_assume_ne!
• debug_checked_assume!
• debug_checked_assume_eq!
• debug_checked_assume_ne!
• precondition!
• checked_precondition!
• checked_precondition_eq!
• checked_precondition_ne!
• debug_checked_precondition!
• debug_checked_precondition_eq!
• debug_checked_precondition_ne!
• verify!
• checked_verify!
• checked_verify_eq!
• checked_verify_ne!
• debug_checked_verify!
• debug_checked_verify_eq!
• debug_checked_verify_ne!

This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are:

• get_model_field!
• result!
• set_model_field!

See the documentation for details on how to use these.