Relax disjoint check for globals and fresh pointers.

intTests/test_llvm_global_fresh_pointer/test.c

@@ -0,0 +1,8 @@
+int glb;
+
+void foo(const int *x) {}
+
+void bar(const int *x) {
+  foo(x);
+}
+

intTests/test_llvm_global_fresh_pointer/test.saw

@@ -0,0 +1,29 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let foo_spec = do {
+  llvm_alloc_global "glb";
+  x_ptr <- llvm_fresh_pointer (llvm_int 32);
+
+  llvm_execute_func [x_ptr];
+};
+
+foo_ov <- llvm_verify m "foo"
+  []
+  false
+  foo_spec
+  (do {
+    print_goal;
+    w4_unint_z3 [];
+  });
+
+llvm_verify m "bar"
+  [foo_ov]
+  false
+  foo_spec
+  (do {
+    print_goal;
+    w4_unint_z3 [];
+  });
+

intTests/test_llvm_global_fresh_pointer/test.sh

@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+

src/SAWScript/Crucible/LLVM/Override.hs

@@ -1044,8 +1044,11 @@ enforceDisjointAllocGlobal ::
   (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) ->
   OverrideMatcher (LLVM arch) md ()
 enforceDisjointAllocGlobal sym loc
-  (LLVMAllocSpec _pmut _pty _palign psz pMd _pfresh _p_sym_init, p)
-  (LLVMAllocGlobal qloc (L.Symbol qname), q) =
+  (LLVMAllocSpec _pmut _pty _palign psz pMd pfresh _p_sym_init, p)
+  (LLVMAllocGlobal qloc (L.Symbol qname), q)
+  | pfresh =
+    pure () -- Fresh pointers need not be disjoint
+  | otherwise =
   do let Crucible.LLVMPointer pblk _ = p
      let Crucible.LLVMPointer qblk _ = q
      c <- liftIO $ W4.notPred sym =<< W4.natEq sym pblk qblk