Exclude witness invariants with __anon structs

src/cdomain/value/domains/invariantCil.ml

@@ -84,6 +84,22 @@ let exp_contains_tmp e =
   ignore (visitCilExpr visitor e);
   !acc
 
+class exp_contains_anon_type_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    match t with
+    | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname ->
+      raise Stdlib.Exit
+    | _ ->
+      DoChildren
+end
+let exp_contains_anon_type e = (* TODO: curry to create object only once *)
+  let visitor = new exp_contains_anon_type_visitor in
+  match visitCilExpr visitor e with
+  | _ -> false
+  | exception Stdlib.Exit -> true
+
+
 (* TODO: synchronize magic constant with BaseDomain *)
 let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
 

src/witness/witnessUtil.ml

@@ -167,6 +167,7 @@ struct
     in
     if GobConfig.get_bool "witness.invariant.split-conjunction" then
       ES.elements (pullOutCommonConjuncts inv')
+      |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
     else
       [inv']
 end

tests/regression/witness/typedef.t/run.t

@@ -4,7 +4,7 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
-    total generation entries: 14
+    total generation entries: 13
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: location_invariant
@@ -62,17 +62,6 @@
       string: '*((int *)p) == 42'
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: typedef.c
-      file_hash: $FILE_HASH
-      line: 14
-      column: 2
-      function: main
-    location_invariant:
-      string: ((struct __anonstruct_s_109580352 *)q)->f == 43
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: typedef.c