Unroll typedefs for witness invariants

We have problems parsing them for validation: goblint/cil#159.

src/cdomain/value/domains/invariantCil.ml

@@ -13,15 +13,24 @@ class exp_replace_original_name_visitor = object
   method! vvrbl (vi: varinfo) =
     ChangeTo (var_replace_original_name vi)
 end
-let exp_replace_original_name e =
+let exp_replace_original_name e = (* TODO: curry to create object only once *)
   let visitor = new exp_replace_original_name_visitor in
   visitCilExpr visitor e
 
+class exp_deep_unroll_types_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    ChangeTo (unrollTypeDeep t)
+end
+let exp_deep_unroll_types =
+  let visitor = new exp_deep_unroll_types_visitor in
+  visitCilExpr visitor
+
 
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> 
+  | Some fd ->
     if CilType.Fundec.equal fd scope then
       GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
     else

src/witness/witnessUtil.ml

@@ -160,7 +160,11 @@ struct
     | e -> to_conjunct_set e
 
   let process_exp inv =
-    let inv' = InvariantCil.exp_replace_original_name inv in
+    let inv' =
+      inv
+      |> InvariantCil.exp_deep_unroll_types
+      |> InvariantCil.exp_replace_original_name
+    in
     if GobConfig.get_bool "witness.invariant.split-conjunction" then
       ES.elements (pullOutCommonConjuncts inv')
     else

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

@@ -59,7 +59,7 @@
       column: 2
       function: main
     location_invariant:
-      string: '*((myint *)p) == 42'
+      string: '*((int *)p) == 42'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -70,7 +70,7 @@
       column: 2
       function: main
     location_invariant:
-      string: ((s *)q)->f == 43
+      string: ((struct __anonstruct_s_109580352 *)q)->f == 43
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -114,7 +114,7 @@
       column: 2
       function: main
     location_invariant:
-      string: '*((myint *)p) == 42'
+      string: '*((int *)p) == 42'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -147,7 +147,7 @@
       column: 2
       function: main
     location_invariant:
-      string: '*((myint *)p) == 42'
+      string: '*((int *)p) == 42'
       type: assertion
       format: C
   - entry_type: location_invariant