Merge branch 'main' into std-non-null

Author: celinval

.github/workflows/bench.yml

@@ -55,12 +55,6 @@ jobs:
           os: ubuntu-20.04
           kani_dir: new
 
-      - name: Build Kani (new variant)
-        run: pushd new && cargo build-dev
-
-      - name: Build Kani (old variant)
-        run: pushd old && cargo build-dev
-
       - name: Copy benchmarks from new to old
         run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
 

.github/workflows/cbmc-latest.yml

@@ -32,10 +32,6 @@ jobs:
           os: ${{ matrix.os }}
           kani_dir: 'kani'
 
-      - name: Build Kani
-        working-directory: ./kani
-        run: cargo build-dev
-
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v4
         with:

.github/workflows/kani-m1.yml

@@ -23,8 +23,5 @@ jobs:
         with:
           os: macos-13-xlarge
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh

.github/workflows/kani.yml

@@ -27,9 +27,6 @@ jobs:
         with:
           os: ${{ matrix.os }}
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
@@ -88,47 +85,19 @@ jobs:
         with:
           os: ubuntu-20.04
 
-      - name: Build Kani using release mode
-        run: cargo build-dev -- --release
-
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
         env:
           RUST_TEST_THREADS: 1
 
-  bookrunner:
+  documentation:
     runs-on: ubuntu-20.04
     permissions:
       contents: write
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
 
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev
-
-      - name: Install book runner dependencies
-        run: ./scripts/setup/install_bookrunner_deps.sh
-
-      - name: Generate book runner report
-        run: cargo run -p bookrunner
-        env:
-          DOC_RUST_LANG_ORG_CHANNEL: nightly
-
-      - name: Print book runner text results
-        run: cat build/output/latest/html/bookrunner.txt
-
-      - name: Print book runner failures grouped by stage
-        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html
-
-      - name: Detect unexpected book runner failures
-        run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
-
       - name: Install book dependencies
         run: ./scripts/setup/ubuntu/install_doc_deps.sh
 

.github/workflows/release.yml

@@ -136,7 +136,7 @@ jobs:
       - name: Get toolchain version used to setup kani
         run: |
           tar zxvf ${{ matrix.prev_job.bundle }}
-          DATE=$(cat ./kani-latest/rust-toolchain-version | cut -d'-' -f2,3,4)
+          DATE=$(cat ./kani-${{ matrix.prev_job.version }}/rust-toolchain-version | cut -d'-' -f2,3,4)
           echo "Nightly date: $DATE"
           echo "DATE=$DATE" >> $GITHUB_ENV
 

.gitignore

@@ -74,10 +74,8 @@ package-lock.json
 tests/rustdoc-gui/src/**.lock
 
 # Before adding new lines, see the comment at the top.
-/.litani_cache_dir
 /.ninja_deps
 /.ninja_log
-/tests/bookrunner
 *Cargo.lock
 tests/kani-dependency-test/diamond-dependency/build
 tests/kani-multicrate/type-mismatch/mismatch/target

.gitmodules

@@ -1,12 +1,3 @@
-[submodule "src/doc/nomicon"]
-	path = tools/bookrunner/rust-doc/nomicon
-	url = https://github.com/rust-lang/nomicon.git
-[submodule "src/doc/reference"]
-	path = tools/bookrunner/rust-doc/reference
-	url = https://github.com/rust-lang/reference.git
-[submodule "src/doc/rust-by-example"]
-	path = tools/bookrunner/rust-doc/rust-by-example
-	url = https://github.com/rust-lang/rust-by-example.git
 [submodule "firecracker"]
 	path = firecracker
 	url = https://github.com/firecracker-microvm/firecracker.git

CHANGELOG.md

@@ -4,6 +4,20 @@ 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.49.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
+
 ## [0.48.0]
 
 ### Major Changes