From d222f9a780b34472263d3c8202b0364e685b866f Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Tue, 2 Jan 2024 17:38:07 -0500 Subject: [PATCH] Build CBMC with `cmake` in all "CBMC latest" jobs (#2965) The "CBMC latest" workflow is composed of two jobs (`regression` and `perf`) which perform testing with the most recent development version of CBMC. At present, the `regression` jobs are not actually testing with the CBMC that we build from source, but the CBMC installed through the setup scripts, as revealed in #2954. This PR changes the `regression` jobs so that they use `cmake` to build. This allows the runner to pick up the recently-built CBMC development version instead of the one installed through setup scripts, as it's done in the `perf` jobs. Unfortunately, [this CI run](https://github.com/adpaco-aws/rmc/actions/runs/7390380572) doesn't demonstrate the fix as it should due to an unrelated breaking change in the latest CBMC version. However, #2952 provides more context in case you need it. --- .github/workflows/cbmc-latest.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 9cb8082ae4b7..e2a1f7a124f2 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -45,8 +45,8 @@ jobs: - name: Build CBMC working-directory: ./cbmc run: | - make -C src minisat2-download cadical-download - make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical + cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" + cmake --build build -- -j 4 # Prepend the bin directory to $PATH echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH