#mirai #annotations #panic #ir #macro


Macros that provide source code annotations for MIRAI

16 releases (stable)

1.12.0 Jul 6, 2021
1.10.1 Aug 7, 2020
1.9.1 Jul 7, 2020
1.6.0 Jan 28, 2020
0.0.1 Mar 28, 2019

#171 in Rust patterns

Download history 9994/week @ 2022-08-17 7602/week @ 2022-08-24 4196/week @ 2022-08-31 5602/week @ 2022-09-07 5043/week @ 2022-09-14 5098/week @ 2022-09-21 5359/week @ 2022-09-28 5008/week @ 2022-10-05 4099/week @ 2022-10-12 3994/week @ 2022-10-19 3509/week @ 2022-10-26 3485/week @ 2022-11-02 4290/week @ 2022-11-09 3885/week @ 2022-11-16 2892/week @ 2022-11-23 2690/week @ 2022-11-30

14,433 downloads per month
Used in 136 crates (20 directly)

MIT license

892 lines

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 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 ('checked_macro')
  • checked at runtime only for debug builds ('debug_checked_macro')

Additionally, the runtime checked kinds provides eq and ne varieties, leaving us (for assume) with:

  • assume!
  • checked_assume!
  • checked_assume_eq!
  • checked_assume_ne!
  • debug_checked_assume!
  • debug_checked_assume_eq!
  • debug_checked_assume_ne!

Likewise for postcondition! precondition! and verify!

Additionally we also have:

  • assumed_postcondition! which is an assume at the definition site, rather than a verify.
  • assume_preconditions! which assumes that the caller has satisfied all (inferred) preconditions of the next call.
  • assume_unreachable! 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 to reach this.
  • verify_unreachable! which requires MIRAI to verify that it is not reachable.

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

  • abstract_value!
  • add_tag!
  • does_not_have_tag!
  • get_model_field!
  • has_tag!
  • result!
  • set_model_field!

See the documentation for details on how to use these.

No runtime deps