YAML witnesses get evaluated at unrelated nodes

[michael-schwarz]

For my thesis, I am re-running some old experiments and find that some invariants for pfscan can not be re-validated. After fixing issues because of #1535 some validation failures remain.

Here, it seems the YAML validator tries to evaluate expression at completely unrelated nodes. For example a witness for line 977 (Node 665) gets evaluated at a node corresponding to line 1032 (where the invariant obviously does not hold).

If I print the node information of failing witnesses with

M.warn ~category:Witness ~loc:msgLoc "Location: %s at %a" (Node.show_id n) d_loc (Node0.location n);

I get

[Warning][Witness] Location: 695 at pfscan_comb.c:1032 (pfscan_comb.c:977:2)

so the locations appear to be wrong.

This is on top of #1417 now, I'll have to see if the same also happens on master.

[michael-schwarz]

Numerically, the offset (55 lines) somehow is quite close to the size of the second input file for Goblint (49 lines), but that may be coincidence.

[michael-schwarz]

Command to reproduce (from bench repo):

../../analyzer/goblint --conf ../../analyzer/conf/traces-rel.json --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 ./pfscan_comb.c ./pfscan_ftw.c --set witness.yaml.validate ./pfscan_comb_traces_rel.yml

[michael-schwarz]

Hmm, it seems the invariants in the file all have entry_type loop_invariant, even when they have nothing to do with loops. Maybe that's also part of what goes wrong...

[michael-schwarz]

loop_invariant vs location_invariant was actually the cause of the problem.