Skip to content

kani-0.65.0

Choose a tag to compare

@github-actions github-actions released this 07 Aug 21:07
· 354 commits to main since this release
677c791

[0.65.0]

Breaking Changes

Major Changes

  • Added support for a few SMT solvers (bitwuzla, cvc5, and z3) as solver attribute values (not packaged with Kani) by @tautschnig in #4218
  • Improved support for contracts and stubs in trait implementations, expanding verification capabilities for trait-based code by @carolynzech in #4250
  • Added new --prove-safety-only option for focused safety verification, allowing you to concentrate on memory safety and undefined behavior detection by @tautschnig in #4239
  • Extended autoharness support to handle references, making it easier to automatically generate verification harnesses by @tautschnig in #4234
  • Multiple performance improvements including parallel goto binary writing, lazy debug info evaluation, and optimized quantifier handling for faster verification times

What's Changed

  • Fixed issue related to the handling of contract closures which was preventing writing contracts for functions that return mutable references by @vonaka in #4151
  • Relaxed the constraint on the pointer type for Kani's memory predicates by @tautschnig in #4193
  • Changed the model for ptr_offset_from to enhance verification performance by @tautschnig in #4180
  • Fixed assign clause inference bug for nested loops by @thanhnguyen-aws in #4179
  • Fixed crash when using multiple quantifiers in one proof by @thanhnguyen-aws in #4221
  • Added support for Cargo.toml's default-members configuration by @tautschnig in #4201
  • Improved memset handling to avoid zero-count invocations by @tautschnig in #4205
  • Enhanced safety by disabling debug assertions under prove-safety-only by @tautschnig in #4262
  • Enhanced performance with parallel goto binary writing by @AlexanderPortland in #4236
  • Improved quantifier handling performance by avoiding irrelevant symbol updates by @AlexanderPortland in #4268
  • Enhanced performance with lazy debug info evaluation by @AlexanderPortland in #4269
  • Improved MIR constant handling by marking them as static constants by @vonaka in #4233

New Contributors

Version Updates

Full Changelog: kani-0.64.0...kani-0.65.0