The updates are sometimes in larger chunks (i.e. multiple releases at once), however the commit messages still contain information about the performed changes. Once everything is reviewed (and https://github.com/peterschrammel/cbmc/pull/28 merged), I will again change the submodule commit and squash everything into one commit.
Short overview of changes:
lots of deprecations and API changes around goto_instructiont (getting function calls, assignments, condition, etc.), an equivalent API was always present so no problems there
argc is now not guaranteed to be >= 1 by CBMC (see the linked commit in the 5.50 commit message) to match the C standard. I had to make tests less strict due to this change.
solver backend now returns annotated_pointer_constant instead of just a simple constant (this had to be adjusted in heap domain)
make_assertions_false which was removed in CBMC is re-added to 2LS
free::record variables collection stopped working due to the variable being moved to __CPROVER_deallocate function, we need to collect __CPROVER_deallocate::record now.
base_type source file removed, these don't seem to be necessary, we can just compare the types, hopefully
Related CBMC PR: https://github.com/peterschrammel/cbmc/pull/28
The updates are sometimes in larger chunks (i.e. multiple releases at once), however the commit messages still contain information about the performed changes. Once everything is reviewed (and https://github.com/peterschrammel/cbmc/pull/28 merged), I will again change the submodule commit and squash everything into one commit.
Short overview of changes:
goto_instructiont
(getting function calls, assignments, condition, etc.), an equivalent API was always present so no problems there>= 1
by CBMC (see the linked commit in the 5.50 commit message) to match the C standard. I had to make tests less strict due to this change.annotated_pointer_constant
instead of just a simple constant (this had to be adjusted in heap domain)make_assertions_false
which was removed in CBMC is re-added to 2LSfree::record
variables collection stopped working due to the variable being moved to__CPROVER_deallocate
function, we need to collect__CPROVER_deallocate::record
now.base_type
source file removed, these don't seem to be necessary, we can just compare the types, hopefullyCC @viktormalik