Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Nightly CBMC jobs fail due to goto-cc version mismatch #2952

Closed
adpaco-aws opened this issue Dec 18, 2023 · 2 comments · Fixed by #2995
Closed

Nightly CBMC jobs fail due to goto-cc version mismatch #2952

adpaco-aws opened this issue Dec 18, 2023 · 2 comments · Fixed by #2995
Assignees
@tautschnig
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@adpaco-aws
Copy link
Contributor

The nightly CBMC jobs attempt to build and run the perf suite with the latest CBMC versions. Unfortunately, it looks like these jobs have been failing over the weekend as in this run:

The input was compiled with an old version of goto-cc; please recompile
error: goto-cc exited with status exit status: 1
@adpaco-aws adpaco-aws added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Dec 18, 2023
@adpaco-aws adpaco-aws self-assigned this Dec 18, 2023
@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Dec 18, 2023 •
edited
Loading

Oddly enough, the standard regression jobs with the latest CBMC are passing, see this run for example. The two differences I can see between these jobs are:

  1. How CBMC is built (one job uses cmake while the other does regular make).
  2. How Kani is built (one job uses the development version and the other one does --release).

I'll check if either is the root cause of these failures.

@adpaco-aws
Copy link
Contributor Author

Ok, it looks like using cmake instead of regular make... makes a difference 🥁😄

This action run shows how the perf job passes if we just use make as in the regression jobs.

@adpaco-aws adpaco-aws mentioned this issue Dec 18, 2023
Closed
@adpaco-aws adpaco-aws mentioned this issue Jan 2, 2024
Merged
adpaco-aws added a commit that referenced this issue Jan 2, 2024
@adpaco-aws
Build CBMC with cmake in all "CBMC latest" jobs (#2965)
d222f9a 
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.
@tautschnig tautschnig mentioned this issue Jan 11, 2024
Closed
@tautschnig tautschnig mentioned this issue Feb 6, 2024
Merged
@adpaco-aws adpaco-aws assigned tautschnig and unassigned adpaco-aws Jul 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Milestone
No milestone
2 participants
@tautschnig @adpaco-aws