From 8a64451e6f474d20a469b939a938577bbe6d3d66 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 9 Mar 2012 09:52:04 +0000
Subject: Merge of Andrew Tolmach's HASP-related changes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Memtype.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'common/Memtype.v')

diff --git a/common/Memtype.v b/common/Memtype.v
index f7635816..2e44331f 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -1159,6 +1159,16 @@ Axiom free_inject:
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 
+Axiom drop_outside_inject:
+  forall f m1 m2 b lo hi p m2',
+  inject f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  inject f m1 m2'.
+
 (** Memory states that inject into themselves. *)
 
 Definition flat_inj (thr: block) : meminj :=
-- 
cgit