20231011 cbmc 5.94.0 #7948

TGWDB · 2023-10-11T14:36:34Z

PR for cbmc 5.94.0. Note that this is trialing including a CHANGELOG as discussed in #7907 .

The following have committed PRs and should review my editing of their PR title in the CHANGELOG to ensure I didn't mangle it: @thomasspriggs @peterschrammel @tautschnig @esteffin @NlightNFotis @qinheping @kroening

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

thomasspriggs · 2023-10-11T14:48:13Z

CHANGELOG

@@ -0,0 +1,22 @@
+## What's Changed
+* Increase support for unions in incremental smt2 decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7926


⛏️ I don't think we have added enough support for any union examples to work from a user perspective.

thomasspriggs · 2023-10-11T14:53:40Z

CHANGELOG

+* Rename {min,max}_exprt to {min,max}_value_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/7931
+* Introduce widen_if_needed by @kroening in https://github.com/diffblue/cbmc/pull/7938
+* format_expr: format constants with natural number type by @kroening in https://github.com/diffblue/cbmc/pull/7940
+* Enable all struct tests under `regression/cbmc/` for new SMT backend by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7809


⛏️ I suspect this is actually a misleadingly named PR, as we enabled the tests which pass only. There are at least some remaining to fix.

tautschnig

Thank you for introducing a changelog!

tautschnig · 2023-10-11T15:07:43Z

CHANGELOG

+* Fix problem on array size L2 renaming by @esteffin in https://github.com/diffblue/cbmc/pull/7877
+* Fix shadow memory missing aggregation on non-compound bitvector types by @esteffin in https://github.com/diffblue/cbmc/pull/7935
+
+## Internal Improvements


I suggest not even including this section, though perhaps those could be listed in the PR description for reviewers to potentially override whoever is putting together the PR. My personal take is that the changelog should strongly focus on observable changes, where "observable" are all those changes that impact users in the first instance and developers if there are substantial API changes.

tautschnig · 2023-10-11T15:08:09Z

CHANGELOG

@@ -0,0 +1,22 @@
+## What's Changed
+* Increase support for unions in incremental smt2 decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7926
+* Add ASV book CBMC examples by @peterschrammel in https://github.com/diffblue/cbmc/pull/7921


Not relevant to users.

tautschnig · 2023-10-11T15:08:59Z

CHANGELOG

+* [DOCS] Add documentation on CBMC Shadow Memory intrinsics by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7913
+* [DOCS] Improve doxygen for shadow_memory_util by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7930


I think those two items could be combined.

tautschnig · 2023-10-11T15:09:35Z

CHANGELOG

+* Shadow memory addresses now also support --pointer-check argument by @esteffin in https://github.com/diffblue/cbmc/pull/7936
+* [DOCS] Add documentation on CBMC Shadow Memory intrinsics by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7913
+* [DOCS] Improve doxygen for shadow_memory_util by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7930
+* [SYNTHESIZER] Allow goto-synthesizer accept all CBMC options  by @qinheping in https://github.com/diffblue/cbmc/pull/7900


I'd reword this as "goto-synthesizer now accepts all CBMC options by @qinheping ..."

tautschnig · 2023-10-11T15:11:49Z

CHANGELOG

@@ -0,0 +1,22 @@
+## What's Changed


Before that line we'll need a #-level heading that states the version that these changes are referring to.

codecov · 2023-10-11T15:24:20Z

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (cf380d5) 78.65% compared to head (95b7ac5) 78.62%.
Report is 3 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7948      +/-   ##
===========================================
- Coverage    78.65%   78.62%   -0.04%     
===========================================
  Files         1701     1701              
  Lines       196204   196204              
===========================================
- Hits        154328   154265      -63     
- Misses       41876    41939      +63

see 64 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

tautschnig · 2023-10-12T08:58:45Z

Could we please get #7954 into this release (i.e., hold off releasing until this is approved, and then rebase this release)?

Increment version number for cbmc 5.94.0

247c450

TGWDB requested review from a team, NlightNFotis, thomasspriggs, peterschrammel, esteffin, kroening and tautschnig as code owners October 11, 2023 14:36

thomasspriggs approved these changes Oct 11, 2023

View reviewed changes

tautschnig approved these changes Oct 11, 2023

View reviewed changes

esteffin approved these changes Oct 11, 2023

View reviewed changes

NlightNFotis approved these changes Oct 11, 2023

View reviewed changes

Add CHANGELOG with changes for cbmc 5.94.0

95b7ac5

TGWDB force-pushed the 20231011-cbmc-5.94.0 branch 2 times, most recently from 7bfb2ff to 95b7ac5 Compare October 11, 2023 22:55

TGWDB merged commit 2833356 into develop Oct 12, 2023

tautschnig deleted the 20231011-cbmc-5.94.0 branch October 17, 2023 13:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

20231011 cbmc 5.94.0 #7948

20231011 cbmc 5.94.0 #7948

TGWDB commented Oct 11, 2023

thomasspriggs Oct 11, 2023

thomasspriggs Oct 11, 2023

tautschnig left a comment

tautschnig Oct 11, 2023

tautschnig Oct 11, 2023

tautschnig Oct 11, 2023

tautschnig Oct 11, 2023

tautschnig Oct 11, 2023

codecov bot commented Oct 11, 2023 •

edited

Loading

tautschnig commented Oct 12, 2023

		@@ -0,0 +1,22 @@
		## What's Changed
		* Increase support for unions in incremental smt2 decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7926

		* [DOCS] Add documentation on CBMC Shadow Memory intrinsics by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7913
		* [DOCS] Improve doxygen for shadow_memory_util by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7930

20231011 cbmc 5.94.0 #7948

20231011 cbmc 5.94.0 #7948

Conversation

TGWDB commented Oct 11, 2023

thomasspriggs Oct 11, 2023

Choose a reason for hiding this comment

thomasspriggs Oct 11, 2023

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Oct 11, 2023

Choose a reason for hiding this comment

tautschnig Oct 11, 2023

Choose a reason for hiding this comment

tautschnig Oct 11, 2023

Choose a reason for hiding this comment

tautschnig Oct 11, 2023

Choose a reason for hiding this comment

tautschnig Oct 11, 2023

Choose a reason for hiding this comment

codecov bot commented Oct 11, 2023 • edited Loading

Codecov Report

tautschnig commented Oct 12, 2023

codecov bot commented Oct 11, 2023 •

edited

Loading