Skip to content

Commit

Permalink
Merge pull request #7981 from NlightNFotis/new_cbmc_release-5.95.0
Browse files Browse the repository at this point in the history
Mark CBMC cbmc-5.95.0.
  • Loading branch information
NlightNFotis authored Oct 28, 2023
2 parents aed4d77 + b70ffec commit 25cb64d
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 4 deletions.
21 changes: 19 additions & 2 deletions CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,12 +1,29 @@
# CBMC 5.94.0
# CBMC 5.95.0

## What's Changed

* Add C front-end support for vector expressions as compile-time constants by @tautschnig in https://github.com/diffblue/cbmc/pull/7947
* C library: add exp, log, pow models by @tautschnig in https://github.com/diffblue/cbmc/pull/7906

## Bug Fixes

* Fix bug with std::sort requires strict weak ordering by @tautschnig in https://github.com/diffblue/cbmc/pull/7956
* SYNTHESIZER: Use only symbols from the original goto as terminals by @qinheping in https://github.com/diffblue/cbmc/pull/7970
* Add missing lowering of symbol values in new SMT backend by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7952
* Restrict memory-analyzer build to Linux x86_64/i386 by @tautschnig in https://github.com/diffblue/cbmc/pull/7958
* Add support for empty unions in incremental SMT decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7966

**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-5.94.0...cbmc-5.95.0

## CBMC 5.94.0

### What's Changed
* Add models for C library: getpwnam, getpwuid, and getopt by @tautschnig in https://github.com/diffblue/cbmc/pull/7919 and https://github.com/diffblue/cbmc/pull/7916
* Shadow memory addresses now also support --pointer-check argument by @esteffin in https://github.com/diffblue/cbmc/pull/7936
* [DOCS] Add documentation on CBMC Shadow Memory intrinsics and shadow memory functions (via doxygen) by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7913 and https://github.com/diffblue/cbmc/pull/7930
* [SYNTHESIZER] goto-synthesizer now accepts all CBMC options by @qinheping in https://github.com/diffblue/cbmc/pull/7900

## Bug Fixes
### Bug Fixes
* Fix problem on array size L2 renaming by @esteffin in https://github.com/diffblue/cbmc/pull/7877
* Fix shadow memory missing aggregation on non-compound bitvector types by @esteffin in https://github.com/diffblue/cbmc/pull/7935
* Fix SMT encoding of structs which contain a single struct field by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7951
Expand Down
2 changes: 1 addition & 1 deletion src/config.inc
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ endif
OSX_IDENTITY="Developer ID Application: Daniel Kroening"

# Detailed version information
CBMC_VERSION = 5.94.0
CBMC_VERSION = 5.95.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 = "5.94.0"
version = "5.95.0"
edition = "2021"
description = "Rust API for CBMC and assorted CProver tools"
repository = "https://github.com/diffblue/cbmc"
Expand Down

0 comments on commit 25cb64d

Please sign in to comment.