MIRAI changelog

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 of rand.Rng.gen_range and rand.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, 2019

  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 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.