Releases: facebookexperimental/MIRAI
v1.0.3
Make --sysroot available for the command line.
Add a rust-toolchain
Make core::slice::Iter methods generic.
Add def ids for un-summarized functions in the call graph being analyzed.
Add (assume|verify)_unreachable macros.
Make the result of an uninterpreted call more complete to allow better refinement.
Promote pre/post conditions for async functions.
v1.0.3 for Libra
Make --sysroot available for the command line.
Add a rust-toolchain
Make core::slice::Iter methods generic.
Add def ids for un-summarized functions in the call graph being analyzed.
Add (assume|verify)_unreachable macros.
Make the result of an uninterpreted call more complete to allow better refinement.
Promote pre/post conditions for async functions.
v1.0.2 for LIBRA
Standard library summaries for cmp::max.
Use joins for conditional expressions with conditions that are TOP.
Fix bug in refinement of conditional expressions.
Apply binary operation distribution recursively during expression simplification.
Discard join condition when joining backward branches (keeps path conditions simpler during fixed point loops).
v1.0.1 for LIBRA
Fixes a bug with name mangling when macros are involved.
More standard library contracts.
Updates dependencies.
Ignores predecessor blocks that are known not to reach a block after round 1 of the fixed point loop.
Fixes diagnostic formatting that resulted in "possible possible ..." messages.
Initial release for use by Libra
This release can handle the Libra code base, at least for now.