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

Update CBMC version to 5.79 #2286

Closed
celinval opened this issue Mar 8, 2023 · 0 comments · Fixed by #2301
Closed

Update CBMC version to 5.79 #2286

celinval opened this issue Mar 8, 2023 · 0 comments · Fixed by #2301
Assignees
@tautschnig
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. T-CBMC Issue related to an existing CBMC issue

Comments

@celinval
Copy link
Contributor

celinval commented Mar 8, 2023 •
edited
Loading

Update CBMC version to 5.79 and re-enable the tests that were disabled here: #2149

In order to re-enable the tests, please rename the test folder and remove the ignored- prefix.
@celinval celinval added [C] Internal Tracks some internal work. I.e.: Users should not be affected. T-CBMC Issue related to an existing CBMC issue labels Mar 8, 2023
@tautschnig tautschnig mentioned this issue Mar 17, 2023
Merged
3 tasks
tautschnig added a commit to tautschnig/kani that referenced this issue Mar 17, 2023
@tautschnig @zhassan-aws
Update CBMC version to 5.79.0
07ba909 
- Re-enable tests that had to be disabled with the toolchain upgrade in
  model-checking#2149. Fixes model-checking#2286, fixes model-checking#2191.
- Do not generate non-NULL pointer constants. Together with the CBMC
  version update this avoids the need for an unwinding annotation in the
  mir-linker test. Fixes model-checking#1978.
- CBMC 5.79.0 ships simplifier improvements that enable constant
  propagation to avoid slow-down with the Display trait. Fixes model-checking#1996.
- CBMC 5.79.0 ships SMT back-end fixes. Fixes model-checking#2002.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
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. T-CBMC Issue related to an existing CBMC issue
Projects
No open projects
Kani 2023-03-27
Status: No status
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Update CBMC version to 5.79.0 tautschnig/kani
2 participants
@tautschnig @celinval