Skip to content

Commit 21d4c8d

Browse files
Test 85/21: Comment on perhaps surprising lack of precision
1 parent e250672 commit 21d4c8d

File tree

1 file changed

+6
-3
lines changed

1 file changed

+6
-3
lines changed

tests/regression/85-narrow_globs/21-dead-escape.c

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,10 @@ void* f(void *d) {
2222
// so none of these unknowns are queried and this check
2323
// succeeds whether eliminate-dead is on or not.
2424
__goblint_check(i == 1);
25-
// Paradoxically, a != &i is not known without eliminate-dead.
25+
// a != &i is not known without eliminate-dead
26+
// The pointer has escaped at some point and was recorded at the global a.
27+
// We don't filter points-to-sets read from globals to exclude things which are locally known (by the ThreadEscape analysis) to not have escaped.
28+
// I don't think this is particularly common, and iterating and querying for each lval is probably just expensive.
2629
__goblint_check(a != &i);
2730
return NULL;
2831
}
@@ -34,6 +37,6 @@ int main(void) {
3437
// a is thought to (possibly) point to the *flow-insensitively* tracked i,
3538
// which is widened by the i++.
3639
__goblint_check(*a <= 1);
37-
40+
3841
return 0;
39-
}
42+
}

0 commit comments

Comments
 (0)