Skip to content

Commit

Permalink
Release CBMC 6.2.0
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Sep 2, 2024
1 parent 59674e3 commit 54cdfbe
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 2 deletions.
25 changes: 25 additions & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
@@ -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 <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
Expand Down
2 changes: 1 addition & 1 deletion src/config.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/libcprover-rust/Cargo.toml
Original file line number Diff line number Diff line change
@@ -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"
Expand Down

0 comments on commit 54cdfbe

Please sign in to comment.