From 3ccbf65b678a302a760bf97639f6c805166b8054 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 17 Jun 2024 10:15:20 +0000 Subject: [PATCH] Release CBMC version 6 --- CHANGELOG | 229 +++++++++++++++++++++++++++++++++ src/config.inc | 2 +- src/libcprover-rust/Cargo.toml | 2 +- 3 files changed, 231 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index a991007693e..f59d308dc3f 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,232 @@ +# CBMC 6.0.0 + +## Major Changes +* Change C++ version to C++17 by @esteffin in https://github.com/diffblue/cbmc/pull/7989 +* Enable default analysis flags for CBMC version 6.0+ by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8093 +* Add support for a `--no-unwinding-assertions` flag by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8109 +* Use malloc fail null by default by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8101 +* introduce 'fatal assertions' by @kroening in https://github.com/diffblue/cbmc/pull/8226 +* Permit re-setting --object-bits by @tautschnig in https://github.com/diffblue/cbmc/pull/7858 +* goto-instrument/unwinding: enable unwinding assertions by default by @tautschnig in https://github.com/diffblue/cbmc/pull/8274 +* JBMC: enable unwinding assertions by default by @tautschnig in https://github.com/diffblue/cbmc/pull/8273 +* generate assert(false) when calling undefined function by @kroening in https://github.com/diffblue/cbmc/pull/8292 +* change default verbosity to M_STATUS by @kroening in https://github.com/diffblue/cbmc/pull/8331 + +## What's Changed +* Add support for union values in traces for incremental smt2 decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7990 +* Variables leaving scope on jumping should always be marked dead by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8092 +* Define coverage blocks so as to be terminated by assumptions by @thomasspriggs in https://github.com/diffblue/cbmc/pull/7810 +* Build and infrastructure fixes for FreeBSD by @tautschnig in https://github.com/diffblue/cbmc/pull/7924 +* Add support for variables entering scope via a goto by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8091 +* Remove JSIL front-end by @tautschnig in https://github.com/diffblue/cbmc/pull/8158 +* Compact propositional encoding of OBJECT_SIZE(ptr) by @tautschnig in https://github.com/diffblue/cbmc/pull/7702 +* C front-end: refuse duplicate declaration of local variable by @tautschnig in https://github.com/diffblue/cbmc/pull/8160 +* CMake builds: support system-installed CaDiCaL by @tautschnig in https://github.com/diffblue/cbmc/pull/8159 +* division-by-zero on float by @kroening in https://github.com/diffblue/cbmc/pull/8233 +* Avoid duplicate "warning:" or "error:" output by @tautschnig in https://github.com/diffblue/cbmc/pull/1359 +* add support for loongarch64 by @wuruilong01 in https://github.com/diffblue/cbmc/pull/8266 +* Add support for GNU Hurd by @tautschnig in https://github.com/diffblue/cbmc/pull/8211 +* `__CPROVER_bool` should not have a memory layout by @kroening in https://github.com/diffblue/cbmc/pull/8325 +* add `emscripten` architecture by @kroening in https://github.com/diffblue/cbmc/pull/8334 +* increase verbosity of warning about missing `__builtin_` declaration by @kroening in https://github.com/diffblue/cbmc/pull/8333 +* increase verbosity level of various messages by @kroening in https://github.com/diffblue/cbmc/pull/8330 + +## Bug Fixes +* Add CODEOWNERS for CHANGELOG by @TGWDB in https://github.com/diffblue/cbmc/pull/7988 +* typecheckt::errort by @kroening in https://github.com/diffblue/cbmc/pull/7982 +* string_constantt typing by @kroening in https://github.com/diffblue/cbmc/pull/7965 +* remove index_type() by @kroening in https://github.com/diffblue/cbmc/pull/7992 +* add a 'language feature' detection facility for goto programs by @kroening in https://github.com/diffblue/cbmc/pull/7771 +* Fix line-number output in document-properties-* by @tautschnig in https://github.com/diffblue/cbmc/pull/7994 +* CODING_STANDARD.md: fix references to clang-format by @kroening in https://github.com/diffblue/cbmc/pull/7995 +* Use simplify_exprtt::resultt in pre-order simplification steps by @tautschnig in https://github.com/diffblue/cbmc/pull/6118 +* CBMC version 6 release process changes by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7987 +* Remove useless steps from Rust CI pipeline by @esteffin in https://github.com/diffblue/cbmc/pull/8030 +* Replace `new-smt-backend` tag with inverted `no-new-smt` tag by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8002 +* Remove local declaration of void_t by @tautschnig in https://github.com/diffblue/cbmc/pull/8031 +* [CI] Minor fixes to CI accompanying C++17 version change by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8028 +* Refactor `smt_function_application_termt::indices` using C++17 feature by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8035 +* Restore post-order simplification of byte_extract(c ? a : b, ...) by @tautschnig in https://github.com/diffblue/cbmc/pull/8005 +* Replace usage of `std::result_of` with `std::invoke_result` by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8037 +* Fix the invariant message for unimplemented SMT count trailing zeros conversion. by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8044 +* Fix test_struct_union_c regression test by @esteffin in https://github.com/diffblue/cbmc/pull/8046 +* DFCC instrumentation: ensure programs are well-formed by @tautschnig in https://github.com/diffblue/cbmc/pull/8045 +* Fix failed coverage in if then else with return statements by @esteffin in https://github.com/diffblue/cbmc/pull/8001 +* Make -Wno-maybe-uninitialized the default with GCC by @tautschnig in https://github.com/diffblue/cbmc/pull/8047 +* Enable all `cbmc` regression tests that are passing to run with new SMT backend by @esteffin in https://github.com/diffblue/cbmc/pull/8051 +* C library check: do not warn about the need for MMX by @tautschnig in https://github.com/diffblue/cbmc/pull/8050 +* Use the C++17 standard `[[nodiscard]]` attribute directly by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8036 +* SYNTHESIZER: Add quick filter into goto-synthesizer by @qinheping in https://github.com/diffblue/cbmc/pull/7973 +* fix conversions between long and long long by @kroening in https://github.com/diffblue/cbmc/pull/8086 +* The emscripten compiler has alloca.h by @kroening in https://github.com/diffblue/cbmc/pull/8085 +* Add default codeowners to `/src/symtab2gb/` and `/src/json-symtab-language/` by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8087 +* Remove util_make_unique by @tautschnig in https://github.com/diffblue/cbmc/pull/8032 +* Run additional regressions with new SMT solver by @esteffin in https://github.com/diffblue/cbmc/pull/8084 +* Use the STL versions of `variant` and `optional` in incremental smt2 decision procedure by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8089 +* Remove usages of the deprecated `std::iterator` by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8088 +* Replace nonstd::optional by C++17 std::optional by @tautschnig in https://github.com/diffblue/cbmc/pull/8034 +* [CI] Perform apt update to sync repo sources before trying to install from them. by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8090 +* Dynamic frames: don't instrument __CPROVER_allocated_memory by @tautschnig in https://github.com/diffblue/cbmc/pull/8094 +* languaget is not a messaget [blocks: #3800] by @tautschnig in https://github.com/diffblue/cbmc/pull/4050 +* Name `-paths-lifo` test profiles uniquely by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8097 +* Keep symbols as nondet rather than using their symbol table values in SMT decision procedure. by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8104 +* CSmith test script: avoid a need for argv modelling by @tautschnig in https://github.com/diffblue/cbmc/pull/8105 +* Assignments to bit-fields yield results of bit-field type by @tautschnig in https://github.com/diffblue/cbmc/pull/8082 +* Make componentt::{base,pretty}_name comments by @tautschnig in https://github.com/diffblue/cbmc/pull/5815 +* Refactor `string_constantt::get_value` and `string_constantt::set_value` call sites. by @NlightNFotis in https://github.com/diffblue/cbmc/pull/7999 +* Remove all references to optionalt by @tautschnig in https://github.com/diffblue/cbmc/pull/8099 +* Remove default messaget value from goto_program_dereferencet by @tautschnig in https://github.com/diffblue/cbmc/pull/8100 +* Replace file_util.{h,cpp} by std::filesystem by @tautschnig in https://github.com/diffblue/cbmc/pull/8033 +* Cleanup USE_STD_STRING/USE_DSTRING configuration option by @tautschnig in https://github.com/diffblue/cbmc/pull/8040 +* Enable dependabot to update GitHub actions by @tautschnig in https://github.com/diffblue/cbmc/pull/8115 +* fix nondeterministic hex_trace test by @kroening in https://github.com/diffblue/cbmc/pull/8121 +* Add Michael and Peter to Repository CI codeowners. by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8114 +* Bump actions/checkout from 3 to 4 by @dependabot in https://github.com/diffblue/cbmc/pull/8117 +* Bump actions/upload-artifact from 3 to 4 by @dependabot in https://github.com/diffblue/cbmc/pull/8119 +* Bump github/codeql-action from 2 to 3 by @dependabot in https://github.com/diffblue/cbmc/pull/8120 +* decision_proceduret API with assumptions by @kroening in https://github.com/diffblue/cbmc/pull/7979 +* simplify prop_conv_solvert::push by @kroening in https://github.com/diffblue/cbmc/pull/8122 +* JSIL: create messaget with a message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8125 +* Remove unused `log` member from dfcc_is_freeablet by @tautschnig in https://github.com/diffblue/cbmc/pull/8124 +* Remove unused safety_checkert constructor by @tautschnig in https://github.com/diffblue/cbmc/pull/8126 +* Permit constructing parsert with a message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8134 +* jsil_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8136 +* Add a document outlining the current release process by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8130 +* java_bytecode_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8140 +* [CI] Bring back core release processes by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8108 +* Run again tests with new default checks by @esteffin in https://github.com/diffblue/cbmc/pull/8106 +* cbmc preprocessing: call set_language_options after checking for null by @kroening in https://github.com/diffblue/cbmc/pull/8149 +* dstringt::starts_with can be const by @kroening in https://github.com/diffblue/cbmc/pull/8148 +* unary_exprt::check and nullary_exprt::check by @kroening in https://github.com/diffblue/cbmc/pull/8151 +* Bump jungwinter/split from 1 to 2 by @dependabot in https://github.com/diffblue/cbmc/pull/8118 +* json_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8137 +* Fix document publishing GitHub Action by @tautschnig in https://github.com/diffblue/cbmc/pull/8152 +* CSmith GitHub action: run apt-get update by @tautschnig in https://github.com/diffblue/cbmc/pull/8155 +* C++ front-end: configure C++11+ syntax without ansi_c_parser object by @tautschnig in https://github.com/diffblue/cbmc/pull/8132 +* JSIL front-end: no need for parser reentrancy by @tautschnig in https://github.com/diffblue/cbmc/pull/8153 +* Conversion check: fix off-by-one error for float-to-unsigned by @tautschnig in https://github.com/diffblue/cbmc/pull/8157 +* Reduce Thomas and Fotis code ownership by @thomasspriggs in https://github.com/diffblue/cbmc/pull/8162 +* Bump actions/cache from 3 to 4 by @dependabot in https://github.com/diffblue/cbmc/pull/8164 +* Remove non-existent user from CODEOWNERS by @tautschnig in https://github.com/diffblue/cbmc/pull/8166 +* Code contracts: do not interleave checking and instrumenting by @tautschnig in https://github.com/diffblue/cbmc/pull/8095 +* Linking: only rename file-local symbols by @tautschnig in https://github.com/diffblue/cbmc/pull/8167 +* C front-end: GCC >= 12 support __builtin_shufflevector by @tautschnig in https://github.com/diffblue/cbmc/pull/8170 +* Make ansi_c_internal_additions independent of the parser object by @tautschnig in https://github.com/diffblue/cbmc/pull/8133 +* cbmc-cover/pointer-function-parameters test: negative numbers are ok by @tautschnig in https://github.com/diffblue/cbmc/pull/8177 +* remove_returns: do not lose location numbers by @tautschnig in https://github.com/diffblue/cbmc/pull/8178 +* MMIO instrumentation cleanup by @tautschnig in https://github.com/diffblue/cbmc/pull/8175 +* argc/argv modelling: argument string must remain in scope by @tautschnig in https://github.com/diffblue/cbmc/pull/8174 +* Bump microsoft/setup-msbuild from 1 to 2 by @dependabot in https://github.com/diffblue/cbmc/pull/8184 +* update_bits_exprt by @kroening in https://github.com/diffblue/cbmc/pull/8182 +* SMT2: fix extractbit with non-const index by @kroening in https://github.com/diffblue/cbmc/pull/8180 +* Support Minisat source variants where l_False/l_True are not macros by @tautschnig in https://github.com/diffblue/cbmc/pull/8107 +* Full slicing always requires consistent location numbers by @tautschnig in https://github.com/diffblue/cbmc/pull/8179 +* Remove support for irep_idt-as-std::string by @tautschnig in https://github.com/diffblue/cbmc/pull/8154 +* Scope tree: fix and clarify comment by @tautschnig in https://github.com/diffblue/cbmc/pull/8188 +* Scope tree: add dot output by @tautschnig in https://github.com/diffblue/cbmc/pull/8189 +* assembler_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8139 +* relax bitvector constant check for Verilog bitvectors by @kroening in https://github.com/diffblue/cbmc/pull/8191 +* Use dstringt::starts_with by @kroening in https://github.com/diffblue/cbmc/pull/8150 +* add a fluent-style typet::with_source_location by @kroening in https://github.com/diffblue/cbmc/pull/8194 +* SMT2: simplify interface by @kroening in https://github.com/diffblue/cbmc/pull/8123 +* introduce `update_bit_exprt` by @kroening in https://github.com/diffblue/cbmc/pull/8190 +* Fix gitignore of goto-bmc by @tautschnig in https://github.com/diffblue/cbmc/pull/8197 +* Fix `missing braces around initializer` GCC warning by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8198 +* C library: ASM functions take void* pointers by @tautschnig in https://github.com/diffblue/cbmc/pull/7932 +* C library: additional floating-point functions and cleanup by @tautschnig in https://github.com/diffblue/cbmc/pull/8195 +* array_set: do not fail upon an invalid (void) pointer by @tautschnig in https://github.com/diffblue/cbmc/pull/8202 +* Avoid cross-platform preprocessor need from test by @tautschnig in https://github.com/diffblue/cbmc/pull/8206 +* Make tests pass when char is unsigned by @tautschnig in https://github.com/diffblue/cbmc/pull/8212 +* Deprecate namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8209 +* C library: model __builtin_powi{,f,l} by @tautschnig in https://github.com/diffblue/cbmc/pull/8192 +* Avoid 64-bit platform support requirement for running tests by @tautschnig in https://github.com/diffblue/cbmc/pull/8213 +* Make exprt::with_source_location type safe by @tautschnig in https://github.com/diffblue/cbmc/pull/8216 +* Remove unused goto_convertt::has_function_call by @tautschnig in https://github.com/diffblue/cbmc/pull/8201 +* C++ front-end: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8227 +* Add missing source locations by @tautschnig in https://github.com/diffblue/cbmc/pull/7856 +* Static initialisation: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8221 +* miniBDD test: support lselect by @tautschnig in https://github.com/diffblue/cbmc/pull/8240 +* nondet-volatile: fix handling of enum types by @tautschnig in https://github.com/diffblue/cbmc/pull/8203 +* C/C++ front-end: accept all floating-point extensions that GCC and Clang support by @tautschnig in https://github.com/diffblue/cbmc/pull/8169 +* statement_list_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8138 +* Support __builtin_dynamic_object_size by @tautschnig in https://github.com/diffblue/cbmc/pull/8156 +* xml_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8135 +* ansi_c_parsert: construct with message handler by @tautschnig in https://github.com/diffblue/cbmc/pull/8141 +* C/C++ front-end: Revert scanner re-entrancy by @tautschnig in https://github.com/diffblue/cbmc/pull/8245 +* Improve printf formatter by @tautschnig in https://github.com/diffblue/cbmc/pull/8205 +* Run performance comparison in CI using Kani's Benchcomp by @tautschnig in https://github.com/diffblue/cbmc/pull/8171 +* Add namespacet::follow_struct_union_tag to simplify follow_tag uses by @tautschnig in https://github.com/diffblue/cbmc/pull/8248 +* Rename follow_struct_or_union_tag to follow_tag by @tautschnig in https://github.com/diffblue/cbmc/pull/8251 +* Visual Studio: fix feraiseexcept test failure by @kroening in https://github.com/diffblue/cbmc/pull/8232 +* Move benchcomp YAML file to avoid spurious GitHub errors by @tautschnig in https://github.com/diffblue/cbmc/pull/8250 +* test.pl now reports both directory and descriptor file name by @kroening in https://github.com/diffblue/cbmc/pull/8252 +* Remove parsert::clear and all of its overrides by @tautschnig in https://github.com/diffblue/cbmc/pull/8244 +* util: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8236 +* goto-analyzer.md: fix typos in examples by @rurban in https://github.com/diffblue/cbmc/pull/8255 +* goto-programs: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8230 +* goto-instrument: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8229 +* Add invariant that multiplication uses operands of the same size by @tautschnig in https://github.com/diffblue/cbmc/pull/8241 +* `format_expr` can now print range-typed constants by @kroening in https://github.com/diffblue/cbmc/pull/8259 +* Bump codecov/codecov-action from 3 to 4 by @dependabot in https://github.com/diffblue/cbmc/pull/8183 +* C library: model asprintf, test {v,}asprintf by @tautschnig in https://github.com/diffblue/cbmc/pull/8237 +* C library: implement {v,}snprintf by @tautschnig in https://github.com/diffblue/cbmc/pull/8239 +* C library: implement {v,}dprintf by @tautschnig in https://github.com/diffblue/cbmc/pull/8238 +* C front-end: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8218 +* initialisation of `_Complex` with an initializer list by @kroening in https://github.com/diffblue/cbmc/pull/8265 +* C library: provide implementations of fopen64, freopen64 by @tautschnig in https://github.com/diffblue/cbmc/pull/8267 +* C library: add __time64 by @tautschnig in https://github.com/diffblue/cbmc/pull/8268 +* C library: add mmap64 by @tautschnig in https://github.com/diffblue/cbmc/pull/8269 +* Remove unanchored "error" string from symtab2gb test specs by @tautschnig in https://github.com/diffblue/cbmc/pull/8270 +* C library: add creat, open, openat by @tautschnig in https://github.com/diffblue/cbmc/pull/8271 +* simplify `extractbits_exprt` representation by @kroening in https://github.com/diffblue/cbmc/pull/8246 +* analyses: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8215 +* goto-harness: remove use of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8220 +* Pointer analysis: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8231 +* Move goto_convert files by @kroening in https://github.com/diffblue/cbmc/pull/8253 +* JBMC: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8210 +* Solvers: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8235 +* C library: add __to{lower,upper} as alternative names for {tolower,toupper} by @tautschnig in https://github.com/diffblue/cbmc/pull/8283 +* C++ front-end: permit GCC attributes in using declarations by @tautschnig in https://github.com/diffblue/cbmc/pull/8286 +* C++ front-end: support [[__nodiscard__]] and [[nodiscard]] by @tautschnig in https://github.com/diffblue/cbmc/pull/8287 +* C++ front-end: fix parentheses matching for alignas parsing by @tautschnig in https://github.com/diffblue/cbmc/pull/8288 +* cbmc-cpp/Array4 test now works by @kroening in https://github.com/diffblue/cbmc/pull/8293 +* Visual Studio has added _Static_assert by @kroening in https://github.com/diffblue/cbmc/pull/8294 +* C++ front-end: not all declarators are code-typed by @tautschnig in https://github.com/diffblue/cbmc/pull/8290 +* [CONTRACTS] Refactor quantified symbol detection for loop contracts by @qinheping in https://github.com/diffblue/cbmc/pull/8299 +* C++ front-end: support attributes with tag-less structs by @tautschnig in https://github.com/diffblue/cbmc/pull/8289 +* introduce `literal_vector_exprt` by @kroening in https://github.com/diffblue/cbmc/pull/8307 +* help: add missing newline by @kroening in https://github.com/diffblue/cbmc/pull/8306 +* `goto_check_ct::add_guarded_property` now has `is_fatal` parameter by @kroening in https://github.com/diffblue/cbmc/pull/8297 +* Make `going_to` variable cprover-prefixed by @qinheping in https://github.com/diffblue/cbmc/pull/8312 +* [CONTRACTS] Use fresh converter in loop contracts instrumentation by @qinheping in https://github.com/diffblue/cbmc/pull/8282 +* [CONTRACTS] Ignore cprover symbols in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8313 +* C++ front-end: fix parsing of >> as closing template args by @tautschnig in https://github.com/diffblue/cbmc/pull/8291 +* Lower-byte-operators: bv_to_expr should support bool target type by @tautschnig in https://github.com/diffblue/cbmc/pull/8318 +* Add support for __fp16 where appropriate by @tautschnig in https://github.com/diffblue/cbmc/pull/8323 +* Fix typos in release workflow by @tautschnig in https://github.com/diffblue/cbmc/pull/8322 +* mod-by-zero is now fatal by @kroening in https://github.com/diffblue/cbmc/pull/8315 +* Undefined shifts are now fatal by @kroening in https://github.com/diffblue/cbmc/pull/8304 +* array-bounds checks are now fatal by @kroening in https://github.com/diffblue/cbmc/pull/8314 +* Simplifier: c_bool (and others) are also bitvector types by @tautschnig in https://github.com/diffblue/cbmc/pull/8247 +* Delete `string_constantt::get_value` and `string_constantt::set_value` functions by @NlightNFotis in https://github.com/diffblue/cbmc/pull/8003 +* Remove deprecated messaget() constructor by @tautschnig in https://github.com/diffblue/cbmc/pull/8143 +* Move GCC-13 CI job to Ubuntu 24.04 by @tautschnig in https://github.com/diffblue/cbmc/pull/8320 +* Make DFCC is_dead_object_update less restrictive by @tautschnig in https://github.com/diffblue/cbmc/pull/8261 +* pointer checks are now fatal by @kroening in https://github.com/diffblue/cbmc/pull/8316 +* Expand list of known compiler built-ins by @tautschnig in https://github.com/diffblue/cbmc/pull/8321 +* CMake: use find_program() to look for bash by @guijan in https://github.com/diffblue/cbmc/pull/8285 +* Switch GitHub CI jobs from macos-11 to macos-13 by @tautschnig in https://github.com/diffblue/cbmc/pull/8328 +* Use all 4 vCPUs on GitHub-hosted runners by @tautschnig in https://github.com/diffblue/cbmc/pull/8327 +* Goto crossing scopes: fix scope tree entry of conditions by @tautschnig in https://github.com/diffblue/cbmc/pull/8187 +* Declutter linking implementation by @tautschnig in https://github.com/diffblue/cbmc/pull/8168 +* Avoid brew symlink conflict in macos-13 by @tautschnig in https://github.com/diffblue/cbmc/pull/8338 +* [CONTRACTS] Allow loop contracts annotated to goto statement by @qinheping in https://github.com/diffblue/cbmc/pull/8281 +* cprover: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8219 +* goto-symex: Replace uses of namespacet::follow by @tautschnig in https://github.com/diffblue/cbmc/pull/8222 +* C front-end: typecheck conditional operator over string literal and 0 by @tautschnig in https://github.com/diffblue/cbmc/pull/7946 + +**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-5.95.1...cbmc-6.0.0 + # CBMC 5.95.1 ## What's Changed diff --git a/src/config.inc b/src/config.inc index 2f41286fb9e..9a829064fc4 100644 --- a/src/config.inc +++ b/src/config.inc @@ -79,7 +79,7 @@ endif OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information -CBMC_VERSION = 6.0.0-preview +CBMC_VERSION = 6.0.0 # Use the CUDD library for BDDs, can be installed using `make -C src cudd-download` # CUDD = ../../cudd-3.0.0 diff --git a/src/libcprover-rust/Cargo.toml b/src/libcprover-rust/Cargo.toml index 351345b5ff3..a31fe44b96c 100644 --- a/src/libcprover-rust/Cargo.toml +++ b/src/libcprover-rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "libcprover_rust" -version = "6.0.0-preview" +version = "6.0.0" edition = "2021" description = "Rust API for CBMC and assorted CProver tools" repository = "https://github.com/diffblue/cbmc"