Merge pull request #7542 from thomasspriggs/tas/gcc12

Fix building with gcc 12

Author: thomasspriggs

.github/workflows/pull-request-checks.yaml

@@ -365,6 +365,59 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 
+  # This job takes approximately 26 to 46 minutes
+  check-ubuntu-22_04-cmake-gcc-12:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-12 gdb g++-12 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-22.04-Release-gcc-12-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-22.04-Release-gcc-12-${{ github.ref }}
+            ${{ runner.os }}-22.04-Release-gcc-12
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc-12 -DCMAKE_CXX_COMPILER=/usr/bin/g++-12
+      - name: Check that doc task works
+        run: ninja -C build doc
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Check if package building works
+        run: |
+          cd build
+          ninja package
+          ls *.deb
+      - name: Run tests
+        run: cd build; ctest . -V -L CORE -j2
+
   # This job takes approximately 5 to 24 minutes
   check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
     runs-on: ubuntu-20.04

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -95,7 +95,7 @@ class remove_exceptionst
     message_handlert &_message_handler)
     : symbol_table(_symbol_table),
       class_hierarchy(_class_hierarchy),
-      function_may_throw(_function_may_throw),
+      function_may_throw(std::move(_function_may_throw)),
       remove_added_instanceof(_remove_added_instanceof),
       message_handler(_message_handler)
   {

src/cprover/cprover_parse_options.cpp

@@ -218,17 +218,15 @@ int cprover_parse_optionst::main()
       return CPROVER_EXIT_SUCCESS;
     }
 
-// gcc produces a spurious warning on optionalt<irep_idt>.
-// This will likely go away once we use std::optional<irep_idt>.
-// To make clang ignore the pragma, we need to guard it with an ifdef.
-#pragma GCC diagnostic push
-#ifndef __clang__
-#  pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
-#endif
-    optionalt<irep_idt> contract = cmdline.isset("contract")
-                                     ? irep_idt(cmdline.get_value("contract"))
-                                     : optionalt<irep_idt>{};
-#pragma GCC diagnostic pop
+    // gcc produces a spurious warning for optionalt<irep_idt> if initialised
+    // with ternary operator. Initialising with an immediately invoked lamda
+    // avoids this.
+    const auto contract = [&]() -> optionalt<irep_idt> {
+      if(cmdline.isset("contract"))
+        return {cmdline.get_value("contract")};
+      else
+        return {};
+    }();
 
     if(cmdline.isset("smt2") || cmdline.isset("text") || variable_encoding)
     {

src/goto-instrument/unwindset.cpp

@@ -172,9 +172,19 @@ void unwindsett::parse_unwindset_one_loop(
       uw = unsafe_string2unsigned(uw_string);
 
     if(thread_nr.has_value())
+    {
+// Work around spurious GCC 12 warning about thread_nr being uninitialised.
+#pragma GCC diagnostic push
+#ifndef __clang__
+#  pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+#endif
       thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;
+#pragma GCC diagnostic pop
+    }
     else
+    {
       loop_map[id] = uw;
+    }
   }
 }