Skip to content

Commit

Permalink
Update to CBMC 6.3.1 and fix auto-update script
Browse files Browse the repository at this point in the history
Update to CBMC release 6.3.1. This release includes a full fix for the
build problem that we carried a patch for (in model-checking#3431 and model-checking#3436), thus
dropping the patching step.

The automatic update of CBMC requires actually installing that newer
version of CBMC, else regression tests fail as seen in
https://github.com/model-checking/kani/actions/runs/10987766383/job/30503118786.

Resolves: model-checking#3507, model-checking#3536
  • Loading branch information
tautschnig committed Sep 23, 2024
1 parent bb241de commit aa8920d
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 76 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/cbmc-update.yml
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,8 @@ jobs:
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
# install the newer CBMC version
scripts/setup/ubuntu/install_cbmc.sh
if ! ./scripts/kani-regression.sh ; then
echo "next_step=create_issue" >> $GITHUB_ENV
else
Expand Down
4 changes: 2 additions & 2 deletions kani-dependencies
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CBMC_MAJOR="6"
CBMC_MINOR="1"
CBMC_VERSION="6.1.1"
CBMC_MINOR="3"
CBMC_VERSION="6.3.1"

# If you update this version number, remember to bump it in `src/setup.rs` too
CBMC_VIEWER_MAJOR="3"
Expand Down
74 changes: 0 additions & 74 deletions scripts/setup/al2/install_cbmc.sh
Original file line number Diff line number Diff line change
Expand Up @@ -21,80 +21,6 @@ git clone \

pushd "${WORK_DIR}"

# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is
# properly fixed in CBMC
cat > varargs.patch << "EOF"
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
- __CPROVER_OBJECT_SIZE(arg))
+ __CPROVER_OBJECT_SIZE(*(void **)&arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
- __CPROVER_OBJECT_SIZE(args))
+ __CPROVER_OBJECT_SIZE(*(void **)&args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
- __CPROVER_OBJECT_SIZE(arg))
+ __CPROVER_OBJECT_SIZE(*(void **)&arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
- __CPROVER_OBJECT_SIZE(args))
+ __CPROVER_OBJECT_SIZE(*(void **)&args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
(void)*fmt;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
- __CPROVER_OBJECT_SIZE(ap))
+ __CPROVER_OBJECT_SIZE(*(void **)&ap))
{
(void)va_arg(ap, int);
__CPROVER_precondition(
- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
"vsnprintf object overlap");
}
@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk(
(void)*fmt;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
- __CPROVER_OBJECT_SIZE(ap))
+ __CPROVER_OBJECT_SIZE(*(void **)&ap))
{
(void)va_arg(ap, int);
__CPROVER_precondition(
- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
"vsnprintf object overlap");
}
EOF
patch -p1 < varargs.patch

cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
-DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \
-DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
Expand Down

0 comments on commit aa8920d

Please sign in to comment.