CHANGELOG

# CBMC 6.5.0

This release addresses both soundness (via #8562) and performance issues (via
#8574, #8576) in our code contracts instrumentation, and includes a collection
of bit-operator cleanup (such as #8524, #8531) and floating-point support
improvements (TiesToAway rounding via #8515, native rounding to integer via
#8538) that aid EBMC/HW-CBMC.

## What's Changed
* CONTRACTS: allow pointer predicates to fail in `assume` contexts by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8562
* Add IEEE 754 TiesToAway rounding mode by @kroening in https://github.com/diffblue/cbmc/pull/8515
* Handle quantifiers with statement expressions by @qinheping in https://github.com/diffblue/cbmc/pull/8605

## Bug Fixes
* SMT2: support `onehot` and `onehot0` by @kroening in https://github.com/diffblue/cbmc/pull/8524
* `cmdlinet`: add `value_opt` methods by @kroening in https://github.com/diffblue/cbmc/pull/8525
* add mulit-ary constructor for xor_exprt, bitxor_exprt, bitand_exprt, … by @kroening in https://github.com/diffblue/cbmc/pull/8529
* add nand_exprt, nor_exprt, xnor_exprt, bitnand_exprt, bitnor_exprt by @kroening in https://github.com/diffblue/cbmc/pull/8531
* SMT2: relations on the range type by @kroening in https://github.com/diffblue/cbmc/pull/8523
* SMT2: allow natural-typed shift distance by @kroening in https://github.com/diffblue/cbmc/pull/8519
* SMT2: fix exception thrown when given unsupported expression by @kroening in https://github.com/diffblue/cbmc/pull/8518
* Add floatbv_mod_exprt and floatbv_rem_exprt classes by @kroening in https://github.com/diffblue/cbmc/pull/8532
* use `zero_extend_exprt` in SMT2 front-end by @kroening in https://github.com/diffblue/cbmc/pull/8493
* SMT2: implement cond by @kroening in https://github.com/diffblue/cbmc/pull/8467
* SMT2: bvnor, bvnand are binary only; add bvxnor by @kroening in https://github.com/diffblue/cbmc/pull/8508
* SMT2: implement nand, nor, xnor by @kroening in https://github.com/diffblue/cbmc/pull/8530
* Fix `onehot0` flattening by @kroening in https://github.com/diffblue/cbmc/pull/8536
* implement `xnor` in prop_conv_solvert by @kroening in https://github.com/diffblue/cbmc/pull/8533
* `ieee_floatt`: add preconditions by @kroening in https://github.com/diffblue/cbmc/pull/8540
* Bugfix: flattening for non-binary `bitnor`, `bitnand`, `bitxnor` by @kroening in https://github.com/diffblue/cbmc/pull/8542
* KNOWNBUG test for enum-range check inside LHS of an assignment by @kroening in https://github.com/diffblue/cbmc/pull/8543
* fix enum-range check for LHSs by @kroening in https://github.com/diffblue/cbmc/pull/8544
* protect `ieee_floatt::rounding_mode` by @kroening in https://github.com/diffblue/cbmc/pull/8551
* SMT2 parser: add abbreviated versions of the rounding modes by @kroening in https://github.com/diffblue/cbmc/pull/8539
* `ieee_floatt::one`(...) by @kroening in https://github.com/diffblue/cbmc/pull/8552
* Compile Java regression test sources (1/n) by @peterschrammel in https://github.com/diffblue/cbmc/pull/8487
* Compile Java regression test sources (2/n) by @peterschrammel in https://github.com/diffblue/cbmc/pull/8548
* Compile Java regression test sources (3/n) by @peterschrammel in https://github.com/diffblue/cbmc/pull/8549
* goto-analyzer: `--show-local-bitvector` by @kroening in https://github.com/diffblue/cbmc/pull/8546
* CONTRACTS: ignore `__CPROVER_dead_object` assignments by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8554
* Compile Java regression test sources (4/n) by @peterschrammel in https://github.com/diffblue/cbmc/pull/8553
* util: Replace std::basic_string<unsigned> with std::basic_string<char32_t> by @xokdvium in https://github.com/diffblue/cbmc/pull/8559
* Fix publish workflow by @tautschnig in https://github.com/diffblue/cbmc/pull/8564
* CONTRACTS: force success for necessary pointer predicates by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8574
* CONTRACTS: separation checks using nondet demonic variable by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8576
* CONTRACTS: ensure at most one predicate per pointer by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8577
* add @peterschrammel as code owner to /src/solvers/floatbv by @kroening in https://github.com/diffblue/cbmc/pull/8580
* SMT2: range_type fixes by @kroening in https://github.com/diffblue/cbmc/pull/8537
* Split `ieee_floatt` into `ieee_float_valuet` and `ieee_floatt` by @kroening in https://github.com/diffblue/cbmc/pull/8550
* Update third-party miniz to 0c30a001bc3c70 by @tautschnig in https://github.com/diffblue/cbmc/pull/8563
* implement boolbvt::get for enumeration types by @kroening in https://github.com/diffblue/cbmc/pull/8589
* bump clang-format to clang-15 by @kroening in https://github.com/diffblue/cbmc/pull/8561
* Remove `namespace_baset::follow(typet)` by @kroening in https://github.com/diffblue/cbmc/pull/8590
* Introduce `floatbv_round_to_integral_exprt` by @kroening in https://github.com/diffblue/cbmc/pull/8538
* line number for files with no newline by @kroening in https://github.com/diffblue/cbmc/pull/8558
* Value-set based dereferencing: fix simplified handling of *(p + i) by @tautschnig in https://github.com/diffblue/cbmc/pull/8578
* fixup #8538 -- correct rounding modes for `floor`, `trunc` by @kroening in https://github.com/diffblue/cbmc/pull/8597
* simplify: rewrite `bitxnor` on booleans to equal by @kroening in https://github.com/diffblue/cbmc/pull/8594
* CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8603

**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.4.1...cbmc-6.5.0

# 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