Make comparison of pointers amenable to meet if they only differ in offsets

Author: michael-schwarz

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

tests/regression/27-inv_invariants/22-meet-ptrs.c

@@ -0,0 +1,24 @@
+//PARAM:  --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+
+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;
+}