Skip to content

Commit

Permalink
Release CBMC version 6.1.0
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Jul 22, 2024
1 parent 3208438 commit 542c428
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 2 deletions.
27 changes: 27 additions & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
@@ -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
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.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
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.0.1"
version = "6.1.0"
edition = "2021"
description = "Rust API for CBMC and assorted CProver tools"
repository = "https://github.com/diffblue/cbmc"
Expand Down

0 comments on commit 542c428

Please sign in to comment.