From 89b437dc9cb69b5d05a4a7053d3cce119259e28d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 12 Nov 2025 12:31:12 +0200
Subject: [PATCH] Remove __annonCompField offsets from witness invariants

---
 src/cdomain/value/domains/invariant.ml    |  1 +
 src/cdomain/value/domains/invariantCil.ml | 26 +++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/src/cdomain/value/domains/invariant.ml b/src/cdomain/value/domains/invariant.ml
index 03cd57634b..94f65b9ada 100644
--- a/src/cdomain/value/domains/invariant.ml
+++ b/src/cdomain/value/domains/invariant.ml
@@ -53,6 +53,7 @@ struct
       inv
       |> exp_deep_unroll_types
       |> InvariantCil.exp_replace_original_name
+      |> InvariantCil.exp_remove_anon_comp_offset
     in
     if GobConfig.get_bool "witness.invariant.split-conjunction" then
       ES.elements (pullOutCommonConjuncts inv')
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index d0194fcd75..df1f3f9e0e 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -17,6 +17,32 @@ let exp_replace_original_name =
   let visitor = new exp_replace_original_name_visitor in
   visitCilExpr visitor
 
+let fieldinfo_is_anon (fi: fieldinfo) =
+  String.starts_with ~prefix:"__annonCompField" fi.fname (* TODO: what if CIL-ed program explicitly has this? *)
+
+let rec offset_remove_anon_comp_offset = function
+  | NoOffset -> NoOffset
+  | Index (e, offs') -> Index (e, offset_remove_anon_comp_offset offs')
+  | Field (fi, offs') ->
+    let offs'' = offset_remove_anon_comp_offset offs' in
+    if fieldinfo_is_anon fi then (
+      match offs'' with
+      | Field _ -> offs''
+      | NoOffset
+      | Index _ -> failwith "offset_remove_anon_comp_offset: anon comp field not followed by field"
+    )
+    else
+      Field (fi, offs'')
+
+class exp_remove_anon_comp_offset_visitor = object
+  inherit nopCilVisitor
+  method! voffs (offs: offset) =
+    ChangeTo (offset_remove_anon_comp_offset offs)
+end
+let exp_remove_anon_comp_offset =
+  let visitor = new exp_remove_anon_comp_offset_visitor in
+  visitCilExpr visitor
+
 class exp_deep_unroll_types_visitor = object
   inherit nopCilVisitor
   method! vtype (t: typ) =