kani-0.55.0
github-actions
released this
05 Sep 17:09
·
189 commits
to main
since this release
Kani Rust verifier release bundle version 0.55.0.
Major/Breaking Changes
- Coverage reporting in Kani is now source-based instead of line-based.
Consequently, the unstable-Zline-coverage
flag has been replaced with a-Zsource-coverage
one.
Check the Source-Coverage RFC for more details. - Several improvements were made to the memory initialization checks. The current state is summarized in #3300. We welcome your feedback!
What's Changed
- Update CBMC build instructions for Amazon Linux 2 by @tautschnig in #3431
- Implement memory initialization state copy functionality by @artemagvanian in #3350
- Make points-to analysis handle all intrinsics explicitly by @artemagvanian in #3452
- Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in #3438
- Fix ICE due to mishandling of Aggregate rvalue for raw pointers to
str
by @celinval in #3448 - Basic support for memory initialization checks for unions by @artemagvanian in #3444
- Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in #3119
- Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in #3419
- Partially integrate uninit memory checks into
verify_std
by @artemagvanian in #3470 - Rust toolchain upgraded to
nightly-2024-09-03
by @jaisnan @carolynzech
Full Changelog: kani-0.54.0...kani-0.55.0