Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
devel:tools:statica
cbmc
cbmc.changes
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
File cbmc.changes of Package cbmc
------------------------------------------------------------------- Thu Jun 15 08:02:45 UTC 2023 - Jiri Slaby <jslaby@suse.cz> - Update to version 5.85.0: * Mark CBMC cbmc-5.85.0. * changed requires variables to requires_ as well as requires_lmbd to differentiate from c++20 keyword requires * Add INVARIANTS checking for empty structs * Add unit test for single member struct encoding * Run Initialisation7 test with new SMT backend * Fix support for structs with a single member * Fix comment and error message typos * Enable SMT solver tests fixed by rudimentary struct support * Conver do{}while(0) to non-loop block * Add warning message in case static library is missing * Field sensitivity: also rewrite byte extract to type casts * CMake build system: support system-provided MiniSat * Add goto-inspect regression tests to Makefile builds * Show before/after lowering in smt2 decision procedure debug output * Add regression test for simple struct support * Add struct encoding to incremental smt2 decision procedure * Refactor smt2 decision procedure to separate lowering * Add encode struct_exprt as field concatenation * Add struct encoding support for symbol expressions * and much more - change URL to github, the original one is ooold - remove * 0001-use-dynamic-minisat-lib.patch (in upstream, sort of) * 0007-gcc-13-include-cstdint-for-int-_t.patch (in upstream) - add * 0001-don-t-add-static-minisat-lib.patch ------------------------------------------------------------------- Tue May 2 07:00:38 UTC 2023 - Jiri Slaby <jslaby@suse.cz> - increase disk constraints on other archs to 11G as the builds are failing. ------------------------------------------------------------------- Wed Mar 22 09:58:02 UTC 2023 - Jiri Slaby <jslaby@suse.cz> - Update to version 5.79.0: * Change the readme.md to only include Rust build commands, now that we no longer build with corrosion * Substitute Ruby for Python oneliner for version finding * Remove dependency on corrosion. * Get the project to work with a toy rust project and link correctly * Add a readme with build instructions on the Rust project * C front-end: fix the interaction between packing and alignment * Import further Clang-defined ia32 builtins * C front-end: declare further GCC built-ins * Improve error reporting in build failures because of missing environment variables * Change environment variable to point to library directory * and much more - renamed * 0001-do-not-build-with-Werror.patch to 0003-do-not-build-with-Werror.patch * 0001-do-not-run-c_library_check.patch to 0005-do-not-run-c_library_check.patch * 0001-make-bash_completion-conforming-to-SUSE.patch to 0004-make-bash_completion-conforming-to-SUSE.patch * 0001-undef-i386.patch to 0006-undef-i386.patch * 0001-use-minisat-s-l_True-l_False.patch to 0002-use-minisat-s-l_True-l_False.patch - added 0007-gcc-13-include-cstdint-for-int-_t.patch ------------------------------------------------------------------- Wed Oct 19 06:32:04 UTC 2022 - Jiri Slaby <jslaby@suse.cz> - Update to version 5.68.0: * Remove vectors: Boolean expressions do not require signed bitvectors * Introduce grammar-based expression enumerators * Update CODEOWNERS * Crangler: support full loop contracts * Move incremental SMT theories into sub directory * change type of numerical architecture symbols to integer * constant_interval_exprt now recognizes integer_typet * C++: __CPROVER_integer and __CPROVER_rational * Add widening strategy into assigns inference * and much more - add _constraints (disk size) to avoid build errors on ppc64 - switch to cmake+ninja - add * 0001-make-bash_completion-conforming-to-SUSE.patch * 0001-do-not-run-c_library_check.patch * 0001-undef-i386.patch ------------------------------------------------------------------- Wed May 11 07:48:23 UTC 2022 - Jiri Slaby <jslaby@suse.cz> - Update to version 5.56.0: * Convert pointer_offset_exprt to SMT * Add conversion of `pointer_object_exprt` and a regression test for that * Add extra test for address-of objects and pointer dereferencing to inte * show bit-pattern of pointers in trace * smt-lib backend: generate annotated_pointer_constant_exprt * CONTRACTS: adding requires and ensures clauses for function pointers * pointer_logic: use mp_integer for numbering objects * and much more - switch from _service to released tarballs ------------------------------------------------------------------- Wed Feb 02 08:06:50 UTC 2022 - jslaby@suse.cz - Update to version 5.49.0: * Regression test scripts: use /Fe with goto-cl * check type invariant of type_with_subtypet * byte operator lowering now preserves c_bit_field_typet * gcc-style asm aliases have multiple subtypes * use ID_frontend_vector in the C front-end * goto-cc: newlines in command files are just whitespace * Fix `irept` printing in failed unit tests * c_enum_typet::underlying_type() and c_bitfield_typet::underlying_type() * array_typet and vector_typet APIs * simplifier now simplifies !(exists/forall) with multiple bindings * constructors for forall_expr/exists_exprt with multiple bindings * and much more ------------------------------------------------------------------- Fri Feb 19 07:50:21 UTC 2021 - jslaby@suse.cz - Update to version 5.24.0+0: * bv_utilst: mark non-modifying members static * bv_pointerst: encapsulate offset/object bit layout * Add documentation for CPROVER_enum_is_in_range * Add regression tests for enum_is_in_range * Implement enum_is_in_range builtin function * bv_pointerst: make all members return (optional) bvt * Make pointer flattened width configurable by bv_pointerst * Enable overriding of boolbvt::boolbv_width * bv_endianness_mapt is specific to bv_pointerst * fix distinct operator * Documentation: consistently use .gb suffix for goto binaries * and much more ------------------------------------------------------------------- Wed Oct 21 06:45:51 UTC 2020 - jslaby@suse.cz - Update to version 5.17.0+12: * symex removed * Remove deprecated windows package building scripts. * Add posix semaphore examples * Duplicate `rw_lock` code * Add test using `pthread_rwlock` * Add pthreads examples * Add test directory for future sequentialization work * Add .github/ responsible members to codeowners. * Remove travis configuration files. * Update CBMC to version 5.17.0 * Cleans-up the implementation to support assigns clauses * Cleans-up all regression tests for assigns clauses * and much more - switch to obs_scm ------------------------------------------------------------------- Wed Jul 31 09:08:41 UTC 2019 - jslaby@suse.com - Update to version 5.8+81: * replace assert(false) by UNREACHABLE * member_offset_bits: express member offset in bits instead of bytes * target name wrong for signed variant of goto-diff * MetaChar: use std::stringstream for incremental escaped-string construction * Test alignment of unions * Do not attempt to compute union sizes when not required * HAVE_BV_REFINEMENT and HAVE_JAVA_BYTECODE are no longer needed * Check for memory leaks in C++ new/delete * Improve ansi-c library syntax check and run via travis * ansi-c library: explicit non-det initialisation, cleanup, syntax fixes * Pointers returned by getenv must not be manipulated * Use iostream for debugging only ------------------------------------------------------------------- Tue Aug 01 13:51:55 UTC 2017 - jslaby@suse.com - Update to version 5.7+730: * Document $, !, @ and # in symbol names * Fix nullptr * Fix linter errors, ignoring big-int and miniz * Allow invariants with structured exceptions * Revert "[depends: #1063] Use nullptr to represent null pointers (targets master)" * Fix nullptr usage, ignoring miniz and big-int * Fix linter errors, ignoring big-int and miniz * Replace macros with exception types * Update exception types with vs2013 support - add 0001-do-not-build-with-Werror.patch - install also man and docs ------------------------------------------------------------------- Wed Mar 9 14:41:10 UTC 2016 - jslaby@suse.com - update to 6174 ------------------------------------------------------------------- Thu Sep 3 17:49:59 UTC 2015 - jslaby@suse.com - update to 5383 ------------------------------------------------------------------- Thu Mar 19 15:33:00 UTC 2015 - jslaby@suse.com - initial package
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor
