Model Checking Rmc Versions Save

Kani Rust verifier release bundle version 0.51.0.

What's Changed

• Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in https://github.com/model-checking/kani/pull/3134
• Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in https://github.com/model-checking/kani/pull/3169
• Emit source locations whenever possible to ease debugging and coverage reporting by @tautschnig in https://github.com/model-checking/kani/pull/3173
• Rust toolchain upgraded to nightly-2024-04-21 by @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.50.0...kani-0.51.0

Major Changes

• Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (https://github.com/model-checking/kani/issues/3138).

What's Changed

• Implement valid value check for write_bytes by @celinval in https://github.com/model-checking/kani/pull/3108
• Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0

What's Changed

• Disable removal of storage markers by @zhassan-aws in https://github.com/model-checking/kani/pull/3083
• Ensure storage markers are kept in std code by @zhassan-aws in https://github.com/model-checking/kani/pull/3080
• Implement validity checks by @celinval in https://github.com/model-checking/kani/pull/3085
• Allow modifies clause for verification only by @feliperodri in https://github.com/model-checking/kani/pull/3098
• Add optional scatterplot to benchcomp output by @tautschnig in https://github.com/model-checking/kani/pull/3077
• Expand ${var} in benchcomp variant env by @karkhaz in https://github.com/model-checking/kani/pull/3090
• Add benchcomp filter command by @karkhaz in https://github.com/model-checking/kani/pull/3105
• Upgrade Rust toolchain to 2024-03-29 by @zhassan-aws @celinval @adpaco-aws @feliperodri

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.48.0...kani-0.49.0

Major Changes

• We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in https://github.com/model-checking/kani/pull/3063

What's Changed

• Fix codegen_atomic_binop for atomic_ptr by @qinheping in https://github.com/model-checking/kani/pull/3047
• Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045
• Add --use-local-toolchain to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056
• Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064
• Add option to override --crate-name from kani by @adpaco-aws in https://github.com/model-checking/kani/pull/3054
• Add method to assert a pointer is valid by @celinval in https://github.com/model-checking/kani/pull/3062
• Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0

What's Changed

• Upgrade toolchain to 2024-02-14 by @zhassan-aws in https://github.com/model-checking/kani/pull/3036

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.46.0...kani-0.47.0

What's Changed

• modifies Clauses for Function Contracts by @JustusAdam in https://github.com/model-checking/kani/pull/2800
• Fix ICEs due to mismatched arguments by @celinval in https://github.com/model-checking/kani/pull/2994. Resolves the following issues:
  • https://github.com/model-checking/kani/issues/2260
  • https://github.com/model-checking/kani/issues/2312
• Enable powf*, exp*, log* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2996
• Upgrade Rust toolchain to nightly-2024-01-25 by @celinval @feliperodri @qinheping

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.45.0...kani-0.46.0

Kani Rust verifier release bundle version 0.45.0.

What's Changed

• Upgrade toolchain to nightly-2024-01-17 by @celinval in https://github.com/model-checking/kani/pull/2976

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0

Kani Rust verifier release bundle version 0.44.0.

What's Changed

• Rust toolchain upgraded to nightly-2024-01-08 by @adpaco-aws @celinval @zhassan-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.43.0...kani-0.44.0

Kani Rust verifier release bundle version 0.43.0.

What's Changed

• Rust toolchain upgraded to nightly-2023-12-14 by @tautschnig and @adpaco-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.42.0...kani-0.43.0

Kani Rust verifier release bundle version 0.42.0.

What's Changed

• Build CBMC from source and install as package on non-x86_64 by @bennofs in https://github.com/model-checking/kani/pull/2877 and https://github.com/model-checking/kani/pull/2878
• Emit suggestions and an explanation when CBMC runs out of memory by @JustusAdam in https://github.com/model-checking/kani/pull/2885
• Rust toolchain upgraded to nightly-2023-11-28 by @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.41.0...kani-0.42.0