Skip to content

Conversation

@tautschnig
Copy link
Member

Description of changes and resolved issues:

Call-outs:

n/a

Testing:

  • How is this change tested? CI runs.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • n/a Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

- 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 <[email protected]>
@tautschnig tautschnig requested a review from a team as a code owner March 17, 2023 15:45
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Thanks @tautschnig!

Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Awesome, thanks @tautschnig !

@tautschnig tautschnig merged commit 048b598 into model-checking:main Mar 17, 2023
@tautschnig tautschnig deleted the cbmc-5.79.0 branch March 17, 2023 16:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

3 participants