Transformation `assert` creates ` __VERIFIER_assert()` that fail

[J2000A]

During the implementation for my bachelor thesis about generating test cases for the incremental analysis I encountered a problem: I use the transformation assert to write out __VERIFIER_assert() that I change to __goblint_check().

However some of the asserts that are generated by the transformation do fail.

Reproduce by: cp tests/regression/01-cpa/20-static_var.c input.c grep -v "__goblint_check(" input.c > tmp.c && mv tmp.c input.c Remove goblint checks from program ./goblint input.c --set trans.activated '["assert"]' sed -i 's/__VERIFIER_assert/__goblint_check/g' transformed.c Rename the verifier asserts to goblint checks ./goblint transformed.c --html

I think this might have something to do with cil. When inspecting the results a new variable x___0 is introduced by cil alongside x. The checks would hold if they were asserting the variable x___0 instead of x.

Note: There are also asserts that are unknown or are deadcode. However I would want to wait for the responses to this issue before creating the other issues.

Analogously the problem for failing asserts is 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):

../../analyzer/tests/regression/01-cpa/20-static_var.c
../../analyzer/tests/regression/01-cpa/37-div.c
../../analyzer/tests/regression/05-lval_ls/19-idxunknown_unlock_precise.c
../../analyzer/tests/regression/26-undefined_behavior/06-pointer-to-arrays-of-different-sizes.c
../../analyzer/tests/regression/26-undefined_behavior/07-arrays-within-structures.c
../../analyzer/tests/regression/28-race_reach/06-cond_racing1.c
../../analyzer/tests/regression/28-race_reach/07-cond_racing2.c
../../analyzer/tests/regression/28-race_reach/08-cond_racefree.c
../../analyzer/tests/regression/37-congruence/03-interval-overflow.c
../../analyzer/tests/regression/41-stdlib/01-qsort.c
../../analyzer/tests/regression/42-annotated-precision/23-26_07-arrays-within-structures.c
../../analyzer/tests/regression/55-loop-unrolling/07-nested-unroll.c
../../analyzer/tests/regression/57-floats/06-library_functions.c
../../analyzer/tests/regression/57-floats/07-equality.c
../../analyzer/tests/regression/57-floats/11-advanced_invariants.c
../../analyzer/tests/regression/57-floats/15-more-library.c
../../analyzer/tests/regression/58-base-mm-tid/11-tid-toy10.c
../../analyzer/tests/regression/63-affeq/02-unsigned_guards.c (Contained SKIP keyword in first line)
../../analyzer/tests/regression/66-interval-set-one/04-interval-overflow.c
../../analyzer/tests/regression/66-interval-set-one/12-tid-toy10.c
../../analyzer/tests/regression/67-interval-sets-two/08-nested-unroll.c
../../analyzer/tests/regression/67-interval-sets-two/19-arrays-within-structures.c
../../analyzer/tests/regression/67-interval-sets-two/39-div.c
../../analyzer/tests/regression/67-interval-sets-two/53-pointer-to-arrays-of-different-sizes.c

[sim642]

The invariant generator for witnesses uses alpha-conversion data from CIL to correctly output invariants w.r.t. the original program's variable names. Could be that the assert transformation also invokes that when it shouldn't since its invariants need to hold in the CIL-transformed program, not the original one.