Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Releases: facebookexperimental/MIRAI

v1.0.3

11 Sep 02:10
75d790f
Compare
Choose a tag to compare

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

11 Sep 17:58
Compare
Choose a tag to compare

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

27 Aug 03:27
Compare
Choose a tag to compare

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

16 Aug 20:42
Compare
Choose a tag to compare

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

02 Aug 19:59
Compare
Choose a tag to compare

This release can handle the Libra code base, at least for now.