-
Notifications
You must be signed in to change notification settings - Fork 269
/
Copy pathCHANGELOG
434 lines (381 loc) · 38.1 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
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
# CBMC 6.4.1
This patch release addresses a hard-coding of C semantics in the back-end for pointer subtraction (via #8497).
## Bug Fixes
* fix `update_bit` lowering by @kroening in https://github.com/diffblue/cbmc/pull/8496
* Pointer subtraction in back-end: no need for bounds checking by @tautschnig in https://github.com/diffblue/cbmc/pull/8497
* remove duplicate SATCHECK_* defines by @kroening in https://github.com/diffblue/cbmc/pull/8501
* simplify bitxnor by @kroening in https://github.com/diffblue/cbmc/pull/8506
* Reword documentation of __CPROVER_{r,w,rw}_ok by @tautschnig in https://github.com/diffblue/cbmc/pull/8472
* simplify x^0 and x^1 by @kroening in https://github.com/diffblue/cbmc/pull/8509
* add multi-ary constructor for `mult_exprt` by @kroening in https://github.com/diffblue/cbmc/pull/8510
* Format bit-vectors with `[` ... `]` vector notation by @kroening in https://github.com/diffblue/cbmc/pull/8514
* add range_type to `from_integer`/`to_integer` by @kroening in https://github.com/diffblue/cbmc/pull/8520
* Bump codecov/codecov-action from 4 to 5 by @dependabot in https://github.com/diffblue/cbmc/pull/8507
* CONTRACTS: add doc for loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8516
* Cadical with preprocessor and local search by @kroening in https://github.com/diffblue/cbmc/pull/8502
**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.4.0...cbmc-6.4.1
# CBMC 6.4.0
This release improves upon automated assigns-clause inference for loop invariants, which should make manually adding assigns clauses to loops less frequent.
## What's Changed
* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490
## Bug Fixes
* SMT2: implement range type by @kroening in https://github.com/diffblue/cbmc/pull/8466
* Man pages: improve wording of unwinding-related options by @tautschnig in https://github.com/diffblue/cbmc/pull/8471
* `format_type` can now format `range_typet` by @kroening in https://github.com/diffblue/cbmc/pull/8473
* Contracts: document use of __CPROVER_loop_entry with arrays by @tautschnig in https://github.com/diffblue/cbmc/pull/8470
* `bitvector_typet`: set width from mp_integer by @kroening in https://github.com/diffblue/cbmc/pull/8477
* CI: add macos-14 (macOS on M1) job by @tautschnig in https://github.com/diffblue/cbmc/pull/8382
* Remove macos-12 CI job by @tautschnig in https://github.com/diffblue/cbmc/pull/8482
* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
* zero extension expression by @kroening in https://github.com/diffblue/cbmc/pull/8442
* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490
**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.3.1...cbmc-6.4.0
# CBMC 6.3.1
This patch release addresses build failures on Apple Silicon (via PR #8461).
## Bug Fixes
* C library: Apple does not adhere to aarch64 ABI by @tautschnig in https://github.com/diffblue/cbmc/pull/8461
**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.3.0...cbmc-6.3.1
# CBMC 6.3.0
This release addresses build failures on aarch64 (64-bit ARM) platforms (via PR #8366) and for some CMake configurations (via PR #8435). Users of loop invariants with dynamic frames have two changes to their user experience:
1) Users will no longer need to give unwinding specifications for `do { ... } while(0)` loops.
2) Loop invariants that are conjunctions will be turned into more fine-grained properties to ease debugging of loop invariants when they aren't successfully proved.
## What's Changed
* Contracts: always remove spurious do {... } while(0) loops by @tautschnig in https://github.com/diffblue/cbmc/pull/8459
* Contracts/DFCC: split conjunctions in loop invariants by @tautschnig in https://github.com/diffblue/cbmc/pull/8458
## Bug Fixes
* Do not define project(CBMC ...) twice to fix CMake failures by @tautschnig in https://github.com/diffblue/cbmc/pull/8435
* Contracts: remove bound-var-rewrite by @tautschnig in https://github.com/diffblue/cbmc/pull/8430
* introduce `zero_expr()` and `one_expr()` for number types by @kroening in https://github.com/diffblue/cbmc/pull/8441
* Fix Alpine's assert-statement conversion special case by @tautschnig in https://github.com/diffblue/cbmc/pull/8438
* Fix Python syntax error in doxygen markdown preprocessor by @tautschnig in https://github.com/diffblue/cbmc/pull/8440
* Goto conversion: fix missing source locations by @tautschnig in https://github.com/diffblue/cbmc/pull/8444
* copy constructors for exception classes by @kroening in https://github.com/diffblue/cbmc/pull/8391
* jbmc, janalyzer: Remove unnecessary dynamic_cast by @tautschnig in https://github.com/diffblue/cbmc/pull/8418
* Move is_null_pointer to constant_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/8445
* add documentation of default for --max-nondet-array-length, see #8428 by @lks9 in https://github.com/diffblue/cbmc/pull/8432
* Move make_with_expr to update_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/8448
* Use boolean_negate for immediate simplification by @tautschnig in https://github.com/diffblue/cbmc/pull/8449
* `format_expr` now prints `bv`-typed constants by @kroening in https://github.com/diffblue/cbmc/pull/8457
* C library: fix use of va_list for AARCH64 by @tautschnig in https://github.com/diffblue/cbmc/pull/8366
**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.2.0...cbmc-6.3.0
# 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