Changelog for cbmc-5.85.0-lp155.1.5.x86_64.rpm :

* Thu Jun 15 2023 Jiri Slaby - 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 02 2023 Jiri Slaby - increase disk constraints on other archs to 11G as the builds are failing.
* Wed Mar 22 2023 Jiri Slaby - 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 2022 Jiri Slaby - 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 2022 Jiri Slaby - 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 2022 jslabyAATTsuse.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 2021 jslabyAATTsuse.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 2020 jslabyAATTsuse.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 2019 jslabyAATTsuse.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 2017 jslabyAATTsuse.com- Update to version 5.7+730:
* Document $, !, AATT 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 09 2016 jslabyAATTsuse.com- update to 6174
* Thu Sep 03 2015 jslabyAATTsuse.com- update to 5383
* Thu Mar 19 2015 jslabyAATTsuse.com- initial package