From c85b6a585073f3fc7c8e34fbd78c613bf619cbeb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 18 Jul 2015 16:01:12 +0200
Subject: Missing case in ValueDomain.pincl, causing incompleteness.

---
 backend/ValueDomain.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'backend/ValueDomain.v')

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 3d0196d3..0de17745 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -301,6 +301,7 @@ Definition pincl (p q: aptr) : bool :=
   | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true
   | Stk ofs1, Stk ofs2 => Int.eq_dec ofs1 ofs2
   | Stk ofs1, Stack => true
+  | Stack, Stack => true
   | _, Ptop => true
   | _, _ => false
   end.
@@ -311,6 +312,14 @@ Proof.
   InvBooleans; subst; auto with va.
 Qed.
 
+Lemma pincl_ge_2: forall p q, pge p q -> pincl q p = true.
+Proof.
+  destruct 1; simpl; auto.
+- destruct p; auto.
+- destruct p; simpl; auto; rewrite ! proj_sumbool_is_true; auto.
+- rewrite ! proj_sumbool_is_true; auto.
+Qed.
+
 Lemma pincl_sound:
   forall b ofs p q,
   pincl p q = true -> pmatch b ofs p -> pmatch b ofs q.
-- 
cgit