Exclude possibly shadowed variables from invariants (issue #1722)

Author: sim642

src/cdomain/value/domains/invariantCil.ml

@@ -26,15 +26,23 @@ let exp_deep_unroll_types =
   let visitor = new exp_deep_unroll_types_visitor in
   visitCilExpr visitor
 
+let var_may_be_shadowed scope vi =
+  let vi_original_name = Cilfacade.find_original_name vi in
+  let local_may_shadow local =
+    not (CilType.Varinfo.equal vi local) && (* exclude self-equality by vid because the original names would always equal *)
+      vi_original_name = Cilfacade.find_original_name local
+  in
+  List.exists local_may_shadow scope.sformals || List.exists local_may_shadow scope.slocals
 
 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 *)
+  | None ->
+    vi.vstorage <> Static && (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
+      not (var_may_be_shadowed scope vi)
   | Some fd ->
-    if CilType.Fundec.equal fd scope then
-      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
-    else
-      false
+    CilType.Fundec.equal fd scope &&
+      (GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)) &&
+      not (var_may_be_shadowed scope vi) (* TODO: could distinguish non-nested and nested? *)
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

tests/regression/56-witness/72-shadowing-invariant.t

@@ -4,7 +4,7 @@
     dead: 0
     total lines: 5
   [Info][Witness] witness generation summary:
-    location invariants: 16
+    location invariants: 6
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -15,15 +15,6 @@ They can be wrong and contradicting.
   $ yamlWitnessStrip < witness.yml
   - entry_type: invariant_set
     content:
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 6
-          column: 3
-          function: main
-        value: foo == 1
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -33,15 +24,6 @@ They can be wrong and contradicting.
           function: main
         value: 2 == foo
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 8
-          column: 3
-          function: main
-        value: foo == 1
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -60,33 +42,6 @@ They can be wrong and contradicting.
           function: main
         value: 2 == foo
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 10
-          column: 5
-          function: main
-        value: 3 == bar
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 10
-          column: 5
-          function: main
-        value: bar == 3
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 10
-          column: 5
-          function: main
-        value: foo == 1
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -105,51 +60,6 @@ They can be wrong and contradicting.
           function: main
         value: 2 == foo
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 11
-          column: 5
-          function: main
-        value: 3 == bar
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 11
-          column: 5
-          function: main
-        value: 4 == bar
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 11
-          column: 5
-          function: main
-        value: bar == 3
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 11
-          column: 5
-          function: main
-        value: bar == 4
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 72-shadowing-invariant.c
-          line: 11
-          column: 5
-          function: main
-        value: foo == 1
-        format: c_expression
     - invariant:
         type: location_invariant
         location: