Merge pull request #1264 from goblint/base-special-lval

Do not invalidate special function lvals recursively
goblint · Nov 27, 2023 · 0fdea44 · 0fdea44
2 parents 975b502 + cb06f70
commit 0fdea44
Show file tree

Hide file tree

Showing 10 changed files with 14 additions and 31 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2132,7 +2132,7 @@ struct
     let invalidate_ret_lv st = match lv with
       | Some lv ->
         if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname;
-        invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
+        invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
       | None -> st
     in
     let addr_type_of_exp exp =

diff --git a/tests/regression/00-sanity/51-base-special-lval.c b/tests/regression/00-sanity/51-base-special-lval.c
@@ -0,0 +1,13 @@
+// Making sure special function lval is not invalidated recursively
+#include <goblint.h>
+
+extern int * anIntPlease();
+int main() {
+  int x = 0;
+  int *p = &x;
+  p = anIntPlease();
+
+  __goblint_check(x == 0); 
+
+  return 0;
+}
diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t
@@ -14,8 +14,6 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21)
   [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
@@ -39,8 +37,6 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21)
   [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)

diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t
@@ -15,11 +15,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:31:3-31:20)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:31:3-31:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:38:3-38:22)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:38:3-38:22)
   [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20)

diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t
@@ -15,11 +15,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:36:3-36:20)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:36:3-36:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:43:3-43:24)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:43:3-43:24)
   [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20)

diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t
@@ -15,11 +15,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:36:3-36:22)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:36:3-36:22)
   [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:43:3-43:24)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:43:3-43:24)
   [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22)

diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t
@@ -17,11 +17,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:31:3-31:20)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:31:3-31:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:39:3-39:17)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:39:3-39:17)
   [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20)

diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t
@@ -17,11 +17,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:32:3-32:17)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:32:3-32:17)
   [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:40:3-40:17)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:40:3-40:17)
   [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17)

diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t
@@ -17,11 +17,7 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:36:3-36:20)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:36:3-36:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20)
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:44:3-44:17)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:44:3-44:17)
   [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20)

diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t
@@ -16,8 +16,6 @@
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:13:3-13:29)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:13:3-13:29)
   [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29)
   [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29)