From aa8920d45b239978174903c1c0edbdbca38a716a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 23 Sep 2024 10:30:41 +0000
Subject: [PATCH] Update to CBMC 6.3.1 and fix auto-update script

Update to CBMC release 6.3.1. This release includes a full fix for the
build problem that we carried a patch for (in #3431 and #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: #3507, #3536
---
 .github/workflows/cbmc-update.yml |  2 +
 kani-dependencies                 |  4 +-
 scripts/setup/al2/install_cbmc.sh | 74 -------------------------------
 3 files changed, 4 insertions(+), 76 deletions(-)

diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
index 7b63c0dae7de..3a215df04b3c 100644
--- a/.github/workflows/cbmc-update.yml
+++ b/.github/workflows/cbmc-update.yml
@@ -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
diff --git a/kani-dependencies b/kani-dependencies
index 421188a08762..6f844839086c 100644
--- a/kani-dependencies
+++ b/kani-dependencies
@@ -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"
diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh
index 3bac22ace3db..81c476dab440 100755
--- a/scripts/setup/al2/install_cbmc.sh
+++ b/scripts/setup/al2/install_cbmc.sh
@@ -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 \