File cbmc.changes of Package cbmc
-------------------------------------------------------------------
Wed Jun 25 08:35:18 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
- require g++-14 for old distros
-------------------------------------------------------------------
Fri May 30 09:23:57 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
- Update to version 6.0.0
* see: https://github.com/diffblue/cbmc/blob/develop/CHANGELOG
- add
* 0002-do-not-build-with-Werror.patch
* 0003-make-bash_completion-conforming-to-SUSE.patch
* 0004-do-not-run-c_library_check.patch
- remove
* 0002-use-minisat-s-l_True-l_False.patch
* 0003-do-not-build-with-Werror.patch
* 0004-make-bash_completion-conforming-to-SUSE.patch
* 0005-do-not-run-c_library_check.patch
* 0006-undef-i386.patch
-------------------------------------------------------------------
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
