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

1 files changed, 5 insertions, 5 deletions

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index cb2f132c..e7debfcb 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -30,7 +30,7 @@ Open Scope error_monad_scope.
 (** To evaluate constant expressions at compile-time, we use the same [value]
   type and the same [sem_*] functions that are used in CompCert C's semantics
   (module [Csem]).  However, we interpret pointer values symbolically:
-  [Vptr (Zpos id) ofs] represents the address of global variable [id]
+  [Vptr id ofs] represents the address of global variable [id]
   plus byte offset [ofs]. *)
 
 (** [constval a] evaluates the constant expression [a].
@@ -111,7 +111,7 @@ Fixpoint constval (a: expr) : res val :=
   | Ecomma r1 r2 ty =>
       do v1 <- constval r1; constval r2
   | Evar x ty =>
-      OK(Vptr (Zpos x) Int.zero)
+      OK(Vptr x Int.zero)
   | Ederef r ty =>
       constval r
   | Efield l f ty =>
@@ -155,9 +155,9 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   | Vlong n, Tlong _ _ => OK(Init_int64 n)
   | Vfloat f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
-  | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
-  | Vptr (Zpos id) ofs, Tpointer _ _ => OK(Init_addrof id ofs)
-  | Vptr (Zpos id) ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs)
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
   end.