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.4.0 #8495

Merged
merged 1 commit into from
Nov 6, 2024
Merged

Release CBMC 6.4.0 #8495

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
24 changes: 24 additions & 0 deletions CHANGELOG
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,27 @@
# CBMC 6.4.0

This release improves upon automated assigns-clause inference for loop invariants, which should make manually adding assigns clauses to loops less frequent.

## What's Changed
* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490

## Bug Fixes
* SMT2: implement range type by @kroening in https://github.com/diffblue/cbmc/pull/8466
* Man pages: improve wording of unwinding-related options by @tautschnig in https://github.com/diffblue/cbmc/pull/8471
* `format_type` can now format `range_typet` by @kroening in https://github.com/diffblue/cbmc/pull/8473
* Contracts: document use of __CPROVER_loop_entry with arrays by @tautschnig in https://github.com/diffblue/cbmc/pull/8470
* `bitvector_typet`: set width from mp_integer by @kroening in https://github.com/diffblue/cbmc/pull/8477
* CI: add macos-14 (macOS on M1) job by @tautschnig in https://github.com/diffblue/cbmc/pull/8382
* Remove macos-12 CI job by @tautschnig in https://github.com/diffblue/cbmc/pull/8482
* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
* zero extension expression by @kroening in https://github.com/diffblue/cbmc/pull/8442
* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490

**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.3.1...cbmc-6.4.0

# CBMC 6.3.1

This patch release addresses build failures on Apple Silicon (via PR #8461).
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.3.1
CBMC_VERSION = 6.4.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.3.1"
version = "6.4.0"
edition = "2021"
description = "Rust API for CBMC and assorted CProver tools"
repository = "https://github.com/diffblue/cbmc"
Expand Down
Loading