Exclude __annonCompField offsets from witness invariants

Author: sim642

src/cdomain/value/domains/invariantCil.ml

@@ -91,11 +91,35 @@ let exp_contains_tmp e =
   !acc
 
 
+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_contains_anon_comp_offset = function
+  | NoOffset -> false
+  | Index (e, offs') -> offset_contains_anon_comp_offset offs' (* does not check e!, done by visitor *)
+  | Field (fi, offs') -> fieldinfo_is_anon fi || offset_contains_anon_comp_offset offs'
+
+class exp_contains_anon_comp_offset_visitor = object
+  inherit nopCilVisitor
+  method! voffs (offs: offset) =
+    if offset_contains_anon_comp_offset offs then
+      raise Stdlib.Exit
+    else
+      DoChildren (* recurse to Index offset expressions! *)
+end
+let exp_contains_anon_comp_offset =
+  let visitor = new exp_contains_anon_comp_offset_visitor in
+  fun e ->
+    match visitCilExpr visitor e with
+    | _ -> false
+    | exception Stdlib.Exit -> true
+
+
 let var_is_suitable ?scope v =
   not (var_is_tmp v) && GobOption.for_all (fun scope -> var_is_in_scope scope v) scope
 
 let exp_is_suitable ?scope e =
-  not (exp_contains_tmp e) && GobOption.for_all (fun scope -> exp_is_in_scope scope e) scope
+  not (exp_contains_tmp e || exp_contains_anon_comp_offset e) && GobOption.for_all (fun scope -> exp_is_in_scope scope e) scope
 
 
 class exp_contains_anon_type_visitor = object