Emit invariants for static global variables
michael-schwarz opened this issue · 1 comments
../../analyzer/goblint --conf ../../analyzer/conf/traces-rel.json --enable ana.sv-comp.functions --set dbg.timeout 1200 --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable allglobs -v --enable witness.yaml.enabled linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i --set witness.yaml.path out.yml
does not produce invariants for the program point in line 11382 which follows a lock. In the earlier version, we created invariants there. Our current version can also validate old invariants and when inspecting the program point there are things that Goblint finds hold there, so it seems to be a generation problem.
In general, for the SV-COMP subset used for ESOP'23 we do not create any invariants anymore.
The difference seems to be due to our witness generation treating all static variables as out-of-scope because they could be syntactically pulled up static variables with limited scope.
However, in the input program, they are actually globals with static linkage, i.e., file scope. We should add an option to add an attribute similar to goblint_cil_nested to those static locals that are pulled up.