Skip to content

Commit 5d44de0

Browse files
authored
Update CBMC version to 5.94 (rust-lang#2821)
Update CBMC version to 5.94 and change our regression script to read the values from kani-dependencies instead of requiring us to keep two sources of truth.
1 parent acca86d commit 5d44de0

File tree

2 files changed

+17
-4
lines changed

2 files changed

+17
-4
lines changed

kani-dependencies

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,10 @@
1-
CBMC_VERSION="5.93.0"
1+
CBMC_MAJOR="5"
2+
CBMC_MINOR="94"
3+
CBMC_VERSION="5.94.0"
4+
25
# If you update this version number, remember to bump it in `src/setup.rs` too
6+
CBMC_VIEWER_MAJOR="3"
7+
CBMC_VIEWER_MINOR="8"
38
CBMC_VIEWER_VERSION="3.8"
9+
410
KISSAT_VERSION="3.1.1"

scripts/kani-regression.sh

+10-3
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,16 @@ KANI_DIR=$SCRIPT_DIR/..
1818
# TODO: We should add a more robust mechanism to detect python unexpected behavior.
1919
export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
2020

21-
# Required dependencies
22-
check-cbmc-version.py --major 5 --minor 93
23-
check-cbmc-viewer-version.py --major 3 --minor 8
21+
# Gather dependencies version from top `kani-dependencies` file.
22+
source "${KANI_DIR}/kani-dependencies"
23+
# Sanity check dependencies values.
24+
[[ "${CBMC_MAJOR}.${CBMC_MINOR}" == "${CBMC_VERSION%.*}" ]] || \
25+
(echo "Conflicting CBMC versions"; exit 1)
26+
[[ "${CBMC_VIEWER_MAJOR}.${CBMC_VIEWER_MINOR}" == "${CBMC_VIEWER_VERSION}" ]] || \
27+
(echo "Conflicting CBMC viewer versions"; exit 1)
28+
# Check if installed versions are correct.
29+
check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR}
30+
check-cbmc-viewer-version.py --major ${CBMC_VIEWER_MAJOR} --minor ${CBMC_VIEWER_MINOR}
2431
check_kissat_version.sh
2532

2633
# Formatting check

0 commit comments

Comments
 (0)