Merge pull request #8719 from tautschnig/bsd-actions

Update *BSD CI actions to the latest OS versions

Author: tautschnig

.github/workflows/bsd.yaml

@@ -18,18 +18,18 @@ jobs:
         with:
           save-always: true
           path: .ccache
-          key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          key: freebsd-15.0-gmake-${{ github.ref }}-${{ github.sha }}-PR
           restore-keys: |
-            freebsd-13.2-gmake-${{ github.ref }}
-            freebsd-13.2-gmake
+            freebsd-15.0-gmake-${{ github.ref }}
+            freebsd-15.0-gmake
       - name: ccache environment
         run: |
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Build and Test
         uses: vmactions/freebsd-vm@v1
         with:
-          release: 13.2
+          release: "15.0"
           usesh: true
           run: |
             # apparently fail-on-error isn't the default here
@@ -49,7 +49,10 @@ jobs:
             gmake -C src -j2 CXX="ccache clang++"
             # gmake -C jbmc/src setup-submodules
             # gmake -C jbmc/src -j2 CXX="ccache clang++"
-            gmake -C unit "CXX=ccache clang++"
+            # https://github.com/catchorg/Catch2/issues/2910 is an issue
+            # specific to Clang/LLVM 19 (which is what FreeBSD 15 ships)
+            gmake -C unit "CXX=ccache clang++" \
+              CXXFLAGS="-Wall -pedantic -Werror -Wswitch-enum -Wno-deprecated-declarations -Wno-c++20-extensions"
             # gmake -C jbmc/unit "CXX=ccache clang++"
             echo "Print ccache stats"
             ccache -s
@@ -80,18 +83,18 @@ jobs:
         with:
           save-always: true
           path: .ccache
-          key: openbsd-7.6-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          key: openbsd-7.7-gmake-${{ github.ref }}-${{ github.sha }}-PR
           restore-keys: |
-            openbsd-7.6-gmake-${{ github.ref }}
-            openbsd-7.6-gmake
+            openbsd-7.7-gmake-${{ github.ref }}
+            openbsd-7.7-gmake
       - name: ccache environment
         run: |
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Build and Test
         uses: vmactions/openbsd-vm@v1
         with:
-          release: 7.6
+          release: "7.7"
           run: |
             # apparently fail-on-error isn't the default here
             set -e -x
@@ -142,23 +145,23 @@ jobs:
         with:
           save-always: true
           path: .ccache
-          key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          key: netbsd-10.1-gmake-${{ github.ref }}-${{ github.sha }}-PR
           restore-keys: |
-            netbsd-9.3-gmake-${{ github.ref }}
-            netbsd-9.3-gmake
+            netbsd-10.1-gmake-${{ github.ref }}
+            netbsd-10.1-gmake
       - name: ccache environment
         run: |
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Build and Test
         uses: vmactions/netbsd-vm@v1
         with:
-          release: 9.3
+          release: "10.1"
           run: |
             # apparently fail-on-error isn't the default here
             set -e -x
             echo "Fetch dependencies"
-            pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10
+            pkg_add -v gmake git python311 patch flex bison ccache parallel z3 gcc10
             ln -s $(which python3.11) /usr/pkg/bin/python3
             export PATH=/usr/pkg/gcc10/bin:$PATH
             echo "Fetch JBMC dependencies"

COMPILING.md

@@ -12,11 +12,8 @@ integration system. It separately tests both the CMake build system and the
 hand-written make files. The latest build steps being used in CI can be
 [found here](https://github.com/diffblue/cbmc/blob/develop/.github/workflows/pull-request-checks.yaml).
 
-The environments below have been used successfully in the
-past, but are not actively tested:
-
-- Solaris 11
-- FreeBSD 13
+The Solaris 11 environment below has been used successfully in the past, but is
+not actively tested.
 
 # Building using CMake
 

regression/cbmc/gcc_vector3/main.c

@@ -42,7 +42,14 @@ void test_shufflevector(void)
 
   vector_u res;
 
+#  if defined(__clang__)
+  // None of the indices refers to the second vector, so we can safely make it
+  // non-deterministic.
+  res.v = __builtin_shufflevector(
+    a, __builtin_nondeterministic_value(a), 0, 1, -1, 3);
+#  else
   res.v = __builtin_shufflevector(a, a, 0, 1, -1, 3);
+#  endif
   assert(res.members[0] == 1);
   assert(res.members[1] == 2);
   // res.members[2] is "don't care"

src/ansi-c/c_typecheck_expr.cpp

@@ -2183,6 +2183,30 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
+      else if(
+        identifier == "__builtin_nondeterministic_value" &&
+        config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
+      {
+        // From Clang's documentation:
+        // Each call to __builtin_nondeterministic_value returns a valid value
+        // of the type given by the argument.
+        // Clang only supports integer types, floating-point types, vector
+        // types.
+        if(expr.arguments().size() != 1)
+        {
+          error().source_location = f_op.source_location();
+          error() << "__builtin_nondeterministic_value expects one operand"
+                  << eom;
+          throw 0;
+        }
+        typecheck_expr(expr.arguments().front());
+
+        side_effect_expr_nondett result{
+          expr.arguments().front().type(), f_op.source_location()};
+        expr.swap(result);
+
+        return;
+      }
       else if(
         identifier == "__builtin_shuffle" &&
         config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)