Skip to content

Commit d222f9a

Browse files
authored
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.
1 parent ee0ff7e commit d222f9a

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

.github/workflows/cbmc-latest.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,8 @@ jobs:
4545
- name: Build CBMC
4646
working-directory: ./cbmc
4747
run: |
48-
make -C src minisat2-download cadical-download
49-
make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
48+
cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
49+
cmake --build build -- -j 4
5050
# Prepend the bin directory to $PATH
5151
echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
5252

0 commit comments

Comments
 (0)