diff --git a/CHANGELOG b/CHANGELOG index d0e93ffd764..281484e041d 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,45 @@ +# CBMC 6.8.0 + +This release extends the JSON interface to reading full GOTO functions (and not +just symbol tables) (via #8713). Also included are various usability +improvements around contracts instrumentation (see #8697, #8694). + +## What's Changed +* Add support for reading GOTO functions from JSON by @tautschnig in https://github.com/diffblue/cbmc/pull/8713 +* Add --external-smt2-solver for custom solver path or custom options by @tautschnig in https://github.com/diffblue/cbmc/pull/8726 + +## Bug Fixes +* Switch macos-13 CI jobs to macos-15-intel by @tautschnig in https://github.com/diffblue/cbmc/pull/8725 +* goto-harness: use __CPROVER_(de)?allocate, not malloc/free by @tautschnig in https://github.com/diffblue/cbmc/pull/8684 +* SMT2 back-end: flatten with_exprt operands by @tautschnig in https://github.com/diffblue/cbmc/pull/8670 +* Simplifier: do not create extractbits with pointer type by @tautschnig in https://github.com/diffblue/cbmc/pull/8678 +* C library: remove explicit zero initialisers by @tautschnig in https://github.com/diffblue/cbmc/pull/8698 +* Contracts instrumentation: cleanup unnecessary includes by @tautschnig in https://github.com/diffblue/cbmc/pull/8696 +* Extend cbmc-incr-oneloop timeout with CMake by @tautschnig in https://github.com/diffblue/cbmc/pull/8701 +* C front-end: tolerate type differences with asm renaming by @tautschnig in https://github.com/diffblue/cbmc/pull/7584 +* Bump actions/checkout from 4 to 5 by @dependabot[bot] in https://github.com/diffblue/cbmc/pull/8709 +* Contracts instrumentation: hide unhelpful "no body" warnings by @tautschnig in https://github.com/diffblue/cbmc/pull/8697 +* DFCC: do not surface confusing warning by @tautschnig in https://github.com/diffblue/cbmc/pull/8694 +* Flow-insensitive value set: don't create index expressions over non-array objects by @tautschnig in https://github.com/diffblue/cbmc/pull/8651 +* Value set: remove array-of-array special case by @tautschnig in https://github.com/diffblue/cbmc/pull/8653 +* unwindsett: goto_model is only needed for options processing by @tautschnig in https://github.com/diffblue/cbmc/pull/8643 +* MacOS CI job: do not re-install CMake by @tautschnig in https://github.com/diffblue/cbmc/pull/8711 +* Add remove-function-body-regex command line option by @tautschnig in https://github.com/diffblue/cbmc/pull/8712 +* Make goto_symext::language_mode protected by @tautschnig in https://github.com/diffblue/cbmc/pull/8646 +* Fix support for mathematical types by @tautschnig in https://github.com/diffblue/cbmc/pull/8324 +* Bump github/codeql-action from 3 to 4 by @dependabot[bot] in https://github.com/diffblue/cbmc/pull/8715 +* Use bv_utilst::sign_bit by @tautschnig in https://github.com/diffblue/cbmc/pull/8716 +* Improve bv_utilst less-than-or-less-or-equals by @tautschnig in https://github.com/diffblue/cbmc/pull/8718 +* Implement popcount in flattening back-end by @tautschnig in https://github.com/diffblue/cbmc/pull/8717 +* operator== for exprt and bool, int, nullptr_t by @tautschnig in https://github.com/diffblue/cbmc/pull/8675 +* Update *BSD CI actions to the latest OS versions by @tautschnig in https://github.com/diffblue/cbmc/pull/8719 +* Mark constant_exprt::value_is_zero_string protected [depends-on: 8675] by @tautschnig in https://github.com/diffblue/cbmc/pull/8455 +* Field sensitivity: account for array size in all index expressions by @tautschnig in https://github.com/diffblue/cbmc/pull/8579 +* Bump actions/upload-artifact from 4 to 5 by @dependabot[bot] in https://github.com/diffblue/cbmc/pull/8721 +* Simplify WITH expression over structs with a single component by @tautschnig in https://github.com/diffblue/cbmc/pull/8724 + +**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.7.1...cbmc-6.8.0 + # CBMC 6.7.1 This release addresses bugs in our handling of array-update ("with") diff --git a/src/config.inc b/src/config.inc index b4e09fdff33..09fbf7923d0 100644 --- a/src/config.inc +++ b/src/config.inc @@ -47,7 +47,7 @@ endif OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information -CBMC_VERSION = 6.7.1 +CBMC_VERSION = 6.8.0 # Use the CUDD library for BDDs, can be installed using `make -C src cudd-download` # CUDD = ../../cudd-3.0.0 diff --git a/src/libcprover-rust/Cargo.toml b/src/libcprover-rust/Cargo.toml index 64bbbe3205f..31c297c47a2 100644 --- a/src/libcprover-rust/Cargo.toml +++ b/src/libcprover-rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "libcprover_rust" -version = "6.7.1" +version = "6.8.0" edition = "2021" description = "Rust API for CBMC and assorted CProver tools" repository = "https://github.com/diffblue/cbmc"