diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml index ef0687d6eb..0419bc2d65 100644 --- a/src/cdomain/value/domains/invariantCil.ml +++ b/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 diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 6c02546168..0e57132c8e 100644 --- a/src/witness/witnessUtil.ml +++ b/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 diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index 62f8409048..27f4a5f5a3 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/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