Skip to content

Commit ed4ce85

Browse files
committed
Fix imprecise AD.meet with NULL (closes #566)
1 parent 304cfd6 commit ed4ce85

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

src/cdomains/addressDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ struct
125125
else remove Addr.NullPtr x
126126
in
127127
match is_top x, is_top y with
128-
| true, true -> uop x y
128+
| true, true -> no_null (no_null (uop x y) x) y
129129
| false, true -> no_null x y
130130
| true, false -> no_null y x
131131
| false, false -> cop x y

tests/regression/27-inv_invariants/15-unknown-null-ptr.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ int main() {
66
if (r == NULL)
77
assert(r == NULL);
88
else
9-
assert(r != NULL); // TODO
9+
assert(r != NULL);
1010

1111
if (r != NULL)
12-
assert(r != NULL); // TODO
12+
assert(r != NULL);
1313
else
1414
assert(r == NULL);
1515

0 commit comments

Comments
 (0)