Build CBMC with cmake in all "CBMC latest" jobs
#2965
Conversation
There was a problem hiding this comment.
Apparently, the cmake build places all the binaries under build/bin, which is the directory that gets added to $GITHUB_PATH. On the other hand, the make build places each binary under its respective directory under src, e.g. cbmc is placed inside src/cbmc/, goto-cc is placed inside src/goto-cc/, etc.
Indeed, that's why the version we build from source isn't picked up in |
These are the auto-generated release notes for comparison purposes: ## What's Changed * Automate cargo update without dependabot by @tautschnig in #2942 * Update nightly toolchain to toolchain-2023-12-15 by @celinval in #2948 * Automatic cargo update to 2023-12-18 by @github-actions in #2951 * Migrate function, block and statement modules to StableMIR by @celinval in #2947 * Update Rust toolchain to `nightly-2023-12-18` by @adpaco-aws in #2953 * Update the rust toolchain to 2023-12-20 by @celinval in #2961 * Migrate foreign function, compiler-interface and kani-middle modules to use StableMIR by @celinval in #2959 * Build CBMC with `cmake` in all "CBMC latest" jobs by @adpaco-aws in #2965 * Automatic cargo update to 2024-01-01 by @github-actions in #2964 * Automatic cargo update to 2024-01-08 by @github-actions in #2968 * Upgrade to 2024-01-08 rust toolchain by @zhassan-aws in #2969 **Full Changelog**: kani-0.43.0...kani-0.44.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
The "CBMC latest" workflow is composed of two jobs (
regressionandperf) which perform testing with the most recent development version of CBMC. At present, theregressionjobs 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
regressionjobs so that they usecmaketo 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 theperfjobs. Unfortunately, this CI run 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.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.