Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Release CBMC 6.3.0 #8460

Merged
merged 1 commit into from
Sep 19, 2024
+30 −2
Merged

Release CBMC 6.3.0 #8460

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions CHANGELOG
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,31 @@
# CBMC 6.3.0

This release addresses build failures on aarch64 (64-bit ARM) platforms (via PR #8366) and for some CMake configurations (via PR #8435). Users of loop invariants with dynamic frames have two changes to their user experience:
1) Users will no longer need to give unwinding specifications for `do { ... } while(0)` loops.
2) Loop invariants that are conjunctions will be turned into more fine-grained properties to ease debugging of loop invariants when they aren't successfully proved.

## What's Changed
* Contracts: always remove spurious do {... } while(0) loops by @tautschnig in https://github.com/diffblue/cbmc/pull/8459
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tell the user why this is great... e.g. "Therefore, introducing a do { ... } while (0) loop, either explicitly or as the result of a macro, will not change the numbering of other loops, and therefore will not impact the setting of unwindsets for other loops."

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or something like that...

* Contracts/DFCC: split conjunctions in loop invariants by @tautschnig in https://github.com/diffblue/cbmc/pull/8458

## Bug Fixes
* Do not define project(CBMC ...) twice to fix CMake failures by @tautschnig in https://github.com/diffblue/cbmc/pull/8435
* Contracts: remove bound-var-rewrite by @tautschnig in https://github.com/diffblue/cbmc/pull/8430
* introduce `zero_expr()` and `one_expr()` for number types by @kroening in https://github.com/diffblue/cbmc/pull/8441
* Fix Alpine's assert-statement conversion special case by @tautschnig in https://github.com/diffblue/cbmc/pull/8438
* Fix Python syntax error in doxygen markdown preprocessor by @tautschnig in https://github.com/diffblue/cbmc/pull/8440
* Goto conversion: fix missing source locations by @tautschnig in https://github.com/diffblue/cbmc/pull/8444
* copy constructors for exception classes by @kroening in https://github.com/diffblue/cbmc/pull/8391
* jbmc, janalyzer: Remove unnecessary dynamic_cast by @tautschnig in https://github.com/diffblue/cbmc/pull/8418
* Move is_null_pointer to constant_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/8445
* add documentation of default for --max-nondet-array-length, see #8428 by @lks9 in https://github.com/diffblue/cbmc/pull/8432
* Move make_with_expr to update_exprt by @tautschnig in https://github.com/diffblue/cbmc/pull/8448
* Use boolean_negate for immediate simplification by @tautschnig in https://github.com/diffblue/cbmc/pull/8449
* `format_expr` now prints `bv`-typed constants by @kroening in https://github.com/diffblue/cbmc/pull/8457
* C library: fix use of va_list for AARCH64 by @tautschnig in https://github.com/diffblue/cbmc/pull/8366

**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.2.0...cbmc-6.3.0

# CBMC 6.2.0

## What's Changed
Expand Down
2 changes: 1 addition & 1 deletion src/config.inc
View file
Open in desktop
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.2.0
CBMC_VERSION = 6.3.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
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "libcprover_rust"
version = "6.2.0"
version = "6.3.0"
edition = "2021"
description = "Rust API for CBMC and assorted CProver tools"
repository = "https://github.com/diffblue/cbmc"
Expand Down
Loading