Merge branch 'main' into kanicov-tool

.github/workflows/deny.yml

@@ -18,6 +18,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+        with:
+          submodules: recursive
       - uses: EmbarkStudios/cargo-deny-action@v2
         with:
           arguments: --all-features --workspace

.github/workflows/format-check.yml

@@ -47,7 +47,7 @@ jobs:
 
       - name: 'Run Clippy'
         run: |
-          cargo clippy --all -- -D warnings
+          cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings
 
       - name: 'Print Clippy Statistics'
         run: |

.github/workflows/kani.yml

@@ -98,6 +98,8 @@ jobs:
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
+        with:
+          submodules: recursive
 
       - name: Install book dependencies
         run: ./scripts/setup/ubuntu/install_doc_deps.sh

.gitignore

@@ -77,6 +77,9 @@ package-lock.json
 ## Rustdoc GUI tests
 tests/rustdoc-gui/src/**.lock
 
+## Charon/Aeneas LLBC files
+*.llbc
+
 # Before adding new lines, see the comment at the top.
 /.ninja_deps
 /.ninja_log

.gitmodules

@@ -5,3 +5,6 @@
 	path = tests/perf/s2n-quic
 	url = https://github.com/aws/s2n-quic
 	branch = main
+[submodule "charon"]
+	path = charon
+	url = https://github.com/AeneasVerif/charon

CHANGELOG.md

@@ -4,6 +4,27 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.56.0]
+
+### Breaking Changes
+
+* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559
+* Deprecate `kani::check` by @celinval in https://github.com/model-checking/kani/pull/3557
+
+### What's Changed
+
+* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496
+* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513
+* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522
+* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527
+* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538
+* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577
+* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514
+* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
+* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0
+
 ## [0.55.0]
 
 ### Major/Breaking Changes