From 54cdfbe70e1c167205a8c4d5fc28aba6b349f219 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 2 Sep 2024 18:55:18 +0000 Subject: [PATCH] Release CBMC 6.2.0 --- CHANGELOG | 25 +++++++++++++++++++++++++ src/config.inc | 2 +- src/libcprover-rust/Cargo.toml | 2 +- 3 files changed, 27 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 5a4fdd87b3c..24a63ab5610 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,28 @@ +# 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 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 diff --git a/src/config.inc b/src/config.inc index ed8c93baca4..b68ca94c372 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.1.1 +CBMC_VERSION = 6.2.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 b6c372e829f..375bd3d0524 100644 --- a/src/libcprover-rust/Cargo.toml +++ b/src/libcprover-rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "libcprover_rust" -version = "6.1.1" +version = "6.2.0" edition = "2021" description = "Rust API for CBMC and assorted CProver tools" repository = "https://github.com/diffblue/cbmc"