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 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) { 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) { 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; + } } }