diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 5b9a00313e..bdae887b4a 100644 --- 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 new file mode 100644 index 0000000000..8f74a1babe --- /dev/null +++ b/tests/regression/00-sanity/51-base-special-lval.c @@ -0,0 +1,13 @@ +// Making sure special function lval is not invalidated recursively +#include + +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 index 4c105d1559..4b8118eec1 100644 --- 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 index bb935cb0ed..68d9cdb779 100644 --- 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 index ba1399d225..85f7bfb709 100644 --- 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 index 71bdcfb2e2..a2e9e2ab15 100644 --- 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 index 46435045b9..a3b5faf083 100644 --- 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 index c7e66c0527..5773245114 100644 --- 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 index 4fc1c7e101..798374d63c 100644 --- 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 index bf34d99936..07999854ff 100644 --- 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)