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 these considerations we get these families of macros: * assume macros * postcondition macros (like verify where defined and like assume for callers) * 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 ('checkedmacro') * checked at runtime only for debug builds ('debugchecked_macro')
Additionally, the runtime checked kinds provides eq and ne varieties, leaving us (for assume) with: * assume! * checkedassume! * checkedassumeeq! * checkedassumene! * debugcheckedassume! * debugcheckedassumeeq! * debugcheckedassume_ne!
Likewise for postcondition! precondition! and verify!
Additionally we also have: * assumedpostcondition! which is an assume at the definition site, rather than a verify. * assumepreconditions! which assumes that the caller has satisfied all (inferred) preconditions of the next call. * assumeunreachable! which assumes that it is unreachable for reasons beyond what MIRAI can reason about. * unrecoverable! which is the same as panic! but explicitly indicates that this is not a programming mistake. * verifyunreachable! which requires MIRAI to verify that it is not unreachable.
This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are: * abstractvalue! * getmodelfield! * result! * setmodel_field!
See the documentation for details on how to use these.