Merge remote-tracking branch 'origin/main' into fix-3129

.github/workflows/cbmc-update.yml

@@ -30,7 +30,7 @@ jobs:
  env:
  GH_TOKEN: ${{ github.token }}
  run: |
- grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV
+ grep ^CBMC_VERSION kani-dependencies | sed 's/"//g' >> $GITHUB_ENV
  CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-)
  echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV
  # check whether the version has changed at all
@@ -47,8 +47,8 @@ jobs:
  elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
  CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
  CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
- sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
- sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
+ sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_LATEST_MAJOR\"/" kani-dependencies
+ sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies
  sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
  git diff
  if ! ./scripts/kani-regression.sh ; then
@@ -79,7 +79,7 @@ jobs:
  token: ${{ github.token }}
  title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed'
  body: >
- Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
+ Updating CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
 
  The failed automated run
  [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})

.github/workflows/toolchain-upgrade.yml

@@ -30,42 +30,11 @@ jobs:
  env:
  GH_TOKEN: ${{ github.token }}
  run: |
- current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/')
- echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV
- current_toolchain_epoch=$(date --date $current_toolchain_date +%s)
- next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d)
- echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV
- if gh issue list -S \
- "Toolchain upgrade to nightly-$next_toolchain_date failed" \
- --json number,title | grep title ; then
- echo "next_step=none" >> $GITHUB_ENV
- elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date ; then
- echo "next_step=create_pr" >> $GITHUB_ENV
- sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml
- git diff
- git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git
- cd rust.git
- current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
- echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV
- next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
- echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV
- EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
- echo "git_log<<$EOF" >> $GITHUB_ENV
- git log --oneline $current_toolchain_hash..$next_toolchain_hash | \
- sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV
- echo "$EOF" >> $GITHUB_ENV
- cd ..
- rm -rf rust.git
- if ! cargo build-dev ; then
- echo "next_step=create_issue" >> $GITHUB_ENV
- else
- if ! ./scripts/kani-regression.sh ; then
- echo "next_step=create_issue" >> $GITHUB_ENV
- fi
- fi
- else
- echo "next_step=none" >> $GITHUB_ENV
- fi
+ source scripts/toolchain_update.sh
+
+ - name: Clean untracked files
+ run: git clean -f
+
  - name: Create Pull Request
  if: ${{ env.next_step == 'create_pr' }}
  uses: peter-evans/create-pull-request@v6

.gitignore

@@ -48,6 +48,10 @@ no_llvm_build
 /tmp/
 # Created by default with `src/ci/docker/run.sh`
 /obj/
+# Created by kani-compiler
+*.rlib
+*.rmeta
+*.mir
 
 ## Temporary files
 *~

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.50.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
+
 ## [0.49.0]
 
 ### What's Changed