Open J2000A opened 1 year ago
michael-schwarz
commented
1 year ago Thank you for this report! For it to be within scope here, the programs would need to actually compile with, e.g., gcc. Did you check whether this is the case?
Otherwise I'd suggest to transfer it to the goblint repo, as the assert transformation is implemented there.
J2000A
commented
1 year ago Hello @michael-schwarz,
the input programs do compile with gcc:
gcc tests/regression/09-regions/36-global_init_rc.c -c -w runs without problems
but the transfored ones do not:
./goblint tests/regression/09-regions/36-global_init_rc.c --enable trans.goblint-check --set trans.activated '["assert"]' --set trans.output transformed.c
gcc transformed.c -c -w
results in
transformed.c:1440:42: error: ‘reallocarray’ undeclared here (not in a function)
1440 | __malloc__(__builtin_free,1), __malloc__(reallocarray,1), __alloc_size__(2,3))) ;
| ^~~~~~~~~~~~
transformed.c: In function ‘main’:
transformed.c:1763:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1763 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1764:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1764 | __goblint_check(p->next == 0);
| ^~
transformed.c:1766:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1766 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1767:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1767 | __goblint_check(p->next == 0);
| ^~
transformed.c:1769:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1769 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1770:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1770 | __goblint_check(p->next == 0);
| ^~
transformed.c:1772:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1772 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1773:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1773 | __goblint_check(p->next == 0);
| ^~
transformed.c:1775:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1775 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1776:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1776 | __goblint_check(p->next == 0);
| ^~
transformed.c:1778:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1778 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1779:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1779 | __goblint_check(p->next == 0);
| ^~
transformed.c:1781:21: error: invalid operands to binary == (have ‘struct s’ and ‘struct s *’)
1781 | __goblint_check(p == & p);
| ^~ ~~~
| |
| struct s *
transformed.c:1782:20: error: invalid type argument of ‘->’ (have ‘struct s’)
1782 | __goblint_check(p->next == 0);
| ^~Thanks for the quick reply! Yes, but this seems like it is the transformation that causes the issue right? So it's less of an issue with CIL rejecting valid code, and more with the transformation in Goblint producing incorrect code, and as such an issue with Goblint?
sim642
commented
1 year ago These might be issues with the invariant expression generation from our domains. We sometimes have representations which don't match the types precisely, so naively dumping them could cause problems like this.
During the implementation for my bachelor thesis about generating test cases for the incremental analysis I encountered a problem: When using the transformation assert sometimes cil files are created that result in parsing errors. @stilscher
Some errors seem to be related to structs: Reproduce by:
./goblint tests/regression/09-regions/36-global_init_rc.c --enable trans.goblint-check --set trans.activated '["assert"]' --set trans.output transformed.c && ./goblint transformed.cCil createsbut it should be
Error Message:
Some seem to be related to the declaration and access of arrays: Reproduce by:
./goblint tests/regression/11-heap/09-no_strong_update_not_unique_thread.c --enable trans.goblint-check --set trans.activated '["assert"]' --set trans.output transformed.c && ./goblint transformed.cbut it should be
Error Message:
Analogously the problems are found when running the mutation generator on the following regression tests (Warning: The error may only occur on a mutated file. Thus, not all of theses errors can be reproduced without the mutation generator):