You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
* Add models for C library: getpwnam, getpwuid, and getopt by @tautschnig in https://github.com/diffblue/cbmc/pull/7919 and https://github.com/diffblue/cbmc/pull/7916
5
+
* Shadow memory addresses now also support --pointer-check argument by @esteffin in https://github.com/diffblue/cbmc/pull/7936
6
+
* [DOCS] Add documentation on CBMC Shadow Memory intrinsics and shadow memory functions (via doxygen) by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7913 and https://github.com/diffblue/cbmc/pull/7930
7
+
* [SYNTHESIZER] goto-synthesizer now accepts all CBMC options by @qinheping in https://github.com/diffblue/cbmc/pull/7900
8
+
9
+
## Bug Fixes
10
+
* Fix problem on array size L2 renaming by @esteffin in https://github.com/diffblue/cbmc/pull/7877
11
+
* Fix shadow memory missing aggregation on non-compound bitvector types by @esteffin in https://github.com/diffblue/cbmc/pull/7935
12
+
13
+
## Code Improvements
14
+
* Interval expressions: cleanup type hierarchy by @tautschnig in https://github.com/diffblue/cbmc/pull/7925
15
+
* Rename {min,max}_exprt to {min,max}_value_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/7931
16
+
* Introduce widen_if_needed by @kroening in https://github.com/diffblue/cbmc/pull/7938
17
+
* format_expr: format constants with natural number type by @kroening in https://github.com/diffblue/cbmc/pull/7940
18
+
* Enable passing struct tests under `regression/cbmc/` for new SMT backend by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7809
0 commit comments