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

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

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

.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

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"

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 \