forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathCHANGELOG
353 lines (318 loc) · 32.3 KB
/
CHANGELOG
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
# CBMC 6.2.0
## What's Changed
* Dynamic frames: do not add trivial properties by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8413
## Bug Fixes
* Contracts/dynamic frames: do not attempt to instrument typedefs by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8403
* Remove dynamic_cast from bv_dimacst by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8406
* Remove uses of `dynamic_cast` from qualifierst hierarchy by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8405
* Remove Java's unnecessary languaget::parse peculiarity by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8407
* Solver factory: set_decision_procedure_time_limit does not require dynamic_cast by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8409
* Solver factory: make_satcheck_prop does not require dynamic_cast by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8410
* Solver factory: all solvers are stack_decision_proceduret by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8408
* Remove qualifierst by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8419
* Contracts (DFCC) regression tests: use CaDiCaL by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8414
* Library functions: mark them as compiled by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8412
* Maintain loop invariant annotation when converting do .. while by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8417
* CONTRACTS: redirect checks to outer write set for loops that get skipped by @remi-delmas-3000 in /~https://github.com/diffblue/cbmc/pull/8416
* CONTRACTS: fix do while latch by @remi-delmas-3000 in /~https://github.com/diffblue/cbmc/pull/8420
* Remove dynamic_cast from counterexample beautification code path by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8421
* Include <cstdint> for int64_t by @ismaell in /~https://github.com/diffblue/cbmc/pull/8426
* SMT2 back-end: fix inconsistent array flattening by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8400
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-6.1.1...cbmc-6.2.0
# CBMC 6.1.1
## What's Changed
* Compile CaDiCaL with -DNDEBUG by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8397
## Bug Fixes
* Enable higher verbosity for benchmarking by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8395
* CI jobs: upgrade CVC5 from 1.0.0 to 1.1.2 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8383
* implement flattening for +/- for the range type by @kroening in /~https://github.com/diffblue/cbmc/pull/8396
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-6.1.0...cbmc-6.1.1
# CBMC 6.1.0
## What's Changed
* Add support for building with GCC 14 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8368
* Add documentation to loop contracts, __CPROVER_loop_entry by @QinyuanWu in /~https://github.com/diffblue/cbmc/pull/8377
* [CONTRACTS] Check side effect of loop contracts during instrumentation by @qinheping in /~https://github.com/diffblue/cbmc/pull/8360
* GOTO conversion: create temporaries with minimal scope by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8363
## Bug Fixes
* [CONTRACTS] Use unified loop contract config by @qinheping in /~https://github.com/diffblue/cbmc/pull/8356
* Replace expired key for signing the MSI Installer by @JohnLBergqvist in /~https://github.com/diffblue/cbmc/pull/8364
* [CONTRACTS] Add loop-contract symbols into symbol table during typecheck by @qinheping in /~https://github.com/diffblue/cbmc/pull/8359
* C library: __fcntl_time64 for Debian/ARM by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8371
* Bump Homebrew/git-user-config version to avoid deprecation warnings by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8341
* Refactor Codecov CI job by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8339
* Regression cleanup: don't repeatedly remove the same file by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8369
* Purge winbug from regression tests by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7857
* Make sure free symbols are declared in SMT2_conv after quantifier rewriting by @qinheping in /~https://github.com/diffblue/cbmc/pull/8361
* Regression test: support big and little endian by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8370
* Fix multiplication and division of complex numbers by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8376
* Update Xen integration test Docker image by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8381
* SMT2 back-end: detect when solver returns unexpected model by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8379
* SMT2 back-end: Bitwuzla does not support lambda expressions by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8387
* C front-end: place requires and ensures in designated scope by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8380
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-6.0.1...cbmc-6.1.0
# CBMC 6.0.1
## Bug Fixes
* Fix Python syntax error by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8344
* Use GNU parallel in Windows CI job by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8345
* goto-synthesizer: ignore __CPROVER_-prefixed symbols by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8348
* Union member fix by @kroening in /~https://github.com/diffblue/cbmc/pull/8347
* GOTO conversion: Declaration hops must not invalidate incomplete gotos by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8349
* Increase Windows/clcache size to 2 GB by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8346
* homebrew-pr CI notification: install go by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8340
* add two helpers for bv_typet by @kroening in /~https://github.com/diffblue/cbmc/pull/8350
* reduce default verbosity of cprover binary by @kroening in /~https://github.com/diffblue/cbmc/pull/8352
* reduce verbosity of runtime messages by @kroening in /~https://github.com/diffblue/cbmc/pull/8354
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-6.0.0...cbmc-6.0.1
# CBMC 6.0.0
## Major Changes
* Change C++ version to C++17 by @esteffin in /~https://github.com/diffblue/cbmc/pull/7989
* Enable default analysis flags for CBMC version 6.0+ by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8093
* Add support for a `--no-unwinding-assertions` flag by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8109
* Use malloc fail null by default by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8101
* introduce 'fatal assertions' by @kroening in /~https://github.com/diffblue/cbmc/pull/8226
* Permit re-setting --object-bits by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7858
* goto-instrument/unwinding: enable unwinding assertions by default by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8274
* JBMC: enable unwinding assertions by default by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8273
* generate assert(false) when calling undefined function by @kroening in /~https://github.com/diffblue/cbmc/pull/8292
* change default verbosity to M_STATUS by @kroening in /~https://github.com/diffblue/cbmc/pull/8331
## What's Changed
* Add support for union values in traces for incremental smt2 decision procedure by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/7990
* Variables leaving scope on jumping should always be marked dead by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8092
* Define coverage blocks so as to be terminated by assumptions by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/7810
* Build and infrastructure fixes for FreeBSD by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7924
* Add support for variables entering scope via a goto by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8091
* Remove JSIL front-end by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8158
* Compact propositional encoding of OBJECT_SIZE(ptr) by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7702
* C front-end: refuse duplicate declaration of local variable by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8160
* CMake builds: support system-installed CaDiCaL by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8159
* division-by-zero on float by @kroening in /~https://github.com/diffblue/cbmc/pull/8233
* Avoid duplicate "warning:" or "error:" output by @tautschnig in /~https://github.com/diffblue/cbmc/pull/1359
* add support for loongarch64 by @wuruilong01 in /~https://github.com/diffblue/cbmc/pull/8266
* Add support for GNU Hurd by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8211
* `__CPROVER_bool` should not have a memory layout by @kroening in /~https://github.com/diffblue/cbmc/pull/8325
* add `emscripten` architecture by @kroening in /~https://github.com/diffblue/cbmc/pull/8334
* increase verbosity of warning about missing `__builtin_` declaration by @kroening in /~https://github.com/diffblue/cbmc/pull/8333
* increase verbosity level of various messages by @kroening in /~https://github.com/diffblue/cbmc/pull/8330
## Bug Fixes
* Add CODEOWNERS for CHANGELOG by @TGWDB in /~https://github.com/diffblue/cbmc/pull/7988
* typecheckt::errort by @kroening in /~https://github.com/diffblue/cbmc/pull/7982
* string_constantt typing by @kroening in /~https://github.com/diffblue/cbmc/pull/7965
* remove index_type() by @kroening in /~https://github.com/diffblue/cbmc/pull/7992
* add a 'language feature' detection facility for goto programs by @kroening in /~https://github.com/diffblue/cbmc/pull/7771
* Fix line-number output in document-properties-* by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7994
* CODING_STANDARD.md: fix references to clang-format by @kroening in /~https://github.com/diffblue/cbmc/pull/7995
* Use simplify_exprtt::resultt in pre-order simplification steps by @tautschnig in /~https://github.com/diffblue/cbmc/pull/6118
* CBMC version 6 release process changes by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/7987
* Remove useless steps from Rust CI pipeline by @esteffin in /~https://github.com/diffblue/cbmc/pull/8030
* Replace `new-smt-backend` tag with inverted `no-new-smt` tag by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8002
* Remove local declaration of void_t by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8031
* [CI] Minor fixes to CI accompanying C++17 version change by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8028
* Refactor `smt_function_application_termt::indices` using C++17 feature by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8035
* Restore post-order simplification of byte_extract(c ? a : b, ...) by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8005
* Replace usage of `std::result_of` with `std::invoke_result` by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8037
* Fix the invariant message for unimplemented SMT count trailing zeros conversion. by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8044
* Fix test_struct_union_c regression test by @esteffin in /~https://github.com/diffblue/cbmc/pull/8046
* DFCC instrumentation: ensure programs are well-formed by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8045
* Fix failed coverage in if then else with return statements by @esteffin in /~https://github.com/diffblue/cbmc/pull/8001
* Make -Wno-maybe-uninitialized the default with GCC by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8047
* Enable all `cbmc` regression tests that are passing to run with new SMT backend by @esteffin in /~https://github.com/diffblue/cbmc/pull/8051
* C library check: do not warn about the need for MMX by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8050
* Use the C++17 standard `[[nodiscard]]` attribute directly by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8036
* SYNTHESIZER: Add quick filter into goto-synthesizer by @qinheping in /~https://github.com/diffblue/cbmc/pull/7973
* fix conversions between long and long long by @kroening in /~https://github.com/diffblue/cbmc/pull/8086
* The emscripten compiler has alloca.h by @kroening in /~https://github.com/diffblue/cbmc/pull/8085
* Add default codeowners to `/src/symtab2gb/` and `/src/json-symtab-language/` by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8087
* Remove util_make_unique by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8032
* Run additional regressions with new SMT solver by @esteffin in /~https://github.com/diffblue/cbmc/pull/8084
* Use the STL versions of `variant` and `optional` in incremental smt2 decision procedure by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8089
* Remove usages of the deprecated `std::iterator` by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8088
* Replace nonstd::optional by C++17 std::optional by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8034
* [CI] Perform apt update to sync repo sources before trying to install from them. by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8090
* Dynamic frames: don't instrument __CPROVER_allocated_memory by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8094
* languaget is not a messaget [blocks: #3800] by @tautschnig in /~https://github.com/diffblue/cbmc/pull/4050
* Name `-paths-lifo` test profiles uniquely by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8097
* Keep symbols as nondet rather than using their symbol table values in SMT decision procedure. by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8104
* CSmith test script: avoid a need for argv modelling by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8105
* Assignments to bit-fields yield results of bit-field type by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8082
* Make componentt::{base,pretty}_name comments by @tautschnig in /~https://github.com/diffblue/cbmc/pull/5815
* Refactor `string_constantt::get_value` and `string_constantt::set_value` call sites. by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/7999
* Remove all references to optionalt by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8099
* Remove default messaget value from goto_program_dereferencet by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8100
* Replace file_util.{h,cpp} by std::filesystem by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8033
* Cleanup USE_STD_STRING/USE_DSTRING configuration option by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8040
* Enable dependabot to update GitHub actions by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8115
* fix nondeterministic hex_trace test by @kroening in /~https://github.com/diffblue/cbmc/pull/8121
* Add Michael and Peter to Repository CI codeowners. by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8114
* Bump actions/checkout from 3 to 4 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8117
* Bump actions/upload-artifact from 3 to 4 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8119
* Bump github/codeql-action from 2 to 3 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8120
* decision_proceduret API with assumptions by @kroening in /~https://github.com/diffblue/cbmc/pull/7979
* simplify prop_conv_solvert::push by @kroening in /~https://github.com/diffblue/cbmc/pull/8122
* JSIL: create messaget with a message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8125
* Remove unused `log` member from dfcc_is_freeablet by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8124
* Remove unused safety_checkert constructor by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8126
* Permit constructing parsert with a message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8134
* jsil_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8136
* Add a document outlining the current release process by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8130
* java_bytecode_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8140
* [CI] Bring back core release processes by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8108
* Run again tests with new default checks by @esteffin in /~https://github.com/diffblue/cbmc/pull/8106
* cbmc preprocessing: call set_language_options after checking for null by @kroening in /~https://github.com/diffblue/cbmc/pull/8149
* dstringt::starts_with can be const by @kroening in /~https://github.com/diffblue/cbmc/pull/8148
* unary_exprt::check and nullary_exprt::check by @kroening in /~https://github.com/diffblue/cbmc/pull/8151
* Bump jungwinter/split from 1 to 2 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8118
* json_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8137
* Fix document publishing GitHub Action by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8152
* CSmith GitHub action: run apt-get update by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8155
* C++ front-end: configure C++11+ syntax without ansi_c_parser object by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8132
* JSIL front-end: no need for parser reentrancy by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8153
* Conversion check: fix off-by-one error for float-to-unsigned by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8157
* Reduce Thomas and Fotis code ownership by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/8162
* Bump actions/cache from 3 to 4 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8164
* Remove non-existent user from CODEOWNERS by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8166
* Code contracts: do not interleave checking and instrumenting by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8095
* Linking: only rename file-local symbols by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8167
* C front-end: GCC >= 12 support __builtin_shufflevector by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8170
* Make ansi_c_internal_additions independent of the parser object by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8133
* cbmc-cover/pointer-function-parameters test: negative numbers are ok by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8177
* remove_returns: do not lose location numbers by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8178
* MMIO instrumentation cleanup by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8175
* argc/argv modelling: argument string must remain in scope by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8174
* Bump microsoft/setup-msbuild from 1 to 2 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8184
* update_bits_exprt by @kroening in /~https://github.com/diffblue/cbmc/pull/8182
* SMT2: fix extractbit with non-const index by @kroening in /~https://github.com/diffblue/cbmc/pull/8180
* Support Minisat source variants where l_False/l_True are not macros by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8107
* Full slicing always requires consistent location numbers by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8179
* Remove support for irep_idt-as-std::string by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8154
* Scope tree: fix and clarify comment by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8188
* Scope tree: add dot output by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8189
* assembler_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8139
* relax bitvector constant check for Verilog bitvectors by @kroening in /~https://github.com/diffblue/cbmc/pull/8191
* Use dstringt::starts_with by @kroening in /~https://github.com/diffblue/cbmc/pull/8150
* add a fluent-style typet::with_source_location by @kroening in /~https://github.com/diffblue/cbmc/pull/8194
* SMT2: simplify interface by @kroening in /~https://github.com/diffblue/cbmc/pull/8123
* introduce `update_bit_exprt` by @kroening in /~https://github.com/diffblue/cbmc/pull/8190
* Fix gitignore of goto-bmc by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8197
* Fix `missing braces around initializer` GCC warning by @remi-delmas-3000 in /~https://github.com/diffblue/cbmc/pull/8198
* C library: ASM functions take void* pointers by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7932
* C library: additional floating-point functions and cleanup by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8195
* array_set: do not fail upon an invalid (void) pointer by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8202
* Avoid cross-platform preprocessor need from test by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8206
* Make tests pass when char is unsigned by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8212
* Deprecate namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8209
* C library: model __builtin_powi{,f,l} by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8192
* Avoid 64-bit platform support requirement for running tests by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8213
* Make exprt::with_source_location type safe by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8216
* Remove unused goto_convertt::has_function_call by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8201
* C++ front-end: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8227
* Add missing source locations by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7856
* Static initialisation: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8221
* miniBDD test: support lselect by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8240
* nondet-volatile: fix handling of enum types by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8203
* C/C++ front-end: accept all floating-point extensions that GCC and Clang support by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8169
* statement_list_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8138
* Support __builtin_dynamic_object_size by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8156
* xml_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8135
* ansi_c_parsert: construct with message handler by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8141
* C/C++ front-end: Revert scanner re-entrancy by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8245
* Improve printf formatter by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8205
* Run performance comparison in CI using Kani's Benchcomp by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8171
* Add namespacet::follow_struct_union_tag to simplify follow_tag uses by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8248
* Rename follow_struct_or_union_tag to follow_tag by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8251
* Visual Studio: fix feraiseexcept test failure by @kroening in /~https://github.com/diffblue/cbmc/pull/8232
* Move benchcomp YAML file to avoid spurious GitHub errors by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8250
* test.pl now reports both directory and descriptor file name by @kroening in /~https://github.com/diffblue/cbmc/pull/8252
* Remove parsert::clear and all of its overrides by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8244
* util: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8236
* goto-analyzer.md: fix typos in examples by @rurban in /~https://github.com/diffblue/cbmc/pull/8255
* goto-programs: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8230
* goto-instrument: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8229
* Add invariant that multiplication uses operands of the same size by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8241
* `format_expr` can now print range-typed constants by @kroening in /~https://github.com/diffblue/cbmc/pull/8259
* Bump codecov/codecov-action from 3 to 4 by @dependabot in /~https://github.com/diffblue/cbmc/pull/8183
* C library: model asprintf, test {v,}asprintf by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8237
* C library: implement {v,}snprintf by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8239
* C library: implement {v,}dprintf by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8238
* C front-end: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8218
* initialisation of `_Complex` with an initializer list by @kroening in /~https://github.com/diffblue/cbmc/pull/8265
* C library: provide implementations of fopen64, freopen64 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8267
* C library: add __time64 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8268
* C library: add mmap64 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8269
* Remove unanchored "error" string from symtab2gb test specs by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8270
* C library: add creat, open, openat by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8271
* simplify `extractbits_exprt` representation by @kroening in /~https://github.com/diffblue/cbmc/pull/8246
* analyses: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8215
* goto-harness: remove use of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8220
* Pointer analysis: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8231
* Move goto_convert files by @kroening in /~https://github.com/diffblue/cbmc/pull/8253
* JBMC: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8210
* Solvers: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8235
* C library: add __to{lower,upper} as alternative names for {tolower,toupper} by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8283
* C++ front-end: permit GCC attributes in using declarations by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8286
* C++ front-end: support [[__nodiscard__]] and [[nodiscard]] by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8287
* C++ front-end: fix parentheses matching for alignas parsing by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8288
* cbmc-cpp/Array4 test now works by @kroening in /~https://github.com/diffblue/cbmc/pull/8293
* Visual Studio has added _Static_assert by @kroening in /~https://github.com/diffblue/cbmc/pull/8294
* C++ front-end: not all declarators are code-typed by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8290
* [CONTRACTS] Refactor quantified symbol detection for loop contracts by @qinheping in /~https://github.com/diffblue/cbmc/pull/8299
* C++ front-end: support attributes with tag-less structs by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8289
* introduce `literal_vector_exprt` by @kroening in /~https://github.com/diffblue/cbmc/pull/8307
* help: add missing newline by @kroening in /~https://github.com/diffblue/cbmc/pull/8306
* `goto_check_ct::add_guarded_property` now has `is_fatal` parameter by @kroening in /~https://github.com/diffblue/cbmc/pull/8297
* Make `going_to` variable cprover-prefixed by @qinheping in /~https://github.com/diffblue/cbmc/pull/8312
* [CONTRACTS] Use fresh converter in loop contracts instrumentation by @qinheping in /~https://github.com/diffblue/cbmc/pull/8282
* [CONTRACTS] Ignore cprover symbols in loop assigns inference by @qinheping in /~https://github.com/diffblue/cbmc/pull/8313
* C++ front-end: fix parsing of >> as closing template args by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8291
* Lower-byte-operators: bv_to_expr should support bool target type by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8318
* Add support for __fp16 where appropriate by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8323
* Fix typos in release workflow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8322
* mod-by-zero is now fatal by @kroening in /~https://github.com/diffblue/cbmc/pull/8315
* Undefined shifts are now fatal by @kroening in /~https://github.com/diffblue/cbmc/pull/8304
* array-bounds checks are now fatal by @kroening in /~https://github.com/diffblue/cbmc/pull/8314
* Simplifier: c_bool (and others) are also bitvector types by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8247
* Delete `string_constantt::get_value` and `string_constantt::set_value` functions by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/8003
* Remove deprecated messaget() constructor by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8143
* Move GCC-13 CI job to Ubuntu 24.04 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8320
* Make DFCC is_dead_object_update less restrictive by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8261
* pointer checks are now fatal by @kroening in /~https://github.com/diffblue/cbmc/pull/8316
* Expand list of known compiler built-ins by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8321
* CMake: use find_program() to look for bash by @guijan in /~https://github.com/diffblue/cbmc/pull/8285
* Switch GitHub CI jobs from macos-11 to macos-13 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8328
* Use all 4 vCPUs on GitHub-hosted runners by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8327
* Goto crossing scopes: fix scope tree entry of conditions by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8187
* Declutter linking implementation by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8168
* Avoid brew symlink conflict in macos-13 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8338
* [CONTRACTS] Allow loop contracts annotated to goto statement by @qinheping in /~https://github.com/diffblue/cbmc/pull/8281
* cprover: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8219
* goto-symex: Replace uses of namespacet::follow by @tautschnig in /~https://github.com/diffblue/cbmc/pull/8222
* C front-end: typecheck conditional operator over string literal and 0 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7946
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-5.95.1...cbmc-6.0.0
# CBMC 5.95.1
## What's Changed
* Multiplication encoding: cleanup, Dadda, data by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7984
## Bug Fixes
* Remove extraneous y parameter from calls to exp and logl by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/7985
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-5.95.0...cbmc-5.95.1
## CBMC 5.95.0
### What's Changed
* Add C front-end support for vector expressions as compile-time constants by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7947
* C library: add exp, log, pow models by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7906
### Bug Fixes
* Fix bug with std::sort requires strict weak ordering by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7956
* SYNTHESIZER: Use only symbols from the original goto as terminals by @qinheping in /~https://github.com/diffblue/cbmc/pull/7970
* Add missing lowering of symbol values in new SMT backend by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/7952
* Restrict memory-analyzer build to Linux x86_64/i386 by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7958
* Add support for empty unions in incremental SMT decision procedure by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/7966
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-5.94.0...cbmc-5.95.0
## CBMC 5.94.0
### What's Changed
* 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
* 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 and shadow memory functions (via doxygen) by @NlightNFotis in /~https://github.com/diffblue/cbmc/pull/7913 and /~https://github.com/diffblue/cbmc/pull/7930
* [SYNTHESIZER] goto-synthesizer now accepts all CBMC options by @qinheping in /~https://github.com/diffblue/cbmc/pull/7900
### Bug Fixes
* 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
* Fix SMT encoding of structs which contain a single struct field by @thomasspriggs in /~https://github.com/diffblue/cbmc/pull/7951
* Fix simplification towards singleton intervals not checking application to only a single variable by @tautschnig in /~https://github.com/diffblue/cbmc/pull/7954
**Full Changelog**: /~https://github.com/diffblue/cbmc/compare/cbmc-5.93.0...cbmc-5.94.0