From 3eff22f8eb8b6858e5c9753548a02c7f69554381 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 15 May 2024 16:08:53 +0200
Subject: [PATCH] Make comparison of pointers amenable to `meet` if they only
 differ in offsets

---
 src/cdomain/value/cdomains/addressDomain.ml   |  1 +
 .../27-inv_invariants/22-meet-ptrs.c          | 24 +++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 tests/regression/27-inv_invariants/22-meet-ptrs.c

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 <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;
+}