analyzer
analyzer copied to clipboard
Remove `__annonCompField` offsets from witness invariants
This is a point in #1722.
For example, this will produce a witness with invariants containing our fictitious __annonCompField offsets:
./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --set exp.architecture 64bit ../sv-benchmarks/c/intel-tdx-module/tdg_mr_report__expected__cover_entry_havoc_memory.i
These should be skipped in witness invariant generation: we can keep the invariant, but just remove such components in the offsets because the following non-anonymous field is supposed to uniquely determine the actual field.
However, there's still a problem: many LDV tasks are CIL-ed and have such field explicitly. There they must remain, but I'm not sure how to differentiate this. Maybe we just have to exclude all such invariants, instead of trying to adapt them.