search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

Emit invariants for static global variables #1538

Open michael-schwarz opened 2 months ago

michael-schwarz commented 2 months ago

../../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.

michael-schwarz commented 2 months ago

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.