Update CBMC build instructions for Amazon Linux 2 (#3431)

The default compiler on Amazon Linux 2 is GCC 7, which is not
sufficiently recent for building CBMC v6+. Install and use GCC 10,
adjust warnings to cope with the flex version provided by Amazon Linux
2, and handle the non-default std::filesystem support. Furthermore,
apply a workaround until diffblue/cbmc#8357
has been fixed on the CBMC side.

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

scripts/setup/al2/install_cbmc.sh

@@ -21,10 +21,83 @@ git clone \
 
 pushd "${WORK_DIR}"
 
-mkdir build
-git submodule update --init
+# 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)
 
-cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
+ (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
+
+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 \
+ -DCMAKE_CXX_FLAGS=-Wno-error=register
 cmake3 --build build -- -j$(nproc)
 sudo make -C build install
 

scripts/setup/al2/install_deps.sh

@@ -11,6 +11,7 @@ set -eu
 DEPS=(
  cmake
  cmake3
+ gcc10-c++
  git
  openssl-devel
  python3-pip