Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update to CBMC 6.3.1 and fix auto-update script #3537

Merged
merged 2 commits into from
Sep 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
# 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
Loading