From 765cede114cdcd4afa883324096baad0489ff59e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 4 Sep 2025 15:25:37 +0300
Subject: [PATCH 1/5] Add __fpending from coreutils-v8.31/comm_3args_ok.c to
 library functions

---
 src/util/library/libraryFunctions.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 2cd7e57d5b..63c1f10b44 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -642,6 +642,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
     ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("clearerr_unlocked", unknown [drop "stream" [w]]); (* TODO: why only w? *)
+    ("__fpending", unknown [drop "stream" [r_deep]]);
     ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
     ("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
     ("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));

From edfcbd3a29601aee701877f32cceda268f7d237e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 4 Sep 2025 15:31:39 +0300
Subject: [PATCH 2/5] Add test 56-witness/71-var_eq-str-invariant (issue #1722)

---
 .../56-witness/71-var_eq-str-invariant.c      |  5 ++++
 .../56-witness/71-var_eq-str-invariant.t      | 25 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 tests/regression/56-witness/71-var_eq-str-invariant.c
 create mode 100644 tests/regression/56-witness/71-var_eq-str-invariant.t

diff --git a/tests/regression/56-witness/71-var_eq-str-invariant.c b/tests/regression/56-witness/71-var_eq-str-invariant.c
new file mode 100644
index 0000000000..afb83b1ed3
--- /dev/null
+++ b/tests/regression/56-witness/71-var_eq-str-invariant.c
@@ -0,0 +1,5 @@
+// CRAM PARAM: --set ana.activated[+] var_eq
+int main() {
+  char text = "foobar";
+  return 0;
+}
diff --git a/tests/regression/56-witness/71-var_eq-str-invariant.t b/tests/regression/56-witness/71-var_eq-str-invariant.t
new file mode 100644
index 0000000000..4f7d010617
--- /dev/null
+++ b/tests/regression/56-witness/71-var_eq-str-invariant.t
@@ -0,0 +1,25 @@
+  $ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 71-var_eq-str-invariant.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3
+  [Info][Witness] witness generation summary:
+    location invariants: 1
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+Should not contain invariant with string literal equality:
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 71-var_eq-str-invariant.c
+          line: 4
+          column: 3
+          function: main
+        value: '"foobar" == text'
+        format: c_expression

From 28f8f76e68b148c39536ee9a0ccd1b662eeef1bf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 4 Sep 2025 15:32:46 +0300
Subject: [PATCH 3/5] Exclude string constant equality invariants from var_eq
 (issue #1722)

---
 src/analyses/varEq.ml                               |  6 +++++-
 .../regression/56-witness/71-var_eq-str-invariant.t | 13 ++-----------
 2 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 196ff2767f..cb9895efe0 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -17,6 +17,10 @@ struct
   struct
     include PartitionDomain.ExpPartitions
 
+    let is_str_constant = function
+      | Const (CStr _ | CWStr _) -> true
+      | _ -> false
+
     let invariant ~scope ss =
       fold (fun s a ->
           if B.mem MyCFG.unknown_exp s then
@@ -25,7 +29,7 @@ struct
             let module B_prod = BatSet.Make2 (Exp) (Exp) in
             let s_prod = B_prod.cartesian_product s s in
             let i = B_prod.Product.fold (fun (x, y) a ->
-                if Exp.compare x y < 0 && not (InvariantCil.exp_contains_tmp x) && not (InvariantCil.exp_contains_tmp y) && InvariantCil.exp_is_in_scope scope x && InvariantCil.exp_is_in_scope scope y then (* each equality only one way, no self-equalities *)
+                if Exp.compare x y < 0 && not (InvariantCil.exp_contains_tmp x) && not (InvariantCil.exp_contains_tmp y) && InvariantCil.exp_is_in_scope scope x && InvariantCil.exp_is_in_scope scope y && not (is_str_constant x) && not (is_str_constant y) then (* each equality only one way, no self-equalities *)
                   let eq = BinOp (Eq, x, y, intType) in
                   Invariant.(a && of_exp eq)
                 else
diff --git a/tests/regression/56-witness/71-var_eq-str-invariant.t b/tests/regression/56-witness/71-var_eq-str-invariant.t
index 4f7d010617..222e4e7497 100644
--- a/tests/regression/56-witness/71-var_eq-str-invariant.t
+++ b/tests/regression/56-witness/71-var_eq-str-invariant.t
@@ -4,7 +4,7 @@
     dead: 0
     total lines: 3
   [Info][Witness] witness generation summary:
-    location invariants: 1
+    location invariants: 0
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -13,13 +13,4 @@ Should not contain invariant with string literal equality:
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: invariant_set
-    content:
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 71-var_eq-str-invariant.c
-          line: 4
-          column: 3
-          function: main
-        value: '"foobar" == text'
-        format: c_expression
+    content: []

From e39b40c497b6deb7d19fdfb7c0ea5919c88d0caa Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 4 Sep 2025 15:38:52 +0300
Subject: [PATCH 4/5] Add test 56-witness/72-shadowing-invariant (issue #1722)

---
 .../56-witness/72-shadowing-invariant.c       |  13 ++
 .../56-witness/72-shadowing-invariant.t       | 161 ++++++++++++++++++
 2 files changed, 174 insertions(+)
 create mode 100644 tests/regression/56-witness/72-shadowing-invariant.c
 create mode 100644 tests/regression/56-witness/72-shadowing-invariant.t

diff --git a/tests/regression/56-witness/72-shadowing-invariant.c b/tests/regression/56-witness/72-shadowing-invariant.c
new file mode 100644
index 0000000000..aff8c2888c
--- /dev/null
+++ b/tests/regression/56-witness/72-shadowing-invariant.c
@@ -0,0 +1,13 @@
+// CRAM PARAM: --set ana.activated[+] var_eq
+
+int foo = 1;
+
+int main() {
+  int foo = 2; // shadows global
+
+  int bar = 3;
+  {
+    int bar = 4; // shadows outer block
+    return 0;
+  }
+}
diff --git a/tests/regression/56-witness/72-shadowing-invariant.t b/tests/regression/56-witness/72-shadowing-invariant.t
new file mode 100644
index 0000000000..ea1d0af53f
--- /dev/null
+++ b/tests/regression/56-witness/72-shadowing-invariant.t
@@ -0,0 +1,161 @@
+  $ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 72-shadowing-invariant.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5
+  [Info][Witness] witness generation summary:
+    location invariants: 16
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+Should not contain invariants containing shadowed variables.
+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:
+          file_name: 72-shadowing-invariant.c
+          line: 8
+          column: 3
+          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:
+          file_name: 72-shadowing-invariant.c
+          line: 8
+          column: 3
+          function: main
+        value: foo == 2
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 72-shadowing-invariant.c
+          line: 10
+          column: 5
+          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:
+          file_name: 72-shadowing-invariant.c
+          line: 10
+          column: 5
+          function: main
+        value: foo == 2
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 72-shadowing-invariant.c
+          line: 11
+          column: 5
+          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:
+          file_name: 72-shadowing-invariant.c
+          line: 11
+          column: 5
+          function: main
+        value: foo == 2
+        format: c_expression

From 4e1a23e69784378132de81c3815aa431738e52c2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 4 Sep 2025 16:18:58 +0300
Subject: [PATCH 5/5] Exclude possibly shadowed variables from invariants
 (issue #1722)

---
 src/cdomain/value/domains/invariantCil.ml     | 18 +++-
 .../56-witness/72-shadowing-invariant.t       | 92 +------------------
 2 files changed, 14 insertions(+), 96 deletions(-)

diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index 9c2c79dfdb..ebe3be0acf 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/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
diff --git a/tests/regression/56-witness/72-shadowing-invariant.t b/tests/regression/56-witness/72-shadowing-invariant.t
index ea1d0af53f..d20e6d3a3d 100644
--- a/tests/regression/56-witness/72-shadowing-invariant.t
+++ b/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: