kani-0.57.0

Major Changes

• kani-cov: A coverage tool for Kani by @adpaco-aws in #3121
• Add a timeout option by @zhassan-aws in #3649
• Loop Contracts Annotation for While-Loop by @qinheping in #3151
• Harness output individual files by @Alexander-Aghili in #3360
• Enable support for Ubuntu 24.04 by @tautschnig in #3758

Breaking Changes

• Make kani::check private by @celinval in #3614
• Remove symtab json support by @celinval in #3695
• Remove CBMC viewer and visualize option by @zhassan-aws in #3699
• Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in #3744

What's Changed

• Remove the overflow checks for wrapping_offset by @zhassan-aws in #3589
• Support fully-qualified --package arguments by @celinval in #3593
• Implement proper function pointer handling for validity checks by @celinval in #3606
• Add fn that checks pointers point to same allocation by @celinval in #3583
• [Lean back-end] Preserve variable names by @zhassan-aws in #3560
• Emit an error when proof_for_contract function is not found by @zhassan-aws in #3609
• [Lean back-end] Rename user-facing options from Aeneas to Lean by @zhassan-aws in #3630
• Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in #3636
• Fix loop contracts transformation when loops in branching by @qinheping in #3640
• Move any_slice_from_array to kani_core by @qinheping in #3646
• Implement Arbitrary for Range* by @c410-f3r in #3666
• Add support for float_to_int_unchecked by @zhassan-aws in #3660
• Change same_allocation to accept wide pointers by @celinval in #3684
• Derive Arbitrary for enums with a single variant by @AlgebraicWolf in #3692
• Apply loop contracts only if there exists some usage by @qinheping in #3694
• Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in #3701
• Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in #3644
• Improve Kani handling of function markers by @celinval in #3718
• Enable contracts for const generic functions by @qinheping in #3726
• List Subcommand Improvements by @carolynzech in #3729
• [Lean back-end] add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in #3721
• Fix issues with how we compute DST size by @celinval in #3687
• Fix size and alignment computation for intrinsics by @celinval in #3734
• Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in #3742
• Add out of bounds check for offset intrinsics by @celinval in #3755
• Automatic upgrade of CBMC from 6.3.1 to 6.4.1
• Rust toolchain upgraded to nightly-2024-12-15 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig

Full Changelog: kani-0.56.0...kani-0.57.0

kani-0.56.0

Major/Breaking Changes

• Remove obsolete linker options (--mir-linker and --legacy-linker) by @zhassan-aws in #3559
• List Subcommand by @carolynzech in #3523
• Deprecate kani::check by @celinval in #3557

What's Changed

• Enable stubbing and function contracts for primitive types by @celinval in #3496
• Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in #3513
• Fail compilation if proof_for_contract is added to generic function by @carolynzech in #3522
• Fix storing coverage data in cargo projects by @adpaco-aws in #3527
• Add experimental API to generate arbitrary pointers by @celinval in #3538
• Running verify-std no longer changes Cargo files by @celinval in #3577
• Add an LLBC backend by @zhassan-aws in #3514
• Fix the computation of the number of bytes of a pointer offset by @zhassan-aws in #3584
• Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
• CBMC upgraded to 6.3.1 by @tautschnig in #3537

Full Changelog: kani-0.55.0...kani-0.56.0

kani-0.55.0

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

kani-0.54.0

Major Changes

• We added support for slices in the #[kani::modifies(...)] clauses when using function contracts.
• We introduce an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros.
• We enabled support for concrete playback for harness that contains stubs or function contracts.
• We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.

Breaking Changes

• The -Z ptr-to-ref-cast-checks option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.

What's Changed

• Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332
• Fix visibility of some Kani intrinsics by @artemagvanian in #3323
• Function Contracts: Modify Slices by @pi314mm in #3295
• Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344
• Add support for global transformations by @artemagvanian in #3348
• Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros by @adpaco-aws in #3283
• Fix contract handling of promoted constants and constant static by @celinval in #3305
• Bump CBMC Viewer to 3.9 by @tautschnig in #3373
• Update to CBMC version 6.1.1 by @tautschnig in #2995
• Define a struct-level #[safety_constraint(...)] attribute by @adpaco-aws in #3270
• Enable concrete playback for contract and stubs by @celinval in #3389
• Add code scanner tool by @celinval in #3120
• Enable contracts in associated functions by @celinval in #3363
• Enable log2*, log10* intrinsics by @tautschnig in #3001
• Enable powif* intrinsics by @tautschnig in #2999
• Enable fma* intrinsics by @tautschnig in #3002
• Enable sqrt* intrinsics by @tautschnig in #3000
• Remove assigns clause for ZST pointers by @carolynzech in #3417
• Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374
• Unify kani library and kani core logic by @jaisnan in #3333
• Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426
• Rust toolchain upgraded to nightly-2024-08-07 by @jaisnan @qinheping @tautschnig @feliperodri

New Contributors

• @carolynzech made their first contribution in #3387

Full Changelog: kani-0.53.0...kani-0.54.0

kani-0.53.0

Major Changes

• The --visualize option is being deprecated and will be removed in a future release. Consider using the --concrete-playback option instead.
• The -Z ptr-to-ref-cast-checks option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
• The -Z uninit-checks option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the -Z ghost-state option.

Breaking Changes

• Remove support for the unstable argument --function by @celinval in #3278
• Remove deprecated --enable-stubbing by @celinval in #3309

What's Changed

• Change ensures into closures by @pi314mm in #3207
• (Re)introduce Invariant trait by @adpaco-aws in #3190
• Remove empty box creation from contracts impl by @celinval in #3233
• Add a new verify-std subcommand to Kani by @celinval in #3231
• Inject pointer validity check when casting raw pointers to references by @artemagvanian in #3221
• Do not turn trivially diverging loops into assume(false) by @tautschnig in #3223
• Fix "unused mut" warnings created by generated code. by @jsalzbergedu in #3247
• Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in #3245
• Use cfg=kani_host for host crates by @tautschnig in #3244
• Add intrinsics and Arbitrary support for no_core by @jaisnan in #3230
• Contracts: Avoid attribute duplication and const function generation for constant function by @celinval in #3255
• Fix contract of constant fn with effect feature by @celinval in #3259
• Fix typed_swap for ZSTs by @tautschnig in #3256
• Add a #[derive(Invariant)] macro by @adpaco-aws in #3250
• Contracts: History Expressions via "old" monad by @pi314mm in #3232
• Function Contracts: remove instances of _renamed by @pi314mm in #3274
• Deprecate --visualize in favor of concrete playback by @celinval in #3281
• Fix operand in fat pointer comparison by @pi314mm in #3297
• Function Contracts: Closure Type Inference by @pi314mm in #3307
• Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in #3306
• Towards Proving Memory Initialization by @artemagvanian in #3264
• Rust toolchain upgraded to nightly-2024-07-01 by @tautschnig @celinval @jaisnan @adpaco-aws

Full Changelog: kani-0.52.0...kani-0.53.0

kani-0.52.0

What's Changed

• New section about linter configuraton checking in the doc by @remi-delmas-3000 in #3198
• Fix {,e}println!() by @GrigorenkoPV in #3209
• Contracts for a few core functions by @celinval in #3107
• Add simple API for shadow memory by @zhassan-aws in #3200
• Upgrade Rust toolchain to 2024-05-28 by @zhassan-aws @remi-delmas-3000 @qinheping

Full Changelog: kani-0.51.0...kani-0.52.0

kani-0.51.0

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 #3134
• Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in #3169
• Emit source locations whenever possible to ease debugging and coverage reporting by @tautschnig in #3173
• Rust toolchain upgraded to nightly-2024-04-21 by @celinval

Full Changelog: kani-0.50.0...kani-0.51.0

kani-0.50.0

Major Changes

• Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (#3138).

What's Changed

• Implement valid value check for write_bytes by @celinval in #3108
• Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

Full Changelog: kani-0.49.0...kani-0.50.0

kani-0.49.0

What's Changed

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

Full Changelog: kani-0.48.0...kani-0.49.0

kani-0.48.0

Major Changes

• We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in #3063

What's Changed

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

Full Changelog: kani-0.47.0...kani-0.48.0