Update to CBMC 5.12 #152
Update to CBMC 5.12 #152
Conversation
|
Thanks for the review, addressed your comments in a separate commit (since it won't be visible in the final commit after squashing anyway) |
| result=typecast_exprt(sum, address.type()); | ||
|
|
||
| return result; | ||
| } |
There was a problem hiding this comment.
What does this branch return?
There was a problem hiding this comment.
As far as I can understand, it converts an expression where a member is accessed to an expression where offset is used instead of the member.
| @@ -112,13 +115,22 @@ bool twols_parse_optionst::unwind_goto_into_loop( | |||
| loopst loops; | |||
| Forall_goto_program_instructions(i_it, body) | |||
| { | |||
| if(i_it->is_backwards_goto()) | |||
There was a problem hiding this comment.
(independent of this PR) If you think that this is a bug in goto program it may be worth creating a unit test for goto program that reproduces the issue.
There was a problem hiding this comment.
I think it may be a bug, though I am not completely sure. In one of our regression tests (termination/ite4), this call resulted in a segfault. We tried to investigate it but it was very weird - we successfully entered the method (hence i_it is fine) but the number of targets of the goto was huge so I'd guess that's where the bug came from (iterating over the targets and accessing a weird memory location).
It may have already been fixed in a later version of CBMC. We could try to revert this commit once we are close to CBMC:develop and if it still fails, we can try to find the root cause + add a unit test. Or maybe could you try it if you have latest CBMC setup? The reproducer is very simple:
int foo(int x)
{
int res;
if(x) return 0;
else return 1;
}
int bar(int x)
{
int res;
if(x) res = 0;
else res = 1;
return res;
}
void main()
{
int x;
int y = foo(x);
assert(0<=y && y<=1);
y = bar(x);
assert(0<=y && y<=1);
}
If I remember correctly, the segfault happened right in the first function at if.
|
Thanks for the review, I will address your comments tomorrow. I'd also like to merge the CI PR first. As for the |
Makes sense. |
|
Please rebase on the submodule |
Fix decision_procedure include
Update satcheckt solver creation
Update initialize method arguments
Workaround missing function id in goto instruction
Workaround changes to symbol_exprt constructor
Convert to_integer argument to const expression
Fix obtaining of entry state
Get rid of deprecated nil_typet
Fix index_exprt initialization
Replace deprecated symbol_typet
Replace get_unsigned_int with get_size_t
Replace deprecated is_procedure_local
Fix construction of byte_extract_exprt
Replace deprecated integer2ulong
Replace deprecated make_typecast
Replace deprecated find_symbols call
Fix langapi include
Fix xml_expr include
Remove unused replace method
Add constructor without arguments to row_valuet
Do not try to create symbol_exprt with 0 arguments
Refactor find_corresponding_symbol to return optionalt to achieve this
Workaround missing default constructor for symbol_exprt
Workaround missing default constant_exprt constructor in preadbs_domain
Correctly include integer_typet
Replace deprecated integer2unsigned
Fix get_loophead_selects prototype
Workaround removed property_checkert
Fix show_goto_functions call
Fix show_properties call
Fix show_defs ssa_analysis output
Fix side_effect_expr_nondett construction
Fix goto unwinding
Link with goto-checker
Initialize values to bottom
Pass message_handler to incremental_solver
Initialize states of analyses to bottom
Use NOT_CHECKED when checking status
Simplify incremental solver using CBMC's push and pop
Make solvers less verbose unless debugging
Do not add __CPROVER variables to counterexample
Avoid the use of is_backwards_goto while unwinding
- The method may in some cases (e.g. ite4 termination regression test)
cause a segfault for unknown reasons. Flip the condition, check using
incoming edges if an instruction is loop head rather than checking
if a goto is loop exit.
Initialize properties with UNKNOWN
- This is better for backwards compatibility for now, since we have no way
of checking if a property was checked or we simply could not check it.
However this is a potential place for improvements.
Initialize constant propagator states
Update expected assert description
- CBMC 5.12 changed the assertion description of fields of structures to
be more user-friendly (the field is named instead of an offset added).
Signed-off-by: František Nečas <[email protected]>
Signed-off-by: František Nečas <[email protected]>
Signed-off-by: František Nečas <[email protected]>
FrNecas
force-pushed
the
frnecas-cbmc-5.12
branch
from
a35adc7 to
8eb92b5
Compare
|
Done, rebased and squashed |
|
Thanks for merging. @peterschrammel could you please create The only problem with the release right now is a regression in heap domain (occurred first with 5.18) which we are currently trying to debug. |
Done. |
There have been a lot of changes in this pull request. Below is just a short overview of the most significant ones and some comments:
failed to find state errorbut it turned out I had to call it a bit differently to make it initialize states.UNKNOWNfor now (for compatibility) but this may be a place for potential refactoring (differentiating between not having checked the property and having checked it but not knowing its correctness).Looking at the CI failures, I will push one more commit with code style fixes (will squash it at the end). I don't really know why compilation with
clang++3.7is failing but it seems to come from CBMC so probably not much I can do about that...Related: peterschrammel/cbmc#25