From b40e056328e183522b50c68aefdbff057bca29cc Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 16 Jun 2013 06:56:02 +0000
Subject: Merge of the "princeton" branch: - Define type "block" as "positive"
 instead of "Z". - Strengthen mem_unchanged_on so that the permissions are
 identical,   instead of possibly increasing. - Move mem_unchanged_on from
 Events to Memory.Mem. - Define it in terms of mem_contents rather than in
 terms of Mem.load. - ExportClight: try to name temporaries introduced by
 SimplExpr - SimplExpr: avoid reusing temporaries between different functions,
   instead, thread a single generator through all functions.

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

(limited to 'common/Memtype.v')

diff --git a/common/Memtype.v b/common/Memtype.v
index 59dc7a3..37ab33c 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -88,8 +88,6 @@ Module Type MEM.
 (** The abstract type of memory states. *)
 Parameter mem: Type.
 
-Definition nullptr: block := 0.
-
 (** * Operations on memory states *)
 
 (** [empty] is the initial memory state. *)
@@ -176,11 +174,9 @@ Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), opti
   block. *)
 
 Parameter nextblock: mem -> block.
-Axiom nextblock_pos:
-  forall m, nextblock m > 0.
 
-Definition valid_block (m: mem) (b: block) :=
-  b < nextblock m.
+Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
+
 Axiom valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
 
@@ -279,7 +275,7 @@ Axiom valid_pointer_implies:
 
 (** ** Properties of the initial memory state. *)
 
-Axiom nextblock_empty: nextblock empty = 1.
+Axiom nextblock_empty: nextblock empty = 1%positive.
 Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Axiom valid_access_empty:
   forall chunk b ofs p, ~valid_access empty chunk b ofs p.
@@ -607,7 +603,7 @@ Axiom alloc_result:
 
 Axiom nextblock_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  nextblock m2 = Zsucc (nextblock m1).
+  nextblock m2 = Psucc (nextblock m1).
 
 Axiom valid_block_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
@@ -640,7 +636,7 @@ Axiom perm_alloc_inv:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
   forall b' ofs k p, 
   perm m2 b' ofs k p ->
-  if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p.
+  if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
 
 (** Effect of [alloc] on access validity. *)
 
@@ -1191,7 +1187,7 @@ Axiom drop_outside_inject:
 (** Memory states that inject into themselves. *)
 
 Definition flat_inj (thr: block) : meminj :=
-  fun (b: block) => if zlt b thr then Some(b, 0) else None.
+  fun (b: block) => if plt b thr then Some(b, 0) else None.
 
 Parameter inject_neutral: forall (thr: block) (m: mem), Prop.
 
@@ -1206,14 +1202,14 @@ Axiom alloc_inject_neutral:
   forall thr m lo hi b m',
   alloc m lo hi = (m', b) ->
   inject_neutral thr m ->
-  nextblock m < thr ->
+  Plt (nextblock m) thr ->
   inject_neutral thr m'.
 
 Axiom store_inject_neutral:
   forall chunk m b ofs v m' thr,
   store chunk m b ofs v = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   val_inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 
@@ -1221,7 +1217,7 @@ Axiom drop_inject_neutral:
   forall m b lo hi p m' thr,
   drop_perm m b lo hi p = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   inject_neutral thr m'.
 
 End MEM.
-- 
cgit v1.2.3