🔒 Use separate lock file to avoid panic in Sled.
Only share the persistent store between crates if flag is present.
Contracts for variants of
Give diagnostics if non public function is a call tree root.
MIR assertions now treated just like verify.
👉 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.
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).
🛠 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.
🚀 This release can handle the Libra code base, at least for now.