From 62358f5f5a7ee726cc76a7cd64d6908ccae71deb Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 15 Feb 2023 18:18:11 +0000 Subject: [PATCH 1/4] Silence spurious maybe uninitialised warning --- src/goto-instrument/unwindset.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index eebd8c5682d..982cc51b1da 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/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(id, *thread_nr)] = uw; +#pragma GCC diagnostic pop + } else + { loop_map[id] = uw; + } } } From 9066460dbe73088e3df3c22cbef09157f58095d1 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 15 Feb 2023 18:20:36 +0000 Subject: [PATCH 2/4] Use immediately invoked lambda to avoid warning Pushing the warning exception is not a straight forward solution in this case. This is because gcc-12 still generates the warning on read of `contract` instead of on initialisation of `contract`. --- src/cprover/cprover_parse_options.cpp | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index feb0b811033..9dea190ee6b 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/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. -// This will likely go away once we use std::optional. -// 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 contract = cmdline.isset("contract") - ? irep_idt(cmdline.get_value("contract")) - : optionalt{}; -#pragma GCC diagnostic pop + // gcc produces a spurious warning for optionalt if initialised + // with ternary operator. Initialising with an immediately invoked lamda + // avoids this. + const auto contract = [&]() -> optionalt { + if(cmdline.isset("contract")) + return {cmdline.get_value("contract")}; + else + return {}; + }(); if(cmdline.isset("smt2") || cmdline.isset("text") || variable_encoding) { From 859ac17b701ba435aa2f936f4a2688d9b26ae9e3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 15 Feb 2023 18:21:15 +0000 Subject: [PATCH 3/4] Fix `function_may_throw` maybe uninitialised error with gcc-12 --- jbmc/src/java_bytecode/remove_exceptions.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index a83328fba8b..e745d0beaf8 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/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) { From bfb968bc9f3c3814c40dffe237ef75e78ec03fde Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 15 Feb 2023 18:21:06 +0000 Subject: [PATCH 4/4] Add check of gcc-12 to pull request checks --- .github/workflows/pull-request-checks.yaml | 53 ++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index eb8d0417fa5..4aedf85bde1 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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