From 224ad3d40aa49deb9a73a3eceef0f1e5448fe85a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 31 Jul 2017 17:10:38 +0200
Subject: [PATCH] Make valid comparisons between pointers and 0.
---
theories/lang/lang.v | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 1dbd8ee6..6cf3ef52 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -220,7 +220,11 @@ Inductive lit_neq (σ : state) : base_lit → base_lit → Prop :=
| IntNeq z1 z2 :
z1 ≠ z2 → lit_neq σ (LitInt z1) (LitInt z2)
| LocNeq l1 l2 :
- l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2).
+ l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2)
+| LocNeqNullR l :
+ lit_neq σ (LitLoc l) (LitInt 0)
+| LocNeqNullL l :
+ lit_neq σ (LitInt 0) (LitLoc l).
Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
| BinOpPlus z1 z2 :
--
GitLab