Skip to content

Commit 7f60099

Browse files
Explain why if is needed and what is checked
1 parent 004e3ae commit 7f60099

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

tests/regression/13-privatized/89-write-lacking-precision.c

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,10 @@ struct a h = {""};
99
struct a i = {"string"};
1010

1111
void* d(void* args) {
12-
struct a r;
1312
if (c->b) {
14-
__goblint_check(strlen(h.b) == 0); // Should also work for write!
13+
// Handled by privatization as a write
14+
// Without fix (#1468) causes both h.b and i.b to become unknown string
15+
__goblint_check(strlen(h.b) == 0); // Check h.b is still known
1516
}
1617
}
1718

0 commit comments

Comments
 (0)