diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index 52e48e5612..1a09aed026 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -112,6 +112,7 @@ struct let amenable_to_meet x y = match x,y with | StrPtr _, StrPtr _ -> true + | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true | _ -> false let leq x y = match x, y with diff --git a/tests/regression/27-inv_invariants/22-meet-ptrs.c b/tests/regression/27-inv_invariants/22-meet-ptrs.c new file mode 100644 index 0000000000..33adfa879f --- /dev/null +++ b/tests/regression/27-inv_invariants/22-meet-ptrs.c @@ -0,0 +1,24 @@ +//PARAM: --enable ana.int.interval +#include +#include +#include + + +int main() { + int arr[20]; + + int top; + + int i = 2; + if(top) { + i = 8; + } + + int* imprecise = &arr[i]; + + if(imprecise == &arr[2]) { + __goblint_check(imprecise == &arr[2]); + } + + return 0; +}