Changelog History
-
v1.0.4 Changes
September 19, 2019🔒 Use separate lock file to avoid panic in Sled.
Only share the persistent store between crates if flag is present.
Contracts for variants ofrand.Rng.gen_range
andrand.Rng.gen_bool
.
Give diagnostics if non public function is a call tree root.
MIR assertions now treated just like verify. -
v1.0.3 Changes
September 11, 2019👉 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 Changes
August 27, 2019Standard 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 Changes
August 16, 2019🛠 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. -
v1.0.0 Changes
August 02, 2019🚀 This release can handle the Libra code base, at least for now.