diff --git a/CHANGELOG b/CHANGELOG index ea5b5c5a764..5d901026841 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,30 @@ +# 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 diff --git a/src/config.inc b/src/config.inc index 4c90ee957af..ffeb09af91b 100644 --- a/src/config.inc +++ b/src/config.inc @@ -79,7 +79,7 @@ endif OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information -CBMC_VERSION = 6.0.1 +CBMC_VERSION = 6.1.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 f222bb56f85..08ffb6d9a52 100644 --- a/src/libcprover-rust/Cargo.toml +++ b/src/libcprover-rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "libcprover_rust" -version = "6.0.1" +version = "6.1.0" edition = "2021" description = "Rust API for CBMC and assorted CProver tools" repository = "https://github.com/diffblue/cbmc"