Skip to content

Conversation

@graebm
Copy link
Contributor

@graebm graebm commented Jun 19, 2024

Issue:
The proofs broke unexpectedly when CBMC 6.0.0 was released, since we were using "latest". We pinned the version back to 5.95.1 in a recent PR to get CI working again.

Description of changes:

  • Upgrade to CBMC 6.0.0
    • For all tools used in proofs, stop using "latest". Pin the exact version, so we're not caught off-guard by unexpected upgrades again in the future
  • Fix proof code to work with CBMC 6

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Comment on lines +2 to +6
cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
cbmc-version: "6.0.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
cbmc-viewer-version: "3.8" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
kissat-tag: "rel-3.1.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you have any automation in place to be notified about available upgrades?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I signed the team account to be notified of new CBMC releases

@graebm graebm merged commit 957c760 into main Jun 19, 2024
@graebm graebm deleted the cmbc6 branch June 19, 2024 22:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants