From 8d2e4096a206571117096c092bf3477809f37d29 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Sep 2017 14:21:46 +0200
Subject: [PATCH] document pointer comparison non-determinism
---
theories/lang/lang.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index e3c8981a..3e86445f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -216,6 +216,13 @@ Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
| IntRefl z : lit_eq σ (LitInt z) (LitInt z)
| LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
+(* Comparing unallocated pointers can non-deterministically say they are equal
+ even if they are not. Given that our `free` actually makes addresses
+ re-usable, this may not be strictly necessary, but it is the most
+ conservative choice that avoids UB (and we cannot use UB as this operation is
+ possible in safe Rust). See
+ <https://internals.rust-lang.org/t/comparing-dangling-pointers/3019> for some
+ more background. *)
| LocUnallocL l1 l2 :
σ !! l1 = None →
lit_eq σ (LitLoc l1) (LitLoc l2)
--
GitLab