analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Remove `__annonCompField` offsets from witness invariants

Open sim642 opened this issue 1 month ago • 0 comments

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.

sim642 avatar Nov 12 '25 10:11 sim642