Merge pull request #145 from AbsInt/64

Support for 64-bit target processors + support for x86 in 64-bit mode

19 files changed, 1300 insertions, 967 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 5d75aa6a..a1ca48d1 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -197,7 +197,7 @@ let builtins_generic = {
           false);
     "__compcert_va_composite",
         (TPtr(TVoid [], []),
-          [TPtr(TVoid [], []); TInt(IUInt, [])],
+          [TPtr(TVoid [], []); TInt(IULong, [])],
           false);
   (* Helper functions for int64 arithmetic *)
     "__i64_dtos",
@@ -251,6 +251,14 @@ let builtins_generic = {
     "__i64_sar",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_smulh",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_umulh",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
          false)
   ]
 }
@@ -393,14 +401,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg =
 
 let make_builtin_va_arg_by_ref helper ty arg =
   let ty_fun =
-    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil),
+    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tcons(Ctyping.size_t, Tnil)),
               Tpointer(Tvoid, noattr), cc_default) in
   let ty_ptr =
     Tpointer(ty, noattr) in
   let call =
     Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
-          Econs(va_list_ptr arg,
-                Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)),
+          Econs(va_list_ptr arg, Econs(Esizeof(ty, Ctyping.size_t), Enil)),
           Tpointer(Tvoid, noattr)) in
   Evalof(Ederef(Ecast(call, ty_ptr), ty), ty)
 
@@ -445,27 +452,31 @@ let convertCallconv va unproto attr =
 
 (** Types *)
 
-let convertIkind = function
-  | C.IBool -> (Unsigned, Ctypes.IBool)
-  | C.IChar -> ((if (!Machine.config).Machine.char_signed
-                 then Signed else Unsigned), I8)
-  | C.ISChar -> (Signed, I8)
-  | C.IUChar -> (Unsigned, I8)
-  | C.IInt -> (Signed, I32)
-  | C.IUInt -> (Unsigned, I32)
-  | C.IShort -> (Signed, I16)
-  | C.IUShort -> (Unsigned, I16)
-  | C.ILong -> (Signed, I32)
-  | C.IULong -> (Unsigned, I32)
-  (* Special-cased in convertTyp below *)
-  | C.ILongLong | C.IULongLong -> assert false
-
-let convertFkind = function
-  | C.FFloat -> F32
-  | C.FDouble -> F64
+let convertIkind k a : coq_type =
+    match k with
+  | C.IBool -> Tint (IBool, Unsigned, a)
+  | C.IChar -> Tint (I8, (if Machine.((!config).char_signed)
+                          then Signed else Unsigned), a)
+  | C.ISChar -> Tint (I8, Signed, a)
+  | C.IUChar -> Tint (I8, Unsigned, a)
+  | C.IInt -> Tint (I32, Signed, a)
+  | C.IUInt -> Tint (I32, Unsigned, a)
+  | C.IShort -> Tint (I16, Signed, a)
+  | C.IUShort -> Tint (I16, Unsigned, a)
+  | C.ILong -> if Machine.((!config).sizeof_long) = 8
+               then Tlong (Signed, a) else Tint (I32, Signed, a)
+  | C.IULong -> if Machine.((!config).sizeof_long) = 8
+                then Tlong (Unsigned, a) else Tint (I32, Unsigned, a)
+  | C.ILongLong -> Tlong (Signed, a)
+  | C.IULongLong -> Tlong (Unsigned, a)
+
+let convertFkind k a : coq_type =
+  match k with
+  | C.FFloat -> Tfloat (F32, a)
+  | C.FDouble -> Tfloat (F64, a)
   | C.FLongDouble ->
       if not !Clflags.option_flongdouble then unsupported "'long double' type";
-      F64
+      Tfloat (F64, a)
 
 let checkFunctionType env tres targs =
   if not !Clflags.option_fstruct_passing then begin
@@ -485,14 +496,10 @@ let checkFunctionType env tres targs =
 let rec convertTyp env t =
   match t with
   | C.TVoid a -> Tvoid
-  | C.TInt(C.ILongLong, a) ->
-      Tlong(Signed, convertAttr a)
-  | C.TInt(C.IULongLong, a) ->
-      Tlong(Unsigned, convertAttr a)
   | C.TInt(ik, a) ->
-      let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a)
+      convertIkind ik (convertAttr a)
   | C.TFloat(fk, a) ->
-      Tfloat(convertFkind fk, convertAttr a)
+      convertFkind fk (convertAttr a)
   | C.TPtr(ty, a) ->
       Tpointer(convertTyp env ty, convertAttr a)
   | C.TArray(ty, None, a) ->
@@ -517,8 +524,7 @@ let rec convertTyp env t =
   | C.TUnion(id, a) ->
       Tunion(intern_string id.name, convertAttr a)
   | C.TEnum(id, a) ->
-      let (sg, sz) = convertIkind Cutil.enum_ikind in
-      Tint(sz, sg, convertAttr a)
+      convertIkind Cutil.enum_ikind (convertAttr a)
 
 and convertParams env = function
     | [] -> Tnil
@@ -653,7 +659,7 @@ let rec convertExpr env e =
 
   | C.EConst(C.CInt(i, k, _)) ->
       let sg = if Cutil.is_signed_ikind k then Signed else Unsigned in
-      if k = ILongLong || k = IULongLong
+      if Cutil.sizeof_ikind k = 8
       then Ctyping.econst_long (coqint_of_camlint64 i) sg
       else Ctyping.econst_int (convertInt i) sg
   | C.EConst(C.CFloat(f, k)) ->
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index a2bfa6e1..4dcf2a47 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -12,25 +12,11 @@
 
 (** Animating the CompCert C semantics *)
 
-Require Import String.
-Require Import Axioms.
-Require Import Classical.
-Require Import Decidableplus.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Determinism.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
+Require Import Axioms Classical.
+Require Import String Coqlib Decidableplus.
+Require Import Errors Maps Integers Floats.
+Require Import AST Values Memory Events Globalenvs Determinism.
+Require Import Ctypes Cop Csyntax Csem.
 Require Cstrategy.
 
 Local Open Scope string_scope.
@@ -74,7 +60,7 @@ Proof.
   intros until ty. destruct a; simpl; congruence.
 Qed.
 
-Definition is_loc (a: expr) : option (block * int * type) :=
+Definition is_loc (a: expr) : option (block * ptrofs * type) :=
   match a with
   | Eloc b ofs ty => Some(b, ofs, ty)
   | _ => None
@@ -106,16 +92,17 @@ Section EXEC.
 Variable ge: genv.
 
 Definition eventval_of_val (v: val) (t: typ) : option eventval :=
-  match v, t with
-  | Vint i, AST.Tint => Some (EVint i)
-  | Vfloat f, AST.Tfloat => Some (EVfloat f)
-  | Vsingle f, AST.Tsingle => Some (EVsingle f)
-  | Vlong n, AST.Tlong => Some (EVlong n)
-  | Vptr b ofs, AST.Tint =>
+  match v with
+  | Vint i => check (typ_eq t AST.Tint); Some (EVint i)
+  | Vfloat f => check (typ_eq t AST.Tfloat); Some (EVfloat f)
+  | Vsingle f => check (typ_eq t AST.Tsingle); Some (EVsingle f)
+  | Vlong n => check (typ_eq t AST.Tlong); Some (EVlong n)
+  | Vptr b ofs =>
       do id <- Genv.invert_symbol ge b;
       check (Genv.public_symbol ge id);
+      check (typ_eq t AST.Tptr);
       Some (EVptr_global id ofs)
-  | _, _ => None
+  | _ => None
   end.
 
 Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
@@ -129,32 +116,45 @@ Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list event
   end.
 
 Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
-  match ev, t with
-  | EVint i, AST.Tint => Some (Vint i)
-  | EVfloat f, AST.Tfloat => Some (Vfloat f)
-  | EVsingle f, AST.Tsingle => Some (Vsingle f)
-  | EVlong n, AST.Tlong => Some (Vlong n)
-  | EVptr_global id ofs, AST.Tint =>
+  match ev with
+  | EVint i => check (typ_eq t AST.Tint); Some (Vint i)
+  | EVfloat f => check (typ_eq t AST.Tfloat); Some (Vfloat f)
+  | EVsingle f => check (typ_eq t AST.Tsingle); Some (Vsingle f)
+  | EVlong n => check (typ_eq t AST.Tlong); Some (Vlong n)
+  | EVptr_global id ofs =>
       check (Genv.public_symbol ge id);
+      check (typ_eq t AST.Tptr);
       do b <- Genv.find_symbol ge id;
       Some (Vptr b ofs)
-  | _, _ => None
+  end.
+
+Ltac mydestr :=
+  match goal with
+  | [ |- None = Some _ -> _ ] => intro X; discriminate
+  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
+  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
+  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
+  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
+  | _ => idtac
   end.
 
 Lemma eventval_of_val_sound:
   forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.
 Proof.
-  intros. destruct v; destruct t; simpl in H; inv H; try constructor.
-  destruct (Genv.invert_symbol ge b) as [id|] eqn:?; try discriminate.
-  destruct (Genv.public_symbol ge id) eqn:?; inv H1.
-  constructor. auto. apply Genv.invert_find_symbol; auto.
+  intros until ev. destruct v; simpl; mydestr; constructor.
+  auto. apply Genv.invert_find_symbol; auto.
 Qed.
 
 Lemma eventval_of_val_complete:
   forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
 Proof.
-  induction 1; simpl; auto.
-  rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto.
+  induction 1; simpl.
+- auto.
+- auto.
+- auto.
+- auto.
+- rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H.
+  rewrite dec_eq_true. auto. 
 Qed.
 
 Lemma list_eventval_of_val_sound:
@@ -177,21 +177,23 @@ Qed.
 Lemma val_of_eventval_sound:
   forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.
 Proof.
-  intros. destruct ev; destruct t; simpl in H; inv H; try constructor.
-  destruct (Genv.public_symbol ge i) eqn:?; try discriminate.
-  destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
-  constructor; auto.
+  intros until v. destruct ev; simpl; mydestr; constructor; auto.
 Qed.
 
 Lemma val_of_eventval_complete:
   forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
 Proof.
-  induction 1; simpl; auto. simpl in *. rewrite H, H0; auto.
+  induction 1; simpl.
+- auto.
+- auto.
+- auto.
+- auto.
+- simpl in *. rewrite H, H0. rewrite dec_eq_true. auto.  
 Qed.
 
 (** Volatile memory accesses. *)
 
-Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int)
+Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs)
                              : option (world * trace * val) :=
   if Genv.block_is_volatile ge b then
     do id <- Genv.invert_symbol ge b;
@@ -202,10 +204,10 @@ Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block)
         Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres)
     end
   else
-    do v <- Mem.load chunk m b (Int.unsigned ofs);
+    do v <- Mem.load chunk m b (Ptrofs.unsigned ofs);
     Some(w, E0, v).
 
-Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) (v: val)
+Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs) (v: val)
                              : option (world * trace * mem) :=
   if Genv.block_is_volatile ge b then
     do id <- Genv.invert_symbol ge b;
@@ -213,19 +215,9 @@ Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block
     do w' <- nextworld_vstore w chunk id ofs ev;
     Some(w', Event_vstore chunk id ofs ev :: nil, m)
   else
-    do m' <- Mem.store chunk m b (Int.unsigned ofs) v;
+    do m' <- Mem.store chunk m b (Ptrofs.unsigned ofs) v;
     Some(w, E0, m').
 
-Ltac mydestr :=
-  match goal with
-  | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate
-  | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X
-  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
-  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
-  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
-  | _ => idtac
-  end.
-
 Lemma do_volatile_load_sound:
   forall w chunk m b ofs w' t v,
   do_volatile_load w chunk m b ofs = Some(w', t, v) ->
@@ -276,7 +268,7 @@ Qed.
 
 (** Accessing locations *)
 
-Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : option (world * trace * val) :=
+Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) : option (world * trace * val) :=
   match access_mode ty with
   | By_value chunk =>
       match type_is_volatile ty with
@@ -288,37 +280,37 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o
   | _ => None
   end.
 
-Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
-  (alignof_blockcopy ge ty | Int.unsigned ofs') /\ (alignof_blockcopy ge ty | Int.unsigned ofs) /\
-  (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-           \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs
-           \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs').
+Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs) : Prop :=
+  (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') /\ (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) /\
+  (b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs
+           \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs
+           \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs').
 
 Remark check_assign_copy:
-  forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int),
+  forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs),
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
 Proof with try (right; intuition omega).
   intros. unfold assign_copy_ok.
   assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
-  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto...
-  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto...
+  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto...
+  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto...
   assert (Y: {b' <> b \/
-              Int.unsigned ofs' = Int.unsigned ofs \/
-              Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/
-              Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'} +
+              Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/
+              Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/
+              Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs'} +
            {~(b' <> b \/
-              Int.unsigned ofs' = Int.unsigned ofs \/
-              Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/
-              Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs')}).
+              Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/
+              Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/
+              Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs')}).
   destruct (eq_block b' b); auto.
-  destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto.
-  destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto.
-  destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto.
+  destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto.
+  destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto.
+  destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto.
   right; intuition omega.
   destruct Y... left; intuition omega.
 Defined.
 
-Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) :=
+Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) :=
   match access_mode ty with
   | By_value chunk =>
       match type_is_volatile ty with
@@ -329,8 +321,8 @@ Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v
       match v with
       | Vptr b' ofs' =>
           if check_assign_copy ty b ofs b' ofs' then
-            do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty);
-            do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes;
+            do bytes <- Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty);
+            do m' <- Mem.storebytes m b (Ptrofs.unsigned ofs) bytes;
             Some(w, E0, m')
           else None
       | _ => None
@@ -433,21 +425,29 @@ Definition do_ef_volatile_store (chunk: memory_chunk)
   | _ => None
   end.
 
-Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int)
+Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m.
 
-Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int)
+Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m.
 
+Definition do_alloc_size (v: val) : option ptrofs :=
+  match v with
+  | Vint n => if Archi.ptr64 then None else Some (Ptrofs.of_int n)
+  | Vlong n => if Archi.ptr64 then Some (Ptrofs.of_int64 n) else None
+  | _ => None
+  end.
+
 Definition do_ef_malloc
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
-  | Vint n :: nil =>
-      let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in
-      do m'' <- Mem.store Mint32 m' b (-4) (Vint n);
-      Some(w, E0, Vptr b Int.zero, m'')
+  | v :: nil =>
+      do sz <- do_alloc_size v;
+      let (m', b) := Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) in
+      do m'' <- Mem.store Mptr m' b (- size_chunk Mptr) v;
+      Some(w, E0, Vptr b Ptrofs.zero, m'')
   | _ => None
   end.
 
@@ -455,14 +455,11 @@ Definition do_ef_free
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
   | Vptr b lo :: nil =>
-      do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4);
-      match vsz with
-      | Vint sz =>
-          check (zlt 0 (Int.unsigned sz));
-          do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz);
-          Some(w, E0, Vundef, m')
-      | _ => None
-      end
+      do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr);
+      do sz <- do_alloc_size vsz;
+      check (zlt 0 (Ptrofs.unsigned sz));
+      do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
+      Some(w, E0, Vundef, m')
   | _ => None
   end.
 
@@ -478,9 +475,9 @@ Definition do_ef_memcpy (sz al: Z)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
   | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
-      if decide (memcpy_args_ok sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc)) then
-        do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
-        do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
+      if decide (memcpy_args_ok sz al bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc)) then
+        do bytes <- Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz;
+        do m' <- Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes;
         Some(w, E0, Vundef, m')
       else None
   | _ => None
@@ -526,6 +523,9 @@ Lemma do_ef_external_sound:
   do_external ef w vargs m = Some(w', t, vres, m') ->
   external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
 Proof with try congruence.
+  assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz).
+  { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; 
+    intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. }
   intros until m'.
   destruct ef; simpl.
 (* EF_external *)
@@ -545,16 +545,16 @@ Proof with try congruence.
   exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
   auto.
 (* EF_malloc *)
-  unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
-  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr.
-  split. econstructor; eauto. constructor.
+  unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr.
+  destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr.
+  split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor.
 (* EF_free *)
   unfold do_ef_free. destruct vargs... destruct v... destruct vargs...
-  mydestr. destruct v... mydestr.
-  split. econstructor; eauto. omega. constructor.
+  mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor.
 (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
-  destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1.
+  destruct v... destruct vargs... mydestr. 
+  apply Decidable_sound in Heqb1. red in Heqb1.
   split. econstructor; eauto; tauto. constructor.
 (* EF_annot *)
   unfold do_ef_annot. mydestr.
@@ -575,6 +575,10 @@ Lemma do_ef_external_complete:
   external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
   do_external ef w vargs m = Some(w', t, vres, m').
 Proof.
+  assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n).
+  { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. 
+    rewrite Ptrofs.of_int64_to_int64; auto.
+    rewrite Ptrofs.of_int_to_int; auto. }
   intros. destruct ef; simpl in *.
 (* EF_external *)
   eapply do_external_function_complete; eauto.
@@ -590,13 +594,13 @@ Proof.
   exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
 (* EF_malloc *)
   inv H; unfold do_ef_malloc.
-  inv H0. rewrite H1. rewrite H2. auto.
+  inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
 (* EF_free *)
   inv H; unfold do_ef_free.
-  inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega.
+  inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
 (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.
-  inv H0. rewrite Decidable_complete, H7, H8. auto.
+  inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto.
   red. tauto.
 (* EF_annot *)
   inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
@@ -680,10 +684,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match e!x with
       | Some(b, ty') =>
           check type_eq ty ty';
-          topred (Lred "red_var_local" (Eloc b Int.zero ty) m)
+          topred (Lred "red_var_local" (Eloc b Ptrofs.zero ty) m)
       | None =>
           do b <- Genv.find_symbol ge x;
-          topred (Lred "red_var_global" (Eloc b Int.zero ty) m)
+          topred (Lred "red_var_global" (Eloc b Ptrofs.zero ty) m)
       end
   | LV, Ederef r ty =>
       match is_val r with
@@ -702,7 +706,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
               do co <- ge.(genv_cenv)!id;
               match field_offset ge f (co_members co) with
               | Error _ => stuck
-              | OK delta => topred (Lred "red_field_struct" (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
+              | OK delta => topred (Lred "red_field_struct" (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m)
               end
           | Tunion id _ =>
               do co <- ge.(genv_cenv)!id;
@@ -782,9 +786,9 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
       end
   | RV, Esizeof ty' ty =>
-      topred (Rred "red_sizeof" (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0)
+      topred (Rred "red_sizeof" (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty'))) ty) m E0)
   | RV, Ealignof ty' ty =>
-      topred (Rred "red_alignof" (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0)
+      topred (Rred "red_alignof" (Eval (Vptrofs (Ptrofs.repr (alignof ge ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
@@ -1870,7 +1874,7 @@ Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type
       match PTree.get id e with
          | Some (b, ty') =>
              check (type_eq ty ty');
-             do w', t, m1 <- do_assign_loc w ty m b Int.zero v1;
+             do w', t, m1 <- do_assign_loc w ty m b Ptrofs.zero v1;
              match t with nil => sem_bind_parameters w e m1 params lv | _ => None end
         | None => None
       end
@@ -2034,15 +2038,12 @@ Definition do_step (w: world) (s: state) : list transition :=
 
 Ltac myinv :=
   match goal with
-  | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X
+  | [ |- In _ nil -> _ ] => intro X; elim X
   | [ |- In _ (ret _ _) -> _ ] =>
-        let X := fresh "X" in
         intro X; elim X; clear X;
-        [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
+        [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
   | [ |- In _ (_ :: nil) -> _ ] =>
-        let X := fresh "X" in
-        intro X; elim X; clear X;
-        [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv]
+        intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
   | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index e6426fb8..7a4c49a2 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -202,7 +202,7 @@ Definition temp_env := PTree.t val.
   memory load is performed.  If the type [ty] indicates an access by
   reference or by copy, the pointer [Vptr b ofs] is returned. *)
 
-Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop :=
+Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : val -> Prop :=
   | deref_loc_value: forall chunk v,
       access_mode ty = By_value chunk ->
       Mem.loadv chunk m (Vptr b ofs) = Some v ->
@@ -220,7 +220,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop :=
   This is allowed only if [ty] indicates an access by value or by copy.
   [m'] is the updated memory state. *)
 
-Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: int):
+Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: ptrofs):
                                             val -> mem -> Prop :=
   | assign_loc_value: forall v chunk m',
       access_mode ty = By_value chunk ->
@@ -228,13 +228,13 @@ Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: in
       assign_loc ce ty m b ofs v m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs')) ->
-      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs)) ->
-      b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-              \/ Int.unsigned ofs' + sizeof ce ty <= Int.unsigned ofs
-              \/ Int.unsigned ofs + sizeof ce ty <= Int.unsigned ofs' ->
-      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ce ty) = Some bytes ->
-      Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
+      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs')) ->
+      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs)) ->
+      b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs
+              \/ Ptrofs.unsigned ofs' + sizeof ce ty <= Ptrofs.unsigned ofs
+              \/ Ptrofs.unsigned ofs + sizeof ce ty <= Ptrofs.unsigned ofs' ->
+      Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ce ty) = Some bytes ->
+      Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
       assign_loc ce ty m b ofs (Vptr b' ofs') m'.
 
 Section SEMANTICS.
@@ -274,7 +274,7 @@ Inductive bind_parameters (e: env):
   | bind_parameters_cons:
       forall m id ty params v1 vl b m1 m2,
       PTree.get id e = Some(b, ty) ->
-      assign_loc ge ty m b Int.zero v1 m1 ->
+      assign_loc ge ty m b Ptrofs.zero v1 m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
@@ -384,9 +384,9 @@ Inductive eval_expr: expr -> val -> Prop :=
       sem_cast v1 (typeof a) ty m = Some v ->
       eval_expr (Ecast a ty) v
   | eval_Esizeof: forall ty1 ty,
-      eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
+      eval_expr (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1)))
   | eval_Ealignof: forall ty1 ty,
-      eval_expr (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1)))
+      eval_expr (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1)))
   | eval_Elvalue: forall a loc ofs v,
       eval_lvalue a loc ofs ->
       deref_loc (typeof a) m loc ofs v ->
@@ -396,14 +396,14 @@ Inductive eval_expr: expr -> val -> Prop :=
   in l-value position.  The result is the memory location [b, ofs]
   that contains the value of the expression [a]. *)
 
-with eval_lvalue: expr -> block -> int -> Prop :=
+with eval_lvalue: expr -> block -> ptrofs -> Prop :=
   | eval_Evar_local:   forall id l ty,
       e!id = Some(l, ty) ->
-      eval_lvalue (Evar id ty) l Int.zero
+      eval_lvalue (Evar id ty) l Ptrofs.zero
   | eval_Evar_global: forall id l ty,
       e!id = None ->
       Genv.find_symbol ge id = Some l ->
-      eval_lvalue (Evar id ty) l Int.zero
+      eval_lvalue (Evar id ty) l Ptrofs.zero
   | eval_Ederef: forall a ty l ofs,
       eval_expr a (Vptr l ofs) ->
       eval_lvalue (Ederef a ty) l ofs
@@ -412,7 +412,7 @@ with eval_lvalue: expr -> block -> int -> Prop :=
       typeof a = Tstruct id att ->
       ge.(genv_cenv)!id = Some co ->
       field_offset ge i (co_members co) = OK delta ->
-      eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta))
+      eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta))
  | eval_Efield_union:   forall a i ty l ofs id co att,
       eval_expr a (Vptr l ofs) ->
       typeof a = Tunion id att ->
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index b9a28ee1..5017fc8e 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -47,8 +47,8 @@ Definition compilenv := PTree.t Z.
 
 Definition var_addr (cenv: compilenv) (id: ident): expr :=
   match PTree.get id cenv with
-  | Some ofs => Econst (Oaddrstack (Int.repr ofs))
-  | None     => Econst (Oaddrsymbol id Int.zero)
+  | Some ofs => Econst (Oaddrstack (Ptrofs.repr ofs))
+  | None     => Econst (Oaddrsymbol id Ptrofs.zero)
   end.
 
 (** * Translation of expressions and statements. *)
@@ -269,7 +269,7 @@ Definition transl_funbody
 
 Definition transl_function (f: Csharpminor.function): res function :=
   let (cenv, stacksize) := build_compilenv f in
-  if zle stacksize Int.max_unsigned
+  if zle stacksize Ptrofs.max_unsigned
   then transl_funbody cenv stacksize f
   else Error(msg "Cminorgen: too many local variables, stack size exceeded").
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 2f551d68..ea1bc89c 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -76,7 +76,7 @@ Lemma sig_preserved:
 Proof.
   intros until tf; destruct f; simpl.
   unfold transl_function. destruct (build_compilenv f).
-  case (zle z Int.max_unsigned); simpl bind; try congruence.
+  case (zle z Ptrofs.max_unsigned); simpl bind; try congruence.
   intros. monadInv H. simpl. eapply sig_preserved_body; eauto.
   intro. inv H. reflexivity.
 Qed.
@@ -190,7 +190,7 @@ Qed.
 
 Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop :=
   | match_var_local: forall b sz ofs,
-      Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) ->
+      Val.inject f (Vptr b Ptrofs.zero) (Vptr sp (Ptrofs.repr ofs)) ->
       match_var f sp (Some(b, sz)) (Some ofs)
   | match_var_global:
       match_var f sp None None.
@@ -311,7 +311,7 @@ Proof.
   intros. rewrite PTree.gsspec. destruct (peq id0 id).
   (* the new var *)
   subst id0. rewrite CENV. constructor. econstructor. eauto.
-  rewrite Int.add_commut; rewrite Int.add_zero; auto.
+  rewrite Ptrofs.add_commut; rewrite Ptrofs.add_zero; auto.
   (* old vars *)
   generalize (me_vars0 id0). rewrite PTree.gro; auto. intros M; inv M.
   constructor; eauto.
@@ -794,7 +794,7 @@ Definition cenv_mem_separated (cenv: compilenv) (vars: list (ident * Z)) (f: mem
 Lemma match_callstack_alloc_variables_rec:
   forall tm sp tf cenv le te lo cs,
   Mem.valid_block tm sp ->
-  fn_stackspace tf <= Int.max_unsigned ->
+  fn_stackspace tf <= Ptrofs.max_unsigned ->
   (forall ofs k p, Mem.perm tm sp ofs k p -> 0 <= ofs < fn_stackspace tf) ->
   (forall ofs k p, 0 <= ofs < fn_stackspace tf -> Mem.perm tm sp ofs k p) ->
   forall e1 m1 vars e2 m2,
@@ -854,7 +854,7 @@ Qed.
 Lemma match_callstack_alloc_variables:
   forall tm1 sp tm2 m1 vars e m2 cenv f1 cs fn le te,
   Mem.alloc tm1 0 (fn_stackspace fn) = (tm2, sp) ->
-  fn_stackspace fn <= Int.max_unsigned ->
+  fn_stackspace fn <= Ptrofs.max_unsigned ->
   alloc_variables empty_env m1 vars e m2 ->
   list_norepet (map fst vars) ->
   cenv_compat cenv vars (fn_stackspace fn) ->
@@ -1225,7 +1225,7 @@ Qed.
 Theorem match_callstack_function_entry:
   forall fn cenv tf m e m' tm tm' sp f cs args targs le,
   build_compilenv fn = (cenv, tf.(fn_stackspace)) ->
-  tf.(fn_stackspace) <= Int.max_unsigned ->
+  tf.(fn_stackspace) <= Ptrofs.max_unsigned ->
   list_norepet (map fst (Csharpminor.fn_vars fn)) ->
   list_norepet (Csharpminor.fn_params fn) ->
   list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) ->
@@ -1334,82 +1334,91 @@ Lemma eval_binop_compat:
      eval_binop op tv1 tv2 tm = Some tv
   /\ Val.inject f v tv.
 Proof.
-  destruct op; simpl; intros.
-  inv H; inv H0; inv H1; TrivialExists.
-    repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-    repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  inv H; inv H0; inv H1; TrivialExists.
-    apply Int.sub_add_l.
-    simpl. destruct (eq_block b1 b0); auto.
-    subst b1. rewrite H in H0; inv H0.
-    rewrite dec_eq_true. rewrite Int.sub_shifted. auto.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+  destruct op; simpl; intros; inv H.
+- TrivialExists. apply Val.add_inject; auto.
+- TrivialExists. apply Val.sub_inject; auto.
+- TrivialExists. inv H0; inv H1; constructor.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
     destruct (Int.eq i0 Int.zero
-      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+    destruct (Int.eq i0 Int.zero); inv H4. TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
     destruct (Int.eq i0 Int.zero
-      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+    destruct (Int.eq i0 Int.zero); inv H4. TrivialExists.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int.iwordsize); constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int.iwordsize); constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int.iwordsize); constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists. apply Val.addl_inject; auto.
+- TrivialExists. apply Val.subl_inject; auto.
+- TrivialExists. inv H0; inv H1; constructor.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
     destruct (Int64.eq i0 Int64.zero
-      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
-    destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+    destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
     destruct (Int64.eq i0 Int64.zero
-      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists.
-  inv H0; try discriminate; inv H1; try discriminate. simpl in *.
-    destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
-(* cmpu *)
-  inv H. econstructor; split; eauto.
-  unfold Val.cmpu.
+      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists.
+- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
+    destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
+- TrivialExists; inv H0; inv H1; simpl; auto.
+  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
+- (* cmp *)
+  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
+- (* cmpu *)
+  TrivialExists. unfold Val.cmpu.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
   replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
-  destruct b; simpl; constructor.
+  apply val_inject_val_of_optbool.
   symmetry. eapply Val.cmpu_bool_inject; eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
   simpl; auto.
-(* cmpf *)
-  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
-(* cmpfs *)
-  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
-(* cmpl *)
-  unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H.
+- (* cmpf *)
+  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
+- (* cmpfs *)
+  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
+- (* cmpl *)
+  unfold Val.cmpl in *. inv H0; inv H1; simpl in H4; inv H4.
   econstructor; split. simpl; eauto. apply val_inject_val_of_bool.
-(* cmplu *)
-  unfold Val.cmplu in *. inv H0; inv H1; simpl in H; inv H.
+- (* cmplu *)
+  unfold Val.cmplu in *.
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
+  simpl in H4; inv H4.
+  replace (Val.cmplu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
   econstructor; split. simpl; eauto. apply val_inject_val_of_bool.
+  symmetry. eapply Val.cmplu_bool_inject; eauto.
+  intros; eapply Mem.valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.different_pointers_inject; eauto.
+  discriminate.
 Qed.
 
 (** * Correctness of Cminor construction functions *)
@@ -1421,21 +1430,22 @@ Lemma var_addr_correct:
   match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
   eval_var_addr ge e id b ->
   exists tv,
-     eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv
-  /\ Val.inject f (Vptr b Int.zero) tv.
+     eval_expr tge (Vptr sp Ptrofs.zero) te tm (var_addr cenv id) tv
+  /\ Val.inject f (Vptr b Ptrofs.zero) tv.
 Proof.
   unfold var_addr; intros.
   assert (match_var f sp e!id cenv!id).
     inv H. inv MENV. auto.
   inv H1; inv H0; try congruence.
   (* local *)
-  exists (Vptr sp (Int.repr ofs)); split.
-  constructor. simpl. rewrite Int.add_zero_l; auto.
+  exists (Vptr sp (Ptrofs.repr ofs)); split.
+  constructor. simpl. rewrite Ptrofs.add_zero_l; auto.
   congruence.
   (* global *)
   exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
-  exists (Vptr b Int.zero); split.
-  constructor. simpl. rewrite symbols_preserved. rewrite H2. auto.
+  exists (Vptr b Ptrofs.zero); split.
+  constructor. simpl. unfold Genv.symbol_address. 
+  rewrite symbols_preserved. rewrite H2. auto.
   econstructor; eauto.
 Qed.
 
@@ -1497,7 +1507,7 @@ Lemma transl_expr_correct:
   forall ta
     (TR: transl_expr cenv a = OK ta),
   exists tv,
-     eval_expr tge (Vptr sp Int.zero) te tm ta tv
+     eval_expr tge (Vptr sp Ptrofs.zero) te tm ta tv
   /\ Val.inject f v tv.
 Proof.
   induction 3; intros; simpl in TR; try (monadInv TR).
@@ -1535,7 +1545,7 @@ Lemma transl_exprlist_correct:
   forall ta
     (TR: transl_exprlist cenv a = OK ta),
   exists tv,
-     eval_exprlist tge (Vptr sp Int.zero) te tm ta tv
+     eval_exprlist tge (Vptr sp Ptrofs.zero) te tm ta tv
   /\ Val.inject_list f v tv.
 Proof.
   induction 3; intros; monadInv TR.
@@ -1569,7 +1579,7 @@ Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -
       transl_funbody cenv sz fn = OK tfn ->
       match_cont k tk cenv xenv cs ->
       match_cont (Csharpminor.Kcall optid fn e le k)
-                 (Kcall optid tfn (Vptr sp Int.zero) te tk)
+                 (Kcall optid tfn (Vptr sp Ptrofs.zero) te tk)
                  cenv' nil
                  (Frame cenv tfn e le te sp lo hi :: cs).
 
@@ -1584,7 +1594,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
                (Mem.nextblock m) (Mem.nextblock tm))
       (MK: match_cont k tk cenv xenv cs),
       match_states (Csharpminor.State fn s k e le m)
-                   (State tfn ts tk (Vptr sp Int.zero) te tm)
+                   (State tfn ts tk (Vptr sp Ptrofs.zero) te tm)
   | match_state_seq:
       forall fn s1 s2 k e le m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz
       (TRF: transl_funbody cenv sz fn = OK tfn)
@@ -1595,7 +1605,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
                (Mem.nextblock m) (Mem.nextblock tm))
       (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs),
       match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e le m)
-                   (State tfn ts1 tk (Vptr sp Int.zero) te tm)
+                   (State tfn ts1 tk (Vptr sp Ptrofs.zero) te tm)
   | match_callstate:
       forall fd args k m tfd targs tk tm f cs cenv
       (TR: transl_fundef fd = OK tfd)
@@ -1789,7 +1799,7 @@ Lemma switch_match_states:
     (MK: match_cont k tk cenv xenv cs)
     (TK: transl_lblstmt_cont cenv xenv ls tk tk'),
   exists S,
-  plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S
+  plus step tge (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S
   /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S.
 Proof.
   intros. inv TK.
@@ -2050,7 +2060,7 @@ Opaque PTree.set.
 (* ifthenelse *)
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
-  left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split.
+  left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split.
   apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
   econstructor; eauto. destruct b; auto.
 
@@ -2152,7 +2162,7 @@ Opaque PTree.set.
 (* internal call *)
   monadInv TR. generalize EQ; clear EQ; unfold transl_function.
   caseEq (build_compilenv f). intros ce sz BC.
-  destruct (zle sz Int.max_unsigned); try congruence.
+  destruct (zle sz Ptrofs.max_unsigned); try congruence.
   intro TRBODY.
   generalize TRBODY; intro TMP. monadInv TMP.
   set (tf := mkfunction (Csharpminor.fn_sig f)
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 4ac56b04..c395a2cb 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -22,6 +22,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Ctypes.
+Require Archi.
 
 (** * Syntax of operators. *)
 
@@ -72,7 +73,7 @@ Inductive incr_or_decr : Type := Incr | Decr.
 (** ** Casts and truth values *)
 
 Inductive classify_cast_cases : Type :=
-  | cast_case_neutral                   (**r int|pointer -> int32|pointer *)
+  | cast_case_pointer                              (**r between pointer types or intptr_t types *)
   | cast_case_i2i (sz2:intsize) (si2:signedness)   (**r int -> int *)
   | cast_case_f2f                                  (**r double -> double *)
   | cast_case_s2s                                  (**r single -> single *)
@@ -89,10 +90,10 @@ Inductive classify_cast_cases : Type :=
   | cast_case_l2s (si1: signedness)                (**r long -> single *)
   | cast_case_f2l (si2:signedness)                 (**r double -> long *)
   | cast_case_s2l (si2:signedness)                 (**r single -> long *)
+  | cast_case_i2bool                               (**r int -> bool *)
+  | cast_case_l2bool                               (**r long -> bool *)
   | cast_case_f2bool                               (**r double -> bool *)
   | cast_case_s2bool                               (**r single -> bool *)
-  | cast_case_l2bool                               (**r long -> bool *)
-  | cast_case_p2bool                               (**r pointer -> bool *)
   | cast_case_struct (id1 id2: ident)              (**r struct -> struct *)
   | cast_case_union  (id1 id2: ident)              (**r union -> union *)
   | cast_case_void                                 (**r any -> void *)
@@ -100,33 +101,54 @@ Inductive classify_cast_cases : Type :=
 
 Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   match tto, tfrom with
-  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
+  (* To [void] *)
+  | Tvoid, _ => cast_case_void
+  (* To [_Bool] *)
+  | Tint IBool _ _, Tint _ _ _ => cast_case_i2bool
+  | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
   | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool
   | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool
-  | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
-  | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
+  | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => 
+      if Archi.ptr64 then cast_case_l2bool else cast_case_i2bool
+  (* To [int] other than [_Bool] *)
+  | Tint sz2 si2 _, Tint _ _ _ =>
+      if Archi.ptr64 then cast_case_i2i sz2 si2
+      else if intsize_eq sz2 I32 then cast_case_pointer
+      else cast_case_i2i sz2 si2
+  | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
   | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2
   | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2
-  | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f
-  | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s
-  | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
-  | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
-  | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
-  | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
-  | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
-  | Tlong _ _, Tlong _ _ => cast_case_l2l
+  | Tint sz2 si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) =>
+      if Archi.ptr64 then cast_case_l2i sz2 si2
+      else if intsize_eq sz2 I32 then cast_case_pointer
+      else cast_case_i2i sz2 si2
+  (* To [long] *)
+  | Tlong _ _, Tlong _ _ =>
+      if Archi.ptr64 then cast_case_pointer else cast_case_l2l
   | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
-  | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
-  | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
   | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2
   | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2
+  | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) =>
+      if Archi.ptr64 then cast_case_pointer else cast_case_i2l si2
+  (* To [float] *)
+  | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
+  | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
   | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1
   | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1
-  | Tpointer _ _, Tlong _ _ => cast_case_l2i I32 Unsigned
-  | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
+  | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f
+  | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s
+  | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
+  | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
+  (* To pointer types *)
+  | Tpointer _ _, Tint _ _ _ =>
+      if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer
+  | Tpointer _ _, Tlong _ _ =>
+      if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned
+  | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer
+  (* To struct or union types *)
   | Tstruct id2 _, Tstruct id1 _ => cast_case_struct id1 id2
   | Tunion id2 _, Tunion id1 _ => cast_case_union id1 id2
-  | Tvoid, _ => cast_case_void
+  (* Catch-all *)
   | _, _ => cast_case_default
   end.
 
@@ -200,9 +222,11 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
 
 Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
   match classify_cast t1 t2 with
-  | cast_case_neutral =>
+  | cast_case_pointer =>
       match v with
-      | Vint _ | Vptr _ _ => Some v
+      | Vptr _ _ => Some v
+      | Vint _ => if Archi.ptr64 then None else Some v
+      | Vlong _ => if Archi.ptr64 then Some v else None
       | _ => None
       end
   | cast_case_i2i sz2 si2 =>
@@ -258,6 +282,25 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
           end
       | _ => None
       end
+  | cast_case_i2bool =>
+      match v with
+      | Vint n =>
+          Some(Vint(if Int.eq n Int.zero then Int.zero else Int.one))
+      | Vptr b ofs =>
+          if Archi.ptr64 then None else
+          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None
+      | _ => None
+      end
+  | cast_case_l2bool =>
+      match v with
+      | Vlong n =>
+          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
+      | Vptr b ofs =>
+          if negb Archi.ptr64 then None else
+          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None
+
+      | _ => None
+      end
   | cast_case_f2bool =>
       match v with
       | Vfloat f =>
@@ -270,12 +313,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
           Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one))
       | _ => None
       end
-  | cast_case_p2bool =>
-      match v with
-      | Vint i => Some (Vint (cast_int_int IBool Signed i))
-      | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None
-      | _ => None
-      end
   | cast_case_l2l =>
       match v with
       | Vlong n => Some (Vlong n)
@@ -291,12 +328,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
       | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n))))
       | _ => None
       end
-  | cast_case_l2bool =>
-      match v with
-      | Vlong n =>
-          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
-      | _ => None
-      end
   | cast_case_l2f si1 =>
       match v with
       | Vlong i => Some (Vfloat (cast_long_float si1 i))
@@ -350,16 +381,15 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
 
 Inductive classify_bool_cases : Type :=
   | bool_case_i                           (**r integer *)
+  | bool_case_l                           (**r long *)
   | bool_case_f                           (**r double float *)
   | bool_case_s                           (**r single float *)
-  | bool_case_p                           (**r pointer *)
-  | bool_case_l                           (**r long *)
   | bool_default.
 
 Definition classify_bool (ty: type) : classify_bool_cases :=
   match typeconv ty with
   | Tint _ _ _ => bool_case_i
-  | Tpointer _ _ => bool_case_p
+  | Tpointer _ _ => if Archi.ptr64 then bool_case_l else bool_case_i
   | Tfloat F64 _ => bool_case_f
   | Tfloat F32 _ => bool_case_s
   | Tlong _ _ => bool_case_l
@@ -376,6 +406,17 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool :=
   | bool_case_i =>
       match v with
       | Vint n => Some (negb (Int.eq n Int.zero))
+      | Vptr b ofs =>
+          if Archi.ptr64 then None else
+          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None
+      | _ => None
+      end
+  | bool_case_l =>
+      match v with
+      | Vlong n => Some (negb (Int64.eq n Int64.zero))
+      | Vptr b ofs =>
+          if negb Archi.ptr64 then None else
+          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None
       | _ => None
       end
   | bool_case_f =>
@@ -388,17 +429,6 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool :=
       | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero))
       | _ => None
       end
-  | bool_case_p =>
-      match v with
-      | Vint n => Some (negb (Int.eq n Int.zero))
-      | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None
-      | _ => None
-      end
-  | bool_case_l =>
-      match v with
-      | Vlong n => Some (negb (Int64.eq n Int64.zero))
-      | _ => None
-      end
   | bool_default => None
   end.
 
@@ -407,35 +437,7 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool :=
 (** *** Boolean negation *)
 
 Definition sem_notbool (v: val) (ty: type) (m: mem): option val :=
-  match classify_bool ty with
-  | bool_case_i =>
-      match v with
-      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | _ => None
-      end
-  | bool_case_f =>
-      match v with
-      | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
-      | _ => None
-      end
-  | bool_case_s =>
-      match v with
-      | Vsingle f => Some (Val.of_bool (Float32.cmp Ceq f Float32.zero))
-      | _ => None
-      end
-  | bool_case_p =>
-      match v with
-      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None
-      | _ => None
-      end
-  | bool_case_l =>
-      match v with
-      | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero))
-      | _ => None
-      end
-  | bool_default => None
-  end.
+  option_map (fun b => Val.of_bool (negb b)) (bool_val v ty m).
 
 (** *** Opposite and absolute value *)
 
@@ -623,59 +625,63 @@ Definition sem_binarith
 (** *** Addition *)
 
 Inductive classify_add_cases : Type :=
-  | add_case_pi(ty: type)     (**r pointer, int *)
-  | add_case_ip(ty: type)     (**r int, pointer *)
-  | add_case_pl(ty: type)     (**r pointer, long *)
-  | add_case_lp(ty: type)     (**r long, pointer *)
-  | add_default.                       (**r numerical type, numerical type *)
+  | add_case_pi (ty: type) (si: signedness)     (**r pointer, int *)
+  | add_case_pl (ty: type)     (**r pointer, long *)
+  | add_case_ip (si: signedness) (ty: type)     (**r int, pointer *)
+  | add_case_lp (ty: type)     (**r long, pointer *)
+  | add_default.               (**r numerical type, numerical type *)
 
 Definition classify_add (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
-  | Tpointer ty _, Tint _ _ _ => add_case_pi ty
-  | Tint _ _ _, Tpointer ty _ => add_case_ip ty
+  | Tpointer ty _, Tint _ si _ => add_case_pi ty si
   | Tpointer ty _, Tlong _ _ => add_case_pl ty
+  | Tint _ si _, Tpointer ty _ => add_case_ip si ty
   | Tlong _ _, Tpointer ty _ => add_case_lp ty
   | _, _ => add_default
   end.
 
+Definition ptrofs_of_int (si: signedness) (n: int) : ptrofs :=
+  match si with
+  | Signed => Ptrofs.of_ints n
+  | Unsigned => Ptrofs.of_intu n
+  end.
+
+Definition sem_add_ptr_int (cenv: composite_env) (ty: type) (si: signedness) (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vptr b1 ofs1, Vint n2 =>
+      let n2 := ptrofs_of_int si n2 in
+      Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
+  | Vint n1, Vint n2 =>
+      if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+  | Vlong n1, Vint n2 =>
+      let n2 := cast_int_long si n2 in
+      if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
+  | _,  _ => None
+  end.
+
+Definition sem_add_ptr_long (cenv: composite_env) (ty: type) (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vptr b1 ofs1, Vlong n2 =>
+      let n2 := Ptrofs.of_int64 n2 in
+      Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
+  | Vint n1, Vlong n2 =>
+      let n2 := Int.repr (Int64.unsigned n2) in
+      if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+  | Vlong n1, Vlong n2 =>
+      if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
+  | _,  _ => None
+  end.
+
 Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val :=
   match classify_add t1 t2 with
-  | add_case_pi ty =>                 (**r pointer plus integer *)
-      match v1,v2 with
-      | Vptr b1 ofs1, Vint n2 =>
-        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
-      | Vint n1, Vint n2 =>
-        Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
-      | _,  _ => None
-      end
-  | add_case_ip ty =>                 (**r integer plus pointer *)
-      match v1,v2 with
-      | Vint n1, Vptr b2 ofs2 =>
-        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
-      | Vint n1, Vint n2 =>
-        Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
-      | _,  _ => None
-      end
-  | add_case_pl ty =>                 (**r pointer plus long *)
-      match v1,v2 with
-      | Vptr b1 ofs1, Vlong n2 =>
-        let n2 := Int.repr (Int64.unsigned n2) in
-        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
-      | Vint n1, Vlong n2 =>
-        let n2 := Int.repr (Int64.unsigned n2) in
-        Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
-      | _,  _ => None
-      end
-  | add_case_lp ty =>                 (**r long plus pointer *)
-      match v1,v2 with
-      | Vlong n1, Vptr b2 ofs2 =>
-        let n1 := Int.repr (Int64.unsigned n1) in
-        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
-      | Vlong n1, Vint n2 =>
-        let n1 := Int.repr (Int64.unsigned n1) in
-        Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
-      | _,  _ => None
-      end
+  | add_case_pi ty si =>             (**r pointer plus integer *)
+      sem_add_ptr_int cenv ty si v1 v2
+  | add_case_pl ty =>                (**r pointer plus long *)
+      sem_add_ptr_long cenv ty v1 v2
+  | add_case_ip si ty =>             (**r integer plus pointer *)
+      sem_add_ptr_int cenv ty si v2 v1
+  | add_case_lp ty =>                (**r long plus pointer *)
+      sem_add_ptr_long cenv ty v2 v1
   | add_default =>
       sem_binarith
         (fun sg n1 n2 => Some(Vint(Int.add n1 n2)))
@@ -688,14 +694,14 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
 (** *** Subtraction *)
 
 Inductive classify_sub_cases : Type :=
-  | sub_case_pi(ty: type)               (**r pointer, int *)
-  | sub_case_pp(ty: type)               (**r pointer, pointer *)
-  | sub_case_pl(ty: type)               (**r pointer, long *)
-  | sub_default.                        (**r numerical type, numerical type *)
+  | sub_case_pi (ty: type) (si: signedness)  (**r pointer, int *)
+  | sub_case_pp (ty: type)               (**r pointer, pointer *)
+  | sub_case_pl (ty: type)               (**r pointer, long *)
+  | sub_default.                         (**r numerical type, numerical type *)
 
 Definition classify_sub (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
-  | Tpointer ty _, Tint _ _ _ => sub_case_pi ty
+  | Tpointer ty _, Tint _ si _ => sub_case_pi ty si
   | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty
   | Tpointer ty _, Tlong _ _ => sub_case_pl ty
   | _, _ => sub_default
@@ -703,22 +709,28 @@ Definition classify_sub (ty1: type) (ty2: type) :=
 
 Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val :=
   match classify_sub t1 t2 with
-  | sub_case_pi ty =>            (**r pointer minus integer *)
-      match v1,v2 with
+  | sub_case_pi ty si =>            (**r pointer minus integer *)
+      match v1, v2 with
       | Vptr b1 ofs1, Vint n2 =>
-          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+          let n2 := ptrofs_of_int si n2 in
+          Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
       | Vint n1, Vint n2 =>
-          Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+          if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vlong n1, Vint n2 =>
+          let n2 := cast_int_long si n2 in
+          if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
       | _,  _ => None
       end
   | sub_case_pl ty =>            (**r pointer minus long *)
-      match v1,v2 with
+      match v1, v2 with
       | Vptr b1 ofs1, Vlong n2 =>
-          let n2 := Int.repr (Int64.unsigned n2) in
-          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+          let n2 := Ptrofs.of_int64 n2 in
+          Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
       | Vint n1, Vlong n2 =>
           let n2 := Int.repr (Int64.unsigned n2) in
-          Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+          if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vlong n1, Vlong n2 =>
+          if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
       | _,  _ => None
       end
   | sub_case_pp ty =>          (**r pointer minus pointer *)
@@ -726,8 +738,8 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
       | Vptr b1 ofs1, Vptr b2 ofs2 =>
           if eq_block b1 b2 then
             let sz := sizeof cenv ty in
-            if zlt 0 sz && zle sz Int.max_signed
-            then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz)))
+            if zlt 0 sz && zle sz Ptrofs.max_signed
+            then Some (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr sz)))
             else None
           else None
       | _, _ => None
@@ -903,6 +915,8 @@ Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
 
 Inductive classify_cmp_cases : Type :=
   | cmp_case_pp                       (**r pointer, pointer *)
+  | cmp_case_pi (si: signedness)      (**r pointer, int *)
+  | cmp_case_ip (si: signedness)      (**r int, pointer *)
   | cmp_case_pl                       (**r pointer, long *)
   | cmp_case_lp                       (**r long, pointer *)
   | cmp_default.                      (**r numerical, numerical *)
@@ -910,32 +924,64 @@ Inductive classify_cmp_cases : Type :=
 Definition classify_cmp (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
   | Tpointer _ _ , Tpointer _ _ => cmp_case_pp
-  | Tpointer _ _ , Tint _ _ _ => cmp_case_pp
-  | Tint _ _ _, Tpointer _ _ => cmp_case_pp
+  | Tpointer _ _ , Tint _ si _ => cmp_case_pi si
+  | Tint _ si _, Tpointer _ _ => cmp_case_ip si
   | Tpointer _ _ , Tlong _ _ => cmp_case_pl
   | Tlong _ _ , Tpointer _ _ => cmp_case_lp
   | _, _ => cmp_default
   end.
 
+Definition cmp_ptr (m: mem) (c: comparison) (v1 v2: val): option val :=
+  option_map Val.of_bool
+   (if Archi.ptr64
+    then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
+    else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2).
+
 Definition sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
   match classify_cmp t1 t2 with
   | cmp_case_pp =>
-      option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
+      cmp_ptr m c v1 v2
+  | cmp_case_pi si =>
+      match v2 with
+      | Vint n2 =>
+          let v2' := Vptrofs (ptrofs_of_int si n2) in
+          cmp_ptr m c v1 v2'
+      | Vptr b ofs =>
+          if Archi.ptr64 then None else cmp_ptr m c v1 v2
+      | _ =>
+          None
+      end
+  | cmp_case_ip si =>
+      match v1 with
+      | Vint n1 =>
+          let v1' := Vptrofs (ptrofs_of_int si n1) in
+          cmp_ptr m c v1' v2
+      | Vptr b ofs =>
+          if Archi.ptr64 then None else cmp_ptr m c v1 v2
+      | _ =>
+          None
+      end
   | cmp_case_pl =>
       match v2 with
       | Vlong n2 =>
-          let n2 := Int.repr (Int64.unsigned n2) in
-          option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2))
-      | _ => None
+          let v2' := Vptrofs (Ptrofs.of_int64 n2) in
+          cmp_ptr m c v1 v2'
+      | Vptr b ofs =>
+          if Archi.ptr64 then cmp_ptr m c v1 v2 else None
+      | _ =>
+          None
       end
   | cmp_case_lp =>
       match v1 with
       | Vlong n1 =>
-          let n1 := Int.repr (Int64.unsigned n1) in
-          option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2)
-      | _ => None
+          let v1' := Vptrofs (Ptrofs.of_int64 n1) in
+          cmp_ptr m c v1' v2
+      | Vptr b ofs =>
+          if Archi.ptr64 then cmp_ptr m c v1 v2 else None
+      | _ =>
+          None
       end
   | cmp_default =>
       sem_binarith
@@ -1047,30 +1093,30 @@ Variables m m': mem.
 Hypothesis valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m b1 (Int.unsigned ofs) = true ->
-  Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.valid_pointer m' b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true ->
-  Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m' b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_pointer_no_overflow:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
   forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   b1 <> b2 ->
-  Mem.valid_pointer m b1 (Int.unsigned ofs1) = true ->
-  Mem.valid_pointer m b2 (Int.unsigned ofs2) = true ->
+  Mem.valid_pointer m b1 (Ptrofs.unsigned ofs1) = true ->
+  Mem.valid_pointer m b2 (Ptrofs.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 
 Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue.
 Proof. unfold Vtrue; auto. Qed.
@@ -1082,11 +1128,18 @@ Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool
 Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse].
 Qed.
 
-Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool.
+Remark val_inject_vptrofs: forall n, Val.inject f (Vptrofs n) (Vptrofs n).
+Proof. intros. unfold Vptrofs. destruct Archi.ptr64; auto. Qed.
+
+Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs.
 
 Ltac TrivialInject :=
   match goal with
-  | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto
+  | [ H: None = Some _ |- _ ] => discriminate
+  | [ H: Some _ = Some _ |- _ ] => inv H; TrivialInject
+  | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x; TrivialInject
+  | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; TrivialInject
+  | [ |- exists v', Some ?v = Some v' /\ _ ] => exists v; split; auto
   | _ => idtac
   end.
 
@@ -1096,20 +1149,31 @@ Lemma sem_cast_inj:
   Val.inject f v1 tv1 ->
   exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv.
 Proof.
-  unfold sem_cast; intros; destruct (classify_cast ty1 ty);
-  inv H0; inv H; TrivialInject.
+  unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; TrivialInject.
 - econstructor; eauto.
-- destruct (cast_float_int si2 f0); inv H1; TrivialInject.
-- destruct (cast_single_int si2 f0); inv H1; TrivialInject.
-- destruct (cast_float_long si2 f0); inv H1; TrivialInject.
-- destruct (cast_single_long si2 f0); inv H1; TrivialInject.
-- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2.
-  erewrite weak_valid_pointer_inj by eauto. TrivialInject. 
-- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
-- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
+- erewrite weak_valid_pointer_inj by eauto. TrivialInject. 
+- erewrite weak_valid_pointer_inj by eauto. TrivialInject. 
+- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto.
+- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto.
 - econstructor; eauto.
 Qed.
 
+Lemma bool_val_inj:
+  forall v ty b tv,
+  bool_val v ty m = Some b ->
+  Val.inject f v tv ->
+  bool_val tv ty m' = Some b.
+Proof.
+  unfold bool_val; intros.
+  destruct (classify_bool ty); inv H0; try congruence.
+  destruct Archi.ptr64; try discriminate.
+  destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H.
+  erewrite weak_valid_pointer_inj by eauto. auto.
+  destruct Archi.ptr64; try discriminate.
+  destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H.
+  erewrite weak_valid_pointer_inj by eauto. auto.
+Qed.
+
 Lemma sem_unary_operation_inj:
   forall op v1 ty v tv1,
   sem_unary_operation op v1 ty m = Some v ->
@@ -1117,15 +1181,14 @@ Lemma sem_unary_operation_inj:
   exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_unary_operation; intros. destruct op.
-  (* notbool *)
-  unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject.
-  destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2.
-  erewrite weak_valid_pointer_inj by eauto. TrivialInject.
-  (* notint *)
+- (* notbool *)
+  unfold sem_notbool in *. destruct (bool_val v1 ty m) as [b|] eqn:BV; simpl in H; inv H.
+  erewrite bool_val_inj by eauto. simpl. TrivialInject.
+- (* notint *)
   unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject.
-  (* neg *)
+- (* neg *)
   unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
-  (* absfloat *)
+- (* absfloat *)
   unfold sem_absfloat in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
 Qed.
 
@@ -1175,6 +1238,24 @@ Proof.
   destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto.
 Qed.
 
+Remark sem_cmp_ptr_inj:
+  forall c v1 v2 v tv1 tv2,
+  cmp_ptr m c v1 v2 = Some v ->
+  Val.inject f v1 tv1 ->
+  Val.inject f v2 tv2 ->
+  exists tv, cmp_ptr m' c tv1 tv2 = Some tv /\ Val.inject f v tv.
+Proof.
+  unfold cmp_ptr; intros. 
+  remember (if Archi.ptr64
+       then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
+       else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as ob.
+  destruct ob as [b|]; simpl in H; inv H.
+  exists (Val.of_bool b); split; auto.
+  destruct Archi.ptr64. 
+  erewrite Val.cmplu_bool_inject by eauto. auto.
+  erewrite Val.cmpu_bool_inject by eauto. auto.
+Qed.
+
 Remark sem_cmp_inj:
   forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
   sem_cmp cmp v1 ty1 v2 ty2 m = Some v ->
@@ -1185,24 +1266,15 @@ Proof.
   intros.
   unfold sem_cmp in *; destruct (classify_cmp ty1 ty2).
 - (* pointer - pointer *)
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
-  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b).
-  simpl. TrivialInject.
-  symmetry. eapply Val.cmpu_bool_inject; eauto.
+  eapply sem_cmp_ptr_inj; eauto.
+- (* pointer - int *)
+  inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto.
+- (* int - pointer *)
+  inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto.
 - (* pointer - long *)
-  destruct v2; try discriminate. inv H1.
-  set (v2 := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
-  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b).
-  simpl. TrivialInject.
-  symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor.
+  inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto.
 - (* long - pointer *)
-  destruct v1; try discriminate. inv H0.
-  set (v1 := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
-  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b).
-  simpl. TrivialInject.
-  symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor.
+  inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto.
 - (* numerical - numerical *)
   assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))).
   {
@@ -1219,27 +1291,31 @@ Lemma sem_binary_operation_inj:
 Proof.
   unfold sem_binary_operation; intros; destruct op.
 - (* add *)
-  unfold sem_add in *; destruct (classify_add ty1 ty2).
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  assert (A: forall cenv ty si v1' v2' tv1' tv2',
+             Val.inject f v1' tv1' -> Val.inject f v2' tv2' ->
+             sem_add_ptr_int cenv ty si v1' v2' = Some v ->
+             exists tv, sem_add_ptr_int cenv ty si tv1' tv2' = Some tv /\ Val.inject f v tv).
+  { intros. unfold sem_add_ptr_int in *; inv H2; inv H3; TrivialInject.
+    econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. }
+  assert (B: forall cenv ty v1' v2' tv1' tv2',
+             Val.inject f v1' tv1' -> Val.inject f v2' tv2' ->
+             sem_add_ptr_long cenv ty v1' v2' = Some v ->
+             exists tv, sem_add_ptr_long cenv ty tv1' tv2' = Some tv /\ Val.inject f v tv).
+  { intros. unfold sem_add_ptr_long in *; inv H2; inv H3; TrivialInject.
+    econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. }
+  unfold sem_add in *; destruct (classify_add ty1 ty2); eauto.
   + eapply sem_binarith_inject; eauto; intros; exact I.
 - (* sub *)
   unfold sem_sub in *; destruct (classify_sub ty1 ty2).
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. rewrite Int.sub_add_l. auto.
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; TrivialInject.
+    econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. 
+  + inv H0; inv H1; TrivialInject.
     destruct (eq_block b1 b0); try discriminate. subst b1.
     rewrite H0 in H2; inv H2. rewrite dec_eq_true.
-    destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3.
-    rewrite Int.sub_shifted. TrivialInject.
-  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
-    econstructor. eauto. rewrite Int.sub_add_l. auto.
+    destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Ptrofs.max_signed); inv H.
+    rewrite Ptrofs.sub_shifted. TrivialInject.
+  + inv H0; inv H1; TrivialInject.
+    econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. 
   + eapply sem_binarith_inject; eauto; intros; exact I.
 - (* mul *)
   eapply sem_binarith_inject; eauto; intros; exact I.
@@ -1286,18 +1362,6 @@ Proof.
 - eapply sem_cmp_inj; eauto.
 Qed.
 
-Lemma bool_val_inj:
-  forall v ty b tv,
-  bool_val v ty m = Some b ->
-  Val.inject f v tv ->
-  bool_val tv ty m' = Some b.
-Proof.
-  unfold bool_val; intros.
-  destruct (classify_bool ty); inv H0; try congruence.
-  destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H.
-  erewrite weak_valid_pointer_inj by eauto. auto.
-Qed.
-
 End GENERIC_INJECTION.
 
 Lemma sem_cast_inject:
@@ -1364,7 +1428,7 @@ Lemma cast_bool_bool_val:
   assert (A: classify_bool t =
     match t with
     | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
+    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => if Archi.ptr64 then bool_case_l else bool_case_i
     | Tfloat F64 _ => bool_case_f
     | Tfloat F32 _ => bool_case_s
     | Tlong _ _ => bool_case_l
@@ -1373,9 +1437,12 @@ Lemma cast_bool_bool_val:
   {
     unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
   }
-  unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
+  unfold bool_val. rewrite A.
+  unfold sem_cast, classify_cast; remember Archi.ptr64 as ptr64; destruct t; simpl; auto; destruct v; auto.
   destruct (Int.eq i0 Int.zero); auto.
+  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i0)); auto.
   destruct (Int64.eq i Int64.zero); auto.
+  destruct (negb ptr64); auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
   destruct f; auto.
   destruct f; auto.
   destruct f; auto.
@@ -1383,13 +1450,30 @@ Lemma cast_bool_bool_val:
   destruct (Float.cmp Ceq f0 Float.zero); auto.
   destruct f; auto.
   destruct (Float32.cmp Ceq f0 Float32.zero); auto.
-  destruct f; auto.
-  destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
-  destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
+  destruct f; auto. 
+  destruct ptr64; auto.
   destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Int.eq i Int.zero); auto.
+  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Int.eq i Int.zero); auto.
+  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto.
+  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
 Qed.
 
 (** Relation between Boolean value and Boolean negation. *)
@@ -1399,13 +1483,13 @@ Lemma notbool_bool_val:
   sem_notbool v t m =
   match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end.
 Proof.
-  intros. unfold sem_notbool, bool_val.
-  destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
+  intros. unfold sem_notbool. destruct (bool_val v t m) as [[] | ]; reflexivity.
 Qed.
 
 (** Properties of values obtained by casting to a given type. *)
 
+Section VAL_CASTED.
+
 Inductive val_casted: val -> type -> Prop :=
   | val_casted_int: forall sz si attr n,
       cast_int_int sz si n = n ->
@@ -1419,9 +1503,13 @@ Inductive val_casted: val -> type -> Prop :=
   | val_casted_ptr_ptr: forall b ofs ty attr,
       val_casted (Vptr b ofs) (Tpointer ty attr)
   | val_casted_int_ptr: forall n ty attr,
-      val_casted (Vint n) (Tpointer ty attr)
+      Archi.ptr64 = false -> val_casted (Vint n) (Tpointer ty attr)
   | val_casted_ptr_int: forall b ofs si attr,
-      val_casted (Vptr b ofs) (Tint I32 si attr)
+      Archi.ptr64 = false -> val_casted (Vptr b ofs) (Tint I32 si attr)
+  | val_casted_long_ptr: forall n ty attr,
+      Archi.ptr64 = true -> val_casted (Vlong n) (Tpointer ty attr)
+  | val_casted_ptr_long: forall b ofs si attr,
+      Archi.ptr64 = true -> val_casted (Vptr b ofs) (Tlong si attr)
   | val_casted_struct: forall id attr b ofs,
       val_casted (Vptr b ofs) (Tstruct id attr)
   | val_casted_union: forall id attr b ofs,
@@ -1429,6 +1517,8 @@ Inductive val_casted: val -> type -> Prop :=
   | val_casted_void: forall v,
       val_casted v Tvoid.
 
+Hint Constructors val_casted.
+
 Remark cast_int_int_idem:
   forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i.
 Proof.
@@ -1438,77 +1528,50 @@ Proof.
   destruct (Int.eq i Int.zero); auto.
 Qed.
 
+Ltac DestructCases :=
+  match goal with
+  | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
+  | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
+  | [H: Some _ = Some _ |- _ ] => inv H; DestructCases
+  | [H: None = Some _ |- _ ] => discriminate H
+  | [H: @eq intsize _ _ |- _ ] => discriminate H || (clear H; DestructCases)
+  | [ |- val_casted (Vint (if ?x then Int.zero else Int.one)) _ ] =>
+       try (constructor; destruct x; reflexivity)
+  | [ |- val_casted (Vint _) (Tint ?sz ?sg _) ] =>
+       try (constructor; apply (cast_int_int_idem sz sg))
+  | _ => idtac
+  end.
+
 Lemma cast_val_is_casted:
   forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'.
 Proof.
-  unfold sem_cast; intros. destruct ty'; simpl in *.
-- (* void *)
-  constructor.
-- (* int *)
-  destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H.
-  constructor. apply (cast_int_int_idem I8 s).
-  constructor. apply (cast_int_int_idem I8 s).
-  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
-  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
-  constructor. apply (cast_int_int_idem I16 s).
-  constructor. apply (cast_int_int_idem I16 s).
-  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
-  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
-  constructor. auto.
-  constructor.
-  constructor. auto.
-  destruct (cast_single_int s f); inv H1. constructor. auto.
-  destruct (cast_float_int s f); inv H1. constructor; auto.
-  constructor; auto.
-  constructor.
-  constructor; auto.
-  constructor.
-  constructor; auto.
-  constructor.
-  constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
-  constructor. simpl. destruct (Int64.eq i Int64.zero); auto.
-  constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto.
-  constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
-- (* long *)
-  destruct ty; try (destruct f); try discriminate.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor.
-  destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-- (* float *)
-  destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor.
-- (* pointer *)
-  destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor.
-- (* array (impossible case) *)
-  discriminate.
-- (* function (impossible case) *)
-  discriminate.
-- (* structs *)
-  destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i); inv H; constructor.
-- (* unions *)
-  destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i); inv H; constructor.
+  unfold sem_cast; intros.
+  destruct ty, ty'; simpl in H; DestructCases; constructor; auto.
 Qed.
 
+End VAL_CASTED.
+
 (** As a consequence, casting twice is equivalent to casting once. *)
 
 Lemma cast_val_casted:
   forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v.
 Proof.
-  intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto.
-  destruct sz; congruence.
-  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
-  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
+  intros. unfold sem_cast; inversion H; clear H; subst v ty; simpl.
+- destruct Archi.ptr64; [ | destruct (intsize_eq sz I32)].
++ destruct sz; f_equal; f_equal; assumption.
++ subst sz; auto.
++ destruct sz; f_equal; f_equal; assumption.
+- auto.
+- auto.
+- destruct Archi.ptr64; auto.
+- auto.
+- rewrite H0; auto.
+- rewrite H0; auto.
+- rewrite H0; auto.
+- rewrite H0; auto.
+- rewrite dec_eq_true; auto.
+- rewrite dec_eq_true; auto.
+- auto. 
 Qed.
 
 Lemma cast_idempotent:
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 30e6200d..0c3e00de 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -63,7 +63,7 @@ Variable ge: genv.
   returned, and [t] the trace of observables (nonempty if this is
   a volatile access). *)
 
-Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop :=
+Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : trace -> val -> Prop :=
   | deref_loc_value: forall chunk v,
       access_mode ty = By_value chunk ->
       type_is_volatile ty = false ->
@@ -87,7 +87,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val ->
   [m'] is the updated memory state and [t] the trace of observables
   (nonempty if this is a volatile store). *)
 
-Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
+Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs):
                                             val -> trace -> mem -> Prop :=
   | assign_loc_value: forall v chunk m',
       access_mode ty = By_value chunk ->
@@ -100,13 +100,13 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
       assign_loc ty m b ofs v t m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (alignof_blockcopy ge ty | Int.unsigned ofs') ->
-      (alignof_blockcopy ge ty | Int.unsigned ofs) ->
-      b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-              \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs
-              \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs' ->
-      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty) = Some bytes ->
-      Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
+      (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') ->
+      (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) ->
+      b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs
+              \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs
+              \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs' ->
+      Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty) = Some bytes ->
+      Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
       assign_loc ty m b ofs (Vptr b' ofs') E0 m'.
 
 (** Allocation of function-local variables.
@@ -142,7 +142,7 @@ Inductive bind_parameters (e: env):
   | bind_parameters_cons:
       forall m id ty params v1 vl b m1 m2,
       PTree.get id e = Some(b, ty) ->
-      assign_loc ty m b Int.zero v1 E0 m1 ->
+      assign_loc ty m b Ptrofs.zero v1 E0 m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
@@ -211,12 +211,12 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop :=
   | red_var_local: forall x ty m b,
       e!x = Some(b, ty) ->
       lred (Evar x ty) m
-           (Eloc b Int.zero ty) m
+           (Eloc b Ptrofs.zero ty) m
   | red_var_global: forall x ty m b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
       lred (Evar x ty) m
-           (Eloc b Int.zero ty) m
+           (Eloc b Ptrofs.zero ty) m
   | red_deref: forall b ofs ty1 ty m,
       lred (Ederef (Eval (Vptr b ofs) ty1) ty) m
            (Eloc b ofs ty) m
@@ -224,7 +224,7 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop :=
       ge.(genv_cenv)!id = Some co ->
       field_offset ge f (co_members co) = OK delta ->
       lred (Efield (Eval (Vptr b ofs) (Tstruct id a)) f ty) m
-           (Eloc b (Int.add ofs (Int.repr delta)) ty) m
+           (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m
   | red_field_union: forall b ofs id co a f ty m,
       ge.(genv_cenv)!id = Some co ->
       lred (Efield (Eval (Vptr b ofs) (Tunion id a)) f ty) m
@@ -274,10 +274,10 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
         E0 (Eparen (if b then r1 else r2) ty ty) m
   | red_sizeof: forall ty1 ty m,
       rred (Esizeof ty1 ty) m
-        E0 (Eval (Vint (Int.repr (sizeof ge ty1))) ty) m
+        E0 (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty1))) ty) m
   | red_alignof: forall ty1 ty m,
       rred (Ealignof ty1 ty) m
-        E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m
+        E0 (Eval (Vptrofs (Ptrofs.repr (alignof ge ty1))) ty) m
   | red_assign: forall b ofs ty1 v2 ty2 m v t m',
       sem_cast v2 ty2 ty1 m = Some v ->
       assign_loc ty1 m b ofs v t m' ->
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index e42091af..4393640c 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -321,7 +321,7 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Evar id) v
   | eval_Eaddrof: forall id b,
       eval_var_addr e id b ->
-      eval_expr (Eaddrof id) (Vptr b Int.zero)
+      eval_expr (Eaddrof id) (Vptr b Ptrofs.zero)
   | eval_Econst: forall cst v,
       eval_constant cst = Some v ->
       eval_expr (Econst cst) v
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 40b51bd3..aeb31fe2 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -49,6 +49,9 @@ Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
 Definition make_singleconst (f: float32) :=  Econst (Osingleconst f).
 
+Definition make_ptrofsconst (n: Z) :=
+  if Archi.ptr64 then make_longconst (Int64.repr n) else make_intconst (Int.repr n).
+
 Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e.
 Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e.
 
@@ -106,7 +109,7 @@ Definition make_longofsingle (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Olonguofsingle e
   end.
 
-Definition make_cmp_ne_zero (e: expr) :=
+Definition make_cmpu_ne_zero (e: expr) :=
   match e with
   | Ebinop (Ocmp c) e1 e2 => e
   | Ebinop (Ocmpu c) e1 e2 => e
@@ -114,7 +117,7 @@ Definition make_cmp_ne_zero (e: expr) :=
   | Ebinop (Ocmpfs c) e1 e2 => e
   | Ebinop (Ocmpl c) e1 e2 => e
   | Ebinop (Ocmplu c) e1 e2 => e
-  | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
+  | _ => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
   end.
 
 (** Variants of [sizeof] and [alignof] that check that the given type is complete. *)
@@ -139,12 +142,12 @@ Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
   | I16, Signed => Eunop Ocast16signed e
   | I16, Unsigned => Eunop Ocast16unsigned e
   | I32, _ => e
-  | IBool, _ => make_cmp_ne_zero e
+  | IBool, _ => make_cmpu_ne_zero e
   end.
 
 Definition make_cast (from to: type) (e: expr) :=
   match classify_cast from to with
-  | cast_case_neutral => OK e
+  | cast_case_pointer => OK e
   | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
   | cast_case_f2f => OK e
   | cast_case_s2s => OK e
@@ -161,10 +164,10 @@ Definition make_cast (from to: type) (e: expr) :=
   | cast_case_l2s si1 => OK (make_singleoflong e si1)
   | cast_case_f2l si2 => OK (make_longoffloat e si2)
   | cast_case_s2l si2 => OK (make_longofsingle e si2)
+  | cast_case_i2bool => OK (make_cmpu_ne_zero e)
   | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
   | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero))
-  | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
-  | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
+  | cast_case_l2bool => OK (Ebinop (Ocmplu Cne) e (make_longconst Int64.zero))
   | cast_case_struct id1 id2 => OK e
   | cast_case_union id1 id2 => OK e
   | cast_case_void => OK e
@@ -176,11 +179,10 @@ Definition make_cast (from to: type) (e: expr) :=
 
 Definition make_boolean (e: expr) (ty: type) :=
   match classify_bool ty with
-  | bool_case_i => make_cmp_ne_zero e
+  | bool_case_i => make_cmpu_ne_zero e
   | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
   | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)
-  | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
-  | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)
+  | bool_case_l => Ebinop (Ocmplu Cne) e (make_longconst Int64.zero)
   | bool_default => e   (**r should not happen *)
   end.
 
@@ -188,12 +190,11 @@ Definition make_boolean (e: expr) (ty: type) :=
 
 Definition make_notbool (e: expr) (ty: type) :=
   match classify_bool ty with
-  | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero))
+  | bool_case_i => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
   | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
   | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero))
-  | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
-  | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero))
-  | _ => Error (msg "Cshmgen.make_notbool")
+  | bool_case_l => OK (Ebinop (Ocmplu Ceq) e (make_longconst Int64.zero))
+  | bool_default => Error (msg "Cshmgen.make_notbool")
   end.
 
 Definition make_neg (e: expr) (ty: type) :=
@@ -202,7 +203,7 @@ Definition make_neg (e: expr) (ty: type) :=
   | neg_case_f => OK (Eunop Onegf e)
   | neg_case_s => OK (Eunop Onegfs e)
   | neg_case_l _ => OK (Eunop Onegl e)
-  | _ => Error (msg "Cshmgen.make_neg")
+  | neg_default => Error (msg "Cshmgen.make_neg")
   end.
 
 Definition make_absfloat (e: expr) (ty: type) :=
@@ -211,14 +212,14 @@ Definition make_absfloat (e: expr) (ty: type) :=
   | neg_case_f => OK (Eunop Oabsf e)
   | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e))
   | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg))
-  | _ => Error (msg "Cshmgen.make_absfloat")
+  | neg_default => Error (msg "Cshmgen.make_absfloat")
   end.
 
 Definition make_notint (e: expr) (ty: type) :=
   match classify_notint ty with
   | notint_case_i _ => OK (Eunop Onotint e)
   | notint_case_l _ => OK (Eunop Onotl e)
-  | _ => Error (msg "Cshmgen.make_notint")
+  | notint_default => Error (msg "Cshmgen.make_notint")
   end.
 
 (** Binary operators *)
@@ -239,42 +240,59 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
   | bin_default => Error (msg "Cshmgen.make_binarith")
   end.
 
+Definition make_add_ptr_int (ce: composite_env) (ty: type) (si: signedness) (e1 e2: expr) :=
+  do sz <- sizeof ce ty;
+  if Archi.ptr64 then
+    let n := make_longconst (Int64.repr sz) in
+    OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si)))
+  else
+    let n := make_intconst (Int.repr sz) in
+    OK (Ebinop Oadd e1 (Ebinop Omul n e2)).
+
+Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) :=
+  do sz <- sizeof ce ty;
+  if Archi.ptr64 then
+    let n := make_longconst (Int64.repr sz) in
+    OK (Ebinop Oaddl e1 (Ebinop Omull n e2))
+  else
+    let n := make_intconst (Int.repr sz) in
+    OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))).
+
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
-  | add_case_pi ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e1 (Ebinop Omul n e2))
-  | add_case_ip ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e2 (Ebinop Omul n e1))
-  | add_case_pl ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
-  | add_case_lp ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
-  | add_default =>
-      make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
+  | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2
+  | add_case_pl ty => make_add_ptr_long ce ty e1 e2
+  | add_case_ip si ty => make_add_ptr_int ce ty si e2 e1
+  | add_case_lp ty => make_add_ptr_long ce ty e2 e1
+  | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
   end.
 
 Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
-  | sub_case_pi ty =>
+  | sub_case_pi ty si =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Osub e1 (Ebinop Omul n e2))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Osubl e1 (Ebinop Omull n (make_longofint e2 si)))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Odivl (Ebinop Osubl e1 e2) n)
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Osubl e1 (Ebinop Omull n e2))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
       make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
   end.
@@ -333,11 +351,20 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   | shift_default => Error (msg "Cshmgen.make_shr")
   end.
 
+Definition make_cmp_ptr (c: comparison) (e1 e2: expr) :=
+  Ebinop (if Archi.ptr64 then Ocmplu c else Ocmpu c) e1 e2.
+
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
-  | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
-  | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2))
-  | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2)
+  | cmp_case_pp => OK (make_cmp_ptr c e1 e2)
+  | cmp_case_pi si =>
+      OK (make_cmp_ptr c e1 (if Archi.ptr64 then make_longofint e2 si else e2))
+  | cmp_case_ip si =>
+      OK (make_cmp_ptr c (if Archi.ptr64 then make_longofint e1 si else e1) e2)
+  | cmp_case_pl =>
+      OK (make_cmp_ptr c e1 (if Archi.ptr64 then e2 else Eunop Ointoflong e2))
+  | cmp_case_lp =>
+      OK (make_cmp_ptr c (if Archi.ptr64 then e1 else Eunop Ointoflong e1) e2)
   | cmp_default =>
       make_binarith
         (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c)
@@ -421,7 +448,9 @@ Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr)
           Error (MSG "Undefined struct " :: CTX id :: nil)
       | Some co =>
           do ofs <- field_offset ce f (co_members co);
-          OK (Ebinop Oadd a (make_intconst (Int.repr ofs)))
+          OK (if Archi.ptr64
+              then Ebinop Oaddl a (make_longconst (Int64.repr ofs))
+              else Ebinop Oadd a (make_intconst (Int.repr ofs)))
       end
   | Tunion id _ =>
       OK a
@@ -469,9 +498,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
       do addr <- make_field_access ce (typeof b) i tb;
       make_load addr ty
   | Clight.Esizeof ty' ty =>
-      do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz))
+      do sz <- sizeof ce ty'; OK(make_ptrofsconst sz)
   | Clight.Ealignof ty' ty =>
-      do al <- alignof ce ty'; OK(make_intconst (Int.repr al))
+      do al <- alignof ce ty'; OK(make_ptrofsconst al)
   end
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 8bc97b99..09e31cb2 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -37,7 +37,7 @@ Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.
   unfold transl_program; intros.
-  eapply match_transform_partial_program2. 
+  eapply match_transform_partial_program2.
   eexact H.
 - intros. destruct f; simpl in H0.
 + monadInv H0. constructor; auto.
@@ -109,7 +109,7 @@ Lemma transl_alignof_blockcopy:
 Proof.
   intros. destruct H.
   unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
-  split. 
+  split.
 - symmetry. apply Ctypes.sizeof_stable; auto.
 - revert C. induction t; simpl; auto;
   destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
@@ -119,10 +119,10 @@ Lemma field_offset_stable:
   forall (cunit prog: Clight.program) id co f,
   linkorder cunit prog ->
   cunit.(prog_comp_env)!id = Some co ->
-  prog.(prog_comp_env)!id = Some co /\ 
+  prog.(prog_comp_env)!id = Some co /\
   field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co).
 Proof.
-  intros. 
+  intros.
   assert (C: composite_consistent cunit.(prog_comp_env) co).
   { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
     apply prog_comp_env_eq. }
@@ -134,7 +134,7 @@ Proof.
   rewrite ! (alignof_stable _ _ A) by auto.
   rewrite ! (sizeof_stable _ _ A) by auto.
   destruct (ident_eq f f1); eauto.
-Qed. 
+Qed.
 
 (** * Properties of the translation functions *)
 
@@ -245,6 +245,19 @@ Proof.
   intros. unfold make_floatconst. econstructor. reflexivity.
 Qed.
 
+Lemma make_ptrofsconst_correct:
+  forall n e le m,
+  eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)).
+Proof.
+  intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF.
+- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n).
+  apply make_longconst_correct.
+  symmetry; auto with ptrofs.
+- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n).
+  apply make_intconst_correct.
+  symmetry; auto with ptrofs.
+Qed.
+
 Lemma make_singleoffloat_correct:
   forall a n e le m,
   eval_expr ge e le m a (Vfloat n) ->
@@ -276,38 +289,62 @@ Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correc
 Hint Constructors eval_expr eval_exprlist: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
-Lemma make_cmp_ne_zero_correct:
+Lemma make_cmpu_ne_zero_correct:
   forall e le m a n,
   eval_expr ge e le m a (Vint n) ->
-  eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)).
+  eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)).
 Proof.
   intros.
-  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero))
+  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero))
                                        (Vint (if Int.eq n Int.zero then Int.zero else Int.one))).
-    econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool.
-    unfold Int.cmp. destruct (Int.eq n Int.zero); auto.
+  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
+    unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. }
   assert (CMP: forall ob,
                Val.of_optbool ob = Vint n ->
                n = (if Int.eq n Int.zero then Int.zero else Int.one)).
-    intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
+  { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
     rewrite Int.eq_false. auto. apply Int.one_not_zero.
-    rewrite Int.eq_true. auto.
+    rewrite Int.eq_true. auto. }
   destruct a; simpl; auto. destruct b; auto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. unfold Val.cmpfs in H6.
-  destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
   simpl in H6. unfold Val.cmpl in H6.
   destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
   simpl in H6. unfold Val.cmplu in H6.
-  destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity.
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity.
+Qed.
+
+Lemma make_cmpu_ne_zero_correct_ptr:
+  forall e le m a b i,
+  eval_expr ge e le m a (Vptr b i) ->
+  Archi.ptr64 = false ->
+  Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true ->
+  eval_expr ge e le m (make_cmpu_ne_zero a) Vone.
+Proof.
+  intros.
+  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone).
+  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
+    unfold Mem.weak_valid_pointer in H1. rewrite H0, H1.
+    rewrite Int.eq_true; auto. }
+  assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)).
+  { intros. destruct ob as [[]|]; discriminate. }
+  assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)).
+  { intros. destruct ob as [[]|]; discriminate. }
+  destruct a; simpl; auto. destruct b0; auto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_BOOL; eauto.
+- inv H; eelim OF_BOOL; eauto.
 Qed.
 
 Lemma make_cast_int_correct:
@@ -320,10 +357,27 @@ Proof.
   destruct si; eauto with cshm.
   destruct si; eauto with cshm.
   auto.
-  apply make_cmp_ne_zero_correct; auto.
+  apply make_cmpu_ne_zero_correct; auto.
 Qed.
 
-Hint Resolve make_cast_int_correct: cshm.
+Lemma make_longofint_correct:
+  forall e le m a n si,
+  eval_expr ge e le m a (Vint n) ->
+  eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)).
+Proof.
+  intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm.
+Qed.
+
+Hint Resolve make_cast_int_correct make_longofint_correct: cshm.
+
+Ltac InvEval :=
+  match goal with
+  | [ H: None = Some _ |- _ ] => discriminate
+  | [ H: Some _ = Some _ |- _ ] => inv H; InvEval
+  | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
+  | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
+  | _ => idtac
+  end.
 
 Lemma make_cast_correct:
   forall e le m a b v ty1 ty2 v',
@@ -333,59 +387,51 @@ Lemma make_cast_correct:
   eval_expr ge e le m b v'.
 Proof.
   intros. unfold make_cast, sem_cast in *;
-  destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm.
-  (* single -> int *)
+  destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm.
+- (* single -> int *)
   unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm.
-  (* float -> int *)
-  destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2.
+- (* float -> int *)
   apply make_cast_int_correct.
-  unfold cast_float_int in E. unfold make_intoffloat.
-  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
-  (* single -> int *)
-  destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2.
+  unfold cast_float_int in Heqo. unfold make_intoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
+- (* single -> int *)
   apply make_cast_int_correct.
-  unfold cast_single_int in E. unfold make_intofsingle.
-  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
-  (* long -> int *)
-  unfold make_longofint, cast_int_long. destruct si1; eauto with cshm.
-  (* long -> float *)
+  unfold cast_single_int in Heqo. unfold make_intofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
+- (* long -> float *)
   unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm.
-  (* long -> single *)
+- (* long -> single *)
   unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm.
-  (* float -> long *)
-  destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2.
-  unfold cast_float_long in E. unfold make_longoffloat.
-  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
-  (* single -> long *)
-  destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2.
-  unfold cast_single_long in E. unfold make_longofsingle.
-  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
-  (* float -> bool *)
+- (* float -> long *)
+  unfold cast_float_long in Heqo. unfold make_longoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
+- (* single -> long *)
+  unfold cast_single_long in Heqo. unfold make_longofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
+- (* int -> bool *)
+  apply make_cmpu_ne_zero_correct; auto.
+- (* pointer (32 bits) -> bool *)
+  eapply make_cmpu_ne_zero_correct_ptr; eauto.
+- (* long -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
+  destruct (Int64.eq i Int64.zero); auto.
+- (* pointer (64 bits) -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1.
+  rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity.
+- (* float -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
   destruct (Float.cmp Ceq f Float.zero); auto.
-  (* single -> bool *)
+- (* single -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq.
   destruct (Float32.cmp Ceq f Float32.zero); auto.
-  (* long -> bool *)
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp.
-  destruct (Int64.eq i Int64.zero); auto.
-  (* int -> bool *)
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
-  destruct (Int.eq i Int.zero); auto.
-  (* pointer -> bool *)
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2.
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true.
-  unfold Mem.weak_valid_pointer in VALID; rewrite VALID. 
-  auto.
-  (* struct *)
-  destruct (ident_eq id1 id2); inv H2; auto.
-  (* union *)
-  destruct (ident_eq id1 id2); inv H2; auto.
+- (* struct *)
+  destruct (ident_eq id1 id2); inv H1; auto.
+- (* union *)
+  destruct (ident_eq id1 id2); inv H1; auto.
 Qed.
 
 Lemma make_boolean_correct:
@@ -397,29 +443,28 @@ Lemma make_boolean_correct:
     /\ Val.bool_of_val vb b.
 Proof.
   intros. unfold make_boolean. unfold bool_val in H0.
-  destruct (classify_bool ty); destruct v; inv H0.
-(* int *)
-  econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto.
+  destruct (classify_bool ty); destruct v; InvEval.
+- (* int *)
+  econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto.
   destruct (Int.eq i Int.zero); simpl; constructor.
-(* float *)
+- (* ptr 32 bits *)
+  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor.
+- (* long *)
+  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto.
+  destruct (Int64.eq i Int64.zero); simpl; constructor.
+- (* ptr 64 bits *)
+  exists Vone; split.
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
+  unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity.
+  constructor.
+- (* float *)
   econstructor; split. econstructor; eauto with cshm. simpl. eauto.
   unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq.
   destruct (Float.cmp Cne f Float.zero); constructor.
-(* single *)
+- (* single *)
   econstructor; split. econstructor; eauto with cshm. simpl. eauto.
   unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq.
   destruct (Float32.cmp Cne f Float32.zero); constructor.
-(* pointer *)
-  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
-  unfold Val.cmpu, Val.cmpu_bool. simpl.
-  destruct (Int.eq i Int.zero); simpl; constructor.
-  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
-  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2.
-  unfold Val.cmpu, Val.cmpu_bool. simpl.
-  unfold Mem.weak_valid_pointer in V; rewrite V. constructor.
-(* long *)
-  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto.
-  destruct (Int64.eq i Int64.zero); simpl; constructor.
 Qed.
 
 Lemma make_neg_correct:
@@ -454,11 +499,24 @@ Lemma make_notbool_correct:
   eval_expr ge e le m a va ->
   eval_expr ge e le m c v.
 Proof.
-  unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1;
-  destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0.
+  unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1.
+  destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
+  destruct (Int.eq i Int.zero); auto.
+- destruct Archi.ptr64 eqn:SF; inv SEM.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
   econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
-  unfold Mem.weak_valid_pointer in V; rewrite V. auto.
+  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
+  destruct (Int64.eq i Int64.zero); auto.
+- destruct Archi.ptr64 eqn:SF; inv SEM.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
+  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool.
+  destruct (Float.cmp Ceq f Float.zero); auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool.
+  destruct (Float32.cmp Ceq f Float32.zero); auto.
 Qed.
 
 Lemma make_notint_correct:
@@ -563,17 +621,48 @@ Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
 Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
+  assert (A: forall ty si a b c e le m va vb v,
+             make_add_ptr_int cunit.(prog_comp_env) ty si a b = OK c ->
+             eval_expr ge e le m a va -> eval_expr ge e le m b vb ->
+             sem_add_ptr_int (prog_comp_env prog) ty si va vb = Some v ->
+             eval_expr ge e le m c v).
+  { unfold make_add_ptr_int, sem_add_ptr_int; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
+    destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  - destruct va; InvEval; destruct vb; inv SEM.
+  + eauto with cshm.
+  + econstructor; eauto with cshm.
+    simpl. rewrite SF. f_equal. f_equal. f_equal.
+    assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
+    { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
+    auto with ptrofs.
+  - destruct va; InvEval; destruct vb; inv SEM.
+  + eauto with cshm.
+  + econstructor; eauto with cshm.
+    simpl. rewrite SF. f_equal. f_equal. f_equal.
+    assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
+    auto with ptrofs.
+  }
+  assert (B: forall ty a b c e le m va vb v,
+             make_add_ptr_long cunit.(prog_comp_env) ty a b = OK c ->
+             eval_expr ge e le m a va -> eval_expr ge e le m b vb ->
+             sem_add_ptr_long (prog_comp_env prog) ty va vb = Some v ->
+             eval_expr ge e le m c v).
+  { unfold make_add_ptr_long, sem_add_ptr_long; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
+    destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  - destruct va; InvEval; destruct vb; inv SEM.
+  + eauto with cshm.
+  + econstructor; eauto with cshm.
+    simpl. rewrite SF. f_equal. f_equal. f_equal. auto with ptrofs.
+  - destruct va; InvEval; destruct vb; inv SEM.
+  + eauto with cshm.
+  + econstructor; eauto with cshm.
+    simpl. rewrite SF. f_equal. f_equal. f_equal.
+    assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
+    auto with ptrofs.
+  }
   red; unfold make_add, sem_add;
   intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_add tya tyb); try (monadInv MAKE).
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+  destruct (classify_add tya tyb); eauto.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -582,25 +671,61 @@ Proof.
   red; unfold make_sub, sem_sub;
   intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_sub tya tyb); try (monadInv MAKE).
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM.
-  destruct (eq_block b0 b1); try discriminate.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
+  assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
+  { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
+  auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
+  assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
+  auto with ptrofs.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ.
   set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
+  destruct va; InvEval; destruct vb; InvEval.
+  destruct (eq_block b0 b1); try discriminate.
   destruct (zlt 0 sz); try discriminate.
-  destruct (zle sz Int.max_signed); simpl in H0; inv H0.
+  destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
+  assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz).
+  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. }
+  destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
++ assert (E: Int64.signed (Int64.repr sz) = sz).
+  { apply Int64.signed_repr.
+    replace Int64.max_signed with Ptrofs.max_signed.
+    generalize Int64.min_signed_neg; omega.
+    unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
   econstructor; eauto with cshm.
-  rewrite dec_eq_true; simpl.
-  assert (E: Int.signed (Int.repr sz) = sz).
-  { apply Int.signed_repr. generalize Int.min_signed_neg; omega. }
+  rewrite SF, dec_eq_true. simpl.
+  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
+  rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction.
+  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
+  rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal.
+  apply f_equal. symmetry. auto with ptrofs.
++ assert (E: Int.signed (Int.repr sz) = sz).
+  { apply Int.signed_repr.
+    replace Int.max_signed with Ptrofs.max_signed.
+    generalize Int.min_signed_neg; omega.
+    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity.
+  }
+  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
   rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
   rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
-  rewrite andb_false_r; auto.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal.
+  symmetry. auto with ptrofs.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
+  auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
+  assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
+  auto with ptrofs.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -716,25 +841,61 @@ Proof.
   unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
 Qed.
 
+Lemma make_cmp_ptr_correct:
+  forall cmp e le m a va b vb v,
+  cmp_ptr m cmp va vb = Some v ->
+  eval_expr ge e le m a va ->
+  eval_expr ge e le m b vb ->
+  eval_expr ge e le m (make_cmp_ptr cmp a b) v.
+Proof.
+  unfold cmp_ptr, make_cmp_ptr; intros.
+  destruct Archi.ptr64.
+- econstructor; eauto.
+- econstructor; eauto. simpl. unfold Val.cmpu.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto.
+Qed.
+
+Remark make_ptrofs_of_int_correct:
+  forall e le m a i si,
+  eval_expr ge e le m a (Vint i) ->
+  eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)).
+Proof.
+  intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF.
+- unfold make_longofint. destruct si.
++ replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)).
+  eauto with cshm.
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
++ replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)).
+  eauto with cshm.
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
+- destruct si.
++ replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto.
+  symmetry. auto with ptrofs.
++ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto.
+  symmetry. auto with ptrofs.
+Qed.
+
+Remark make_ptrofs_of_int64_correct:
+  forall e le m a i,
+  eval_expr ge e le m a (Vlong i) ->
+  eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)).
+Proof.
+  intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF.
+- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto.
+  symmetry. auto with ptrofs.
+- econstructor; eauto. simpl. apply f_equal. apply f_equal.
+  apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr.
+Qed.
+
 Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp).
 Proof.
   red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_cmp tya tyb).
-- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto.
-- inv MAKE. destruct vb; try discriminate.
-  set (vb := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb.
-  unfold Val.cmpu. rewrite E. auto.
-- inv MAKE. destruct va; try discriminate.
-  set (va := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va.
-  unfold Val.cmpu. rewrite E. auto.
+- inv MAKE. eapply make_cmp_ptr_correct; eauto.
+- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
+- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
+- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
+- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -806,7 +967,7 @@ Lemma make_memcpy_correct:
   step ge (State f s k e le m) E0 (State f Sskip k e le m').
 Proof.
   intros. inv H1; try congruence.
-  monadInv H3. 
+  monadInv H3.
   exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
   change le with (set_optvar None Vundef le) at 2.
   econstructor.
@@ -954,8 +1115,8 @@ Lemma match_env_alloc_variables:
 Proof.
   induction 2; simpl; intros.
 - inv H0. exists te1; split. constructor. auto.
-- monadInv H2. monadInv EQ. simpl in *. 
-  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. 
+- monadInv H2. monadInv EQ. simpl in *.
+  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ.
   exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)).
   auto.
   constructor.
@@ -1042,49 +1203,53 @@ Lemma transl_expr_lvalue_correct:
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
 Proof.
   apply eval_expr_lvalue_ind; intros; try (monadInv TR).
-(* const int *)
+- (* const int *)
   apply make_intconst_correct.
-(* const float *)
+- (* const float *)
   apply make_floatconst_correct.
-(* const single *)
+- (* const single *)
   apply make_singleconst_correct.
-(* const long *)
+- (* const long *)
   apply make_longconst_correct.
-(* temp var *)
+- (* temp var *)
   constructor; auto.
-(* addrof *)
+- (* addrof *)
   simpl in TR. auto.
-(* unop *)
+- (* unop *)
   eapply transl_unop_correct; eauto.
-(* binop *)
+- (* binop *)
   eapply transl_binop_correct; eauto.
-(* cast *)
+- (* cast *)
   eapply make_cast_correct; eauto.
-(* sizeof *)
-  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct.
-(* alignof *)
-  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct.
-(* rvalue out of lvalue *)
+- (* sizeof *)
+  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
+- (* alignof *)
+  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
+- (* rvalue out of lvalue *)
   exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
   eapply make_load_correct; eauto.
-(* var local *)
+- (* var local *)
   exploit (me_local _ _ MENV); eauto. intros EQ.
   econstructor. eapply eval_var_addr_local. eauto.
-(* var global *)
+- (* var global *)
   econstructor. eapply eval_var_addr_global.
   eapply match_env_globals; eauto.
   rewrite symbols_preserved. auto.
-(* deref *)
+- (* deref *)
   simpl in TR. eauto.
-(* field struct *)
-  unfold make_field_access in EQ0. rewrite H1 in EQ0. 
+- (* field struct *)
+  unfold make_field_access in EQ0. rewrite H1 in EQ0.
   destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
   exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
-  rewrite <- B in EQ1. 
-  eapply eval_Ebinop; eauto.
-  apply make_intconst_correct.
-  simpl. unfold ge in *; simpl in *. congruence.
-(* field union *)
+  rewrite <- B in EQ1.
+  assert (x0 = delta) by (unfold ge in *; simpl in *; congruence).
+  subst x0.
+  destruct Archi.ptr64 eqn:SF.
++ eapply eval_Ebinop; eauto using make_longconst_correct.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
++ eapply eval_Ebinop; eauto using make_intconst_correct.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
+- (* field union *)
   unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
   auto.
 Qed.
@@ -1389,7 +1554,7 @@ Proof.
   rewrite H in CF. simpl in CF. inv CF.
   econstructor; split.
   apply plus_one. econstructor; eauto.
-  eapply transl_expr_correct with (cunit := cu); eauto. 
+  eapply transl_expr_correct with (cunit := cu); eauto.
   eapply transl_arglist_correct with (cunit := cu); eauto.
   erewrite typlist_of_arglist_eq by eauto.
   eapply transl_fundef_sig1; eauto.
@@ -1558,7 +1723,7 @@ Proof.
   econstructor; eauto. constructor.
 
 - (* internal function *)
-  inv H. inv TR. monadInv H5. 
+  inv H. inv TR. monadInv H5.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   exploit match_env_alloc_variables; eauto.
   apply match_env_empty.
@@ -1568,7 +1733,7 @@ Proof.
   simpl. erewrite transl_vars_names by eauto. assumption.
   simpl. assumption.
   simpl. assumption.
-  simpl; eauto. 
+  simpl; eauto.
   simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
   simpl. econstructor; eauto.
   unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
@@ -1628,7 +1793,7 @@ End CORRECTNESS.
 Instance TransfCshmgenLink : TransfLink match_prog.
 Proof.
   red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
-  generalize H. 
+  generalize H.
 Local Transparent Ctypes.Linker_program.
   simpl; unfold link_program.
   destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
@@ -1638,15 +1803,15 @@ Local Transparent Ctypes.Linker_program.
            (prog_comp_env_eq p2) EQ) as (env & P & Q).
   intros E.
   eapply Linking.link_match_program; eauto.
-- intros. 
+- intros.
 Local Transparent Linker_fundef Linking.Linker_fundef.
-  inv H3; inv H4; simpl in H2. 
+  inv H3; inv H4; simpl in H2.
 + discriminate.
 + destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto.
 + destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto.
 + destruct (external_function_eq ef ef0 && typelist_eq args args0 &&
          type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2.
-  InvBooleans. subst ef0. econstructor; split. 
+  InvBooleans. subst ef0. econstructor; split.
   simpl; rewrite dec_eq_true; eauto.
   left; constructor. congruence.
 - intros. exists tt. auto.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 6b2924e4..2f731068 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -84,16 +84,16 @@ Section SIMPLE_EXPRS.
 Variable e: env.
 Variable m: mem.
 
-Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
+Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop :=
   | esl_loc: forall b ofs ty,
       eval_simple_lvalue (Eloc b ofs ty) b ofs
   | esl_var_local: forall x ty b,
       e!x = Some(b, ty) ->
-      eval_simple_lvalue (Evar x ty) b Int.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      eval_simple_lvalue (Evar x ty) b Int.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
       eval_simple_lvalue (Ederef r ty) b ofs
@@ -102,7 +102,7 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
       typeof r = Tstruct id a ->
       ge.(genv_cenv)!id = Some co ->
       field_offset ge f (co_members co) = OK delta ->
-      eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta))
   | esl_field_union: forall r f ty b ofs id co a,
       eval_simple_rvalue r (Vptr b ofs) ->
       typeof r = Tunion id a ->
@@ -133,9 +133,9 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       sem_cast v1 (typeof r1) ty m = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
-      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
+      eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1)))
   | esr_alignof: forall ty1 ty,
-      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))).
+      eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))).
 
 Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
@@ -813,13 +813,13 @@ Ltac StepR REC C' a :=
   exists v; constructor.
 (* var *)
   exploit safe_inv; eauto; simpl. intros [b A].
-  exists b; exists Int.zero.
+  exists b; exists Ptrofs.zero.
   intuition. apply esl_var_local; auto. apply esl_var_global; auto.
 (* field *)
   StepR IHa (fun x => C(Efield x f0 ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl.
   intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction.
-  destruct TY as (co & delta & CE & OFS). exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
+  destruct TY as (co & delta & CE & OFS). exists b; exists (Ptrofs.add ofs (Ptrofs.repr delta)); econstructor; eauto.
   destruct TY as (co & CE).  exists b; exists ofs; econstructor; eauto.
 (* valof *)
   destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index fd7a6b96..914328be 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -55,7 +55,7 @@ Inductive expr : Type :=
                                              (**r function call [r1(rargs)] *)
   | Ebuiltin (ef: external_function) (tyargs: typelist) (rargs: exprlist) (ty: type)
                                                  (**r builtin function call *)
-  | Eloc (b: block) (ofs: int) (ty: type)
+  | Eloc (b: block) (ofs: ptrofs) (ty: type)
                        (**r memory location, result of evaluating a l-value *)
   | Eparen (r: expr) (tycast: type) (ty: type)   (**r marked subexpression *)
 
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 9faa6d40..0794743d 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -78,15 +78,19 @@ with typelist : Type :=
   | Tnil: typelist
   | Tcons: type -> typelist -> typelist.
 
+Lemma intsize_eq: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}.
+Proof.
+  decide equality.
+Defined.
+
 Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
 with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}.
 Proof.
-  assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: attr), {x=y} + {x<>y}).
   { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
-  generalize ident_eq zeq bool_dec ident_eq; intros.
+  generalize ident_eq zeq bool_dec ident_eq intsize_eq; intros.
   decide equality.
   decide equality.
   decide equality.
@@ -272,7 +276,7 @@ Fixpoint alignof (env: composite_env) (t: type) : Z :=
       | Tlong _ _ => Archi.align_int64
       | Tfloat F32 _ => 4
       | Tfloat F64 _ => Archi.align_float64
-      | Tpointer _ _ => 4
+      | Tpointer _ _ => if Archi.ptr64 then 8 else 4
       | Tarray t' _ _ => alignof env t'
       | Tfunction _ _ _ => 1
       | Tstruct id _ | Tunion id _ =>
@@ -299,11 +303,11 @@ Proof.
     exists 1%nat; auto.
     exists 2%nat; auto.
     exists 0%nat; auto.
-    (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
+    unfold Archi.align_int64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
   destruct f.
     exists 2%nat; auto.
-    (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
-  exists 2%nat; auto.
+    unfold Archi.align_float64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
+  exists (if Archi.ptr64 then 3%nat else 2%nat); destruct Archi.ptr64; auto.
   apply IHt.
   exists 0%nat; auto.
   destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
@@ -335,7 +339,7 @@ Fixpoint sizeof (env: composite_env) (t: type) : Z :=
   | Tlong _ _ => 8
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
-  | Tpointer _ _ => 4
+  | Tpointer _ _ => if Archi.ptr64 then 8 else 4
   | Tarray t' n _ => sizeof env t' * Z.max 0 n
   | Tfunction _ _ _ => 1
   | Tstruct id _ | Tunion id _ =>
@@ -348,6 +352,7 @@ Proof.
   induction t; simpl; try omega.
   destruct i; omega.
   destruct f; omega.
+  destruct Archi.ptr64; omega.
   change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega.
   destruct (env!i). apply co_sizeof_pos. omega.
   destruct (env!i). apply co_sizeof_pos. omega.
@@ -370,8 +375,8 @@ Proof.
   induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl.
 - apply Zdivide_refl.
 - destruct i; apply Zdivide_refl.
-- exists (8 / Archi.align_int64); reflexivity.
-- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity.
+- exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity.
+- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity.
 - apply Zdivide_refl.
 - apply Z.divide_mul_l; auto.
 - apply Zdivide_refl.
@@ -576,7 +581,7 @@ Definition access_mode (ty: type) : mode :=
   | Tfloat F32 _ => By_value Mfloat32
   | Tfloat F64 _ => By_value Mfloat64
   | Tvoid => By_nothing
-  | Tpointer _ _ => By_value Mint32
+  | Tpointer _ _ => By_value Mptr
   | Tarray _ _ _ => By_reference
   | Tfunction _ _ _ => By_reference
   | Tstruct _ _ => By_copy
@@ -609,7 +614,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
   | Tlong _ _ => 8
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
-  | Tpointer _ _ => 4
+  | Tpointer _ _ => if Archi.ptr64 then 8 else 4
   | Tarray t' _ _ => alignof_blockcopy env t'
   | Tfunction _ _ _ => 1
   | Tstruct id _ | Tunion id _ =>
@@ -633,9 +638,14 @@ Proof.
     rewrite two_power_nat_two_p. rewrite ! inj_S.
     change 8 with (two_p 3). apply two_p_monotone. omega.
   }
-  induction ty; simpl; auto.
+  induction ty; simpl.
+  auto.
   destruct i; auto.
+  auto.
   destruct f; auto.
+  destruct Archi.ptr64; auto.
+  apply IHty.
+  auto.
   destruct (env!i); auto.
   destruct (env!i); auto.
 Qed.
@@ -714,20 +724,16 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist :=
 
 Definition typ_of_type (t: type) : AST.typ :=
   match t with
-  | Tfloat F32 _ => AST.Tsingle
-  | Tfloat _ _ => AST.Tfloat
+  | Tvoid => AST.Tint
+  | Tint _ _ _ => AST.Tint
   | Tlong _ _ => AST.Tlong
-  | _ => AST.Tint
+  | Tfloat F32 _ => AST.Tsingle
+  | Tfloat F64 _ => AST.Tfloat
+  | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr
   end.
 
 Definition opttyp_of_type (t: type) : option AST.typ :=
-  match t with
-  | Tvoid => None
-  | Tfloat F32 _ => Some AST.Tsingle
-  | Tfloat _ _ => Some AST.Tfloat
-  | Tlong _ _ => Some AST.Tlong
-  | _ => Some AST.Tint
-  end.
+  if type_eq t Tvoid then None else Some (typ_of_type t).
 
 Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
   match tl with
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 440e4e84..ba1d34fb 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -26,6 +26,12 @@ Local Open Scope error_monad_scope.
 Definition strict := false.
 Opaque strict.
 
+Definition size_t : type :=
+  if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr.
+
+Definition ptrdiff_t : type :=
+  if Archi.ptr64 then Tlong Signed noattr else Tint I32 Signed noattr.
+
 (** * Operations over types *)
 
 (** The type of a member of a composite (struct or union).
@@ -107,20 +113,14 @@ Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type :=
   match op with
   | Oadd =>
       match classify_add ty1 ty2 with
-      | add_case_pi ty | add_case_ip ty
-      | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr)
+      | add_case_pi ty _ | add_case_ip _ ty
+      | add_case_pl ty   | add_case_lp ty => OK (Tpointer ty noattr)
       | add_default => binarith_type ty1 ty2 "operator +"
       end
   | Osub =>
       match classify_sub ty1 ty2 with
-      | sub_case_pi ty | sub_case_pl ty => OK (Tpointer ty noattr)
-(*
-      | sub_case_pp ty1 ty2 =>
-          if type_eq (remove_attributes ty1) (remove_attributes ty2)
-          then OK (Tint I32 Signed noattr)
-          else Error (msg "operator - : incompatible pointer types")
-*)
-      | sub_case_pp ty => OK (Tint I32 Signed noattr)
+      | sub_case_pi ty _ | sub_case_pl ty => OK (Tpointer ty noattr)
+      | sub_case_pp ty => OK ptrdiff_t
       | sub_default => binarith_type ty1 ty2 "operator infix -"
       end
   | Omul => binarith_type ty1 ty2 "operator infix *"
@@ -281,9 +281,13 @@ Inductive wt_val : val -> type -> Prop :=
       wt_int n sz sg ->
       wt_val (Vint n) (Tint sz sg a)
   | wt_val_ptr_int: forall b ofs sg a,
+      Archi.ptr64 = false ->
       wt_val (Vptr b ofs) (Tint I32 sg a)
   | wt_val_long: forall n sg a,
       wt_val (Vlong n) (Tlong sg a)
+  | wt_val_ptr_long: forall b ofs sg a,
+      Archi.ptr64 = true ->
+      wt_val (Vptr b ofs) (Tlong sg a)
   | wt_val_float: forall f a,
       wt_val (Vfloat f) (Tfloat F64 a)
   | wt_val_single: forall f a,
@@ -291,7 +295,11 @@ Inductive wt_val : val -> type -> Prop :=
   | wt_val_pointer: forall b ofs ty a,
       wt_val (Vptr b ofs) (Tpointer ty a)
   | wt_val_int_pointer: forall n ty a,
+      Archi.ptr64 = false ->
       wt_val (Vint n) (Tpointer ty a)
+  | wt_val_long_pointer: forall n ty a,
+      Archi.ptr64 = true ->
+      wt_val (Vlong n) (Tpointer ty a)
   | wt_val_array: forall b ofs ty sz a,
       wt_val (Vptr b ofs) (Tarray ty sz a)
   | wt_val_function: forall b ofs tyargs tyres cc,
@@ -359,9 +367,9 @@ Inductive wt_rvalue : expr -> Prop :=
       wt_cast (typeof r2) ty -> wt_cast (typeof r3) ty ->
       wt_rvalue (Econdition r1 r2 r3 ty)
   | wt_Esizeof: forall ty,
-      wt_rvalue (Esizeof ty (Tint I32 Unsigned noattr))
+      wt_rvalue (Esizeof ty size_t)
   | wt_Ealignof: forall ty,
-      wt_rvalue (Ealignof ty (Tint I32 Unsigned noattr))
+      wt_rvalue (Ealignof ty size_t)
   | wt_Eassign: forall l r,
       wt_lvalue l -> wt_rvalue r -> wt_cast (typeof r) (typeof l) ->
       wt_rvalue (Eassign l r (typeof l))
@@ -522,11 +530,10 @@ Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
 
 Ltac DestructCases :=
   match goal with
-  | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x; DestructCases
-  | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x; DestructCases
-  | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases
-  | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; DestructCases
-  | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases
+  | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
+  | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases
+  | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases
+  | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
   | [H: Some _ = Some _ |- _ ] => inv H; DestructCases
   | [H: None = Some _ |- _ ] => discriminate
   | [H: OK _ = OK _ |- _ ] => inv H; DestructCases
@@ -628,11 +635,14 @@ Definition econst_int (n: int) (sg: signedness) : expr :=
   (Eval (Vint n) (Tint I32 sg noattr)).
 
 Definition econst_ptr_int (n: int) (ty: type) : expr :=
-  (Eval (Vint n) (Tpointer ty noattr)).
+  (Eval (if Archi.ptr64 then Vlong (Int64.repr (Int.unsigned n)) else Vint n) (Tpointer ty noattr)).
 
 Definition econst_long (n: int64) (sg: signedness) : expr :=
   (Eval (Vlong n) (Tlong sg noattr)).
 
+Definition econst_ptr_long (n: int64) (ty: type) : expr :=
+  (Eval (if Archi.ptr64 then Vlong n else Vint (Int64.loword n)) (Tpointer ty noattr)).
+
 Definition econst_float (n: float) : expr :=
   (Eval (Vfloat n) (Tfloat F64 noattr)).
 
@@ -684,10 +694,10 @@ Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr :=
   OK (Econdition r1 r2 r3 ty).
 
 Definition esizeof (ty: type) : expr :=
-  Esizeof ty (Tint I32 Unsigned noattr).
+  Esizeof ty size_t.
 
 Definition ealignof (ty: type) : expr :=
-  Ealignof ty (Tint I32 Unsigned noattr).
+  Ealignof ty size_t.
 
 Definition eassign (l r: expr) : res expr :=
   do x1 <- check_lval l; do x2 <- check_rval r;
@@ -954,7 +964,9 @@ Lemma binarith_type_cast:
   binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t.
 Proof.
   unfold wt_cast, binarith_type, classify_binarith; intros; DestructCases;
-  simpl; split; try congruence. destruct f; congruence.
+  simpl; split; try congruence;
+  try (destruct Archi.ptr64; congruence).
+  destruct f0; congruence.
 Qed.
 
 Lemma typeconv_cast:
@@ -969,6 +981,16 @@ Proof.
   destruct i; auto.
 Qed.
 
+Lemma wt_cast_int:
+  forall i1 s1 a1 i2 s2 a2, wt_cast (Tint i1 s1 a1) (Tint i2 s2 a2).
+Proof.
+  intros; red; simpl.
+  destruct Archi.ptr64; [ | destruct (Ctypes.intsize_eq i2 I32)].
+- destruct i2; congruence.
+- subst i2; congruence.
+- destruct i2; congruence.
+Qed.
+ 
 Lemma type_combine_cast:
   forall t1 t2 t,
   type_combine t1 t2 = OK t ->
@@ -980,9 +1002,9 @@ Proof.
   unfold wt_cast; destruct t1; try discriminate; destruct t2; simpl in H; inv H.
 - simpl; split; congruence.
 - destruct (intsize_eq i i0 && signedness_eq s s0); inv H3.
-  simpl; destruct i; split; congruence.
+  split; apply wt_cast_int.
 - destruct (signedness_eq s s0); inv H3.
-  simpl; split; congruence.
+  simpl; split; try congruence; destruct Archi.ptr64; congruence.
 - destruct (floatsize_eq f f0); inv H3.
   simpl; destruct f0; split; congruence.
 - monadInv H3. simpl; split; congruence.
@@ -1006,11 +1028,14 @@ Proof.
   destruct (typeconv t1) eqn:T1; try discriminate;
   destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast.
 - split; apply typeconv_cast; unfold wt_cast.
-  rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
+  rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. 
+  rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. 
 - split; apply typeconv_cast; unfold wt_cast.
-  rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
+  rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. 
+  rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. 
 - split; apply typeconv_cast; unfold wt_cast.
-  rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
+  rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. 
+  rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. 
 Qed.
 
 Section SOUNDNESS_CONSTRUCTORS.
@@ -1063,7 +1088,7 @@ Qed.
 Lemma econst_ptr_int_sound:
   forall n ty, wt_expr ce e (econst_ptr_int n ty).
 Proof.
-  unfold econst_ptr_int; auto with ty.
+  unfold econst_ptr_int; intros. destruct Archi.ptr64 eqn:SF; auto with ty.
 Qed.
 
 Lemma econst_long_sound:
@@ -1072,6 +1097,12 @@ Proof.
   unfold econst_long; auto with ty.
 Qed.
 
+Lemma econst_ptr_long_sound:
+  forall n ty, wt_expr ce e (econst_ptr_long n ty).
+Proof.
+  unfold econst_ptr_long; intros. destruct Archi.ptr64 eqn:SF; auto with ty.
+Qed.
+
 Lemma econst_float_sound:
   forall n, wt_expr ce e (econst_float n).
 Proof.
@@ -1354,28 +1385,17 @@ Proof.
 - destruct (Int.eq n Int.zero); auto.
 Qed.
 
-Hint Resolve pres_cast_int_int: ty.
+Lemma wt_val_casted:
+  forall v ty, val_casted v ty -> wt_val v ty.
+Proof.
+  induction 1; constructor; auto. 
+- rewrite <- H; apply pres_cast_int_int.
+Qed.
 
 Lemma pres_sem_cast:
   forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2.
 Proof.
-  unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty.
-- constructor. apply (pres_cast_int_int I8 s).
-- constructor. apply (pres_cast_int_int I16 s).
-- destruct (Int.eq n Int.zero); auto with ty.
-- constructor. apply (pres_cast_int_int I8 s).
-- constructor. apply (pres_cast_int_int I16 s).
-- destruct (Int64.eq n Int64.zero); auto with ty.
-- constructor. apply (pres_cast_int_int I8 s).
-- constructor. apply (pres_cast_int_int I16 s).
-- destruct (Float.cmp Ceq f Float.zero); auto with ty.
-- constructor. apply (pres_cast_int_int I8 s).
-- constructor. apply (pres_cast_int_int I16 s).
-- destruct (Float32.cmp Ceq f Float32.zero); auto with ty.
-- constructor. reflexivity.
-- destruct (Int.eq n Int.zero); auto with ty.
-- constructor. reflexivity.
-- constructor. reflexivity.
+  intros. apply wt_val_casted. eapply cast_val_is_casted; eauto.
 Qed.
 
 Lemma pres_sem_binarith:
@@ -1459,6 +1479,8 @@ Proof with (try discriminate).
 - inv H; eauto.
 - DestructCases; eauto.
 - DestructCases; eauto.
+- DestructCases; eauto.
+- DestructCases; eauto.
 - unfold sem_binarith in H0.
   set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *.
   destruct (sem_cast v1 ty1 ty') as [v1'|]...
@@ -1476,10 +1498,11 @@ Proof.
   intros until m; intros TY SEM WT1 WT2.
   destruct op; simpl in TY; simpl in SEM.
 - (* add *)
-  unfold sem_add in SEM; DestructCases; auto with ty.
+  unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty.
   eapply pres_sem_binarith; eauto; intros; exact I.
 - (* sub *)
   unfold sem_sub in SEM; DestructCases; auto with ty.
+  unfold ptrdiff_t, Vptrofs. destruct Archi.ptr64; auto with ty.
   eapply pres_sem_binarith; eauto; intros; exact I.
 - (* mul *)
   unfold sem_mul in SEM. eapply pres_sem_binarith; eauto; intros; exact I.
@@ -1522,13 +1545,12 @@ Proof.
   intros until v; intros TY SEM WT1.
   destruct op; simpl in TY; simpl in SEM.
 - (* notbool *)
-  unfold sem_notbool in SEM; DestructCases.
-  destruct (Int.eq i Int.zero); constructor; auto with ty.
-  destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty.
-  destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty.
-  destruct (Int.eq i Int.zero); constructor; auto with ty.
-  constructor. constructor.
-  destruct (Int64.eq i Int64.zero); constructor; auto with ty.
+  unfold sem_notbool in SEM.
+  assert (A: ty = Tint I32 Signed noattr) by (destruct (classify_bool ty1); inv TY; auto).
+  assert (B: exists b, v = Val.of_bool b).
+  { destruct (bool_val v1 ty1 m); inv SEM. exists (negb b); auto. }
+  destruct B as [b B].
+  rewrite A, B. destruct b; constructor; auto with ty.
 - (* notint *)
   unfold sem_notint in SEM; DestructCases; auto with ty.
 - (* neg *)
@@ -1542,16 +1564,18 @@ Lemma wt_load_result:
   access_mode ty = By_value chunk ->
   wt_val (Val.load_result chunk v) ty.
 Proof.
-  intros until v; intros AC. destruct ty; simpl in AC; try discriminate.
-  destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl; destruct v; auto with ty.
-  constructor; red. apply Int.sign_ext_idem; omega.
-  constructor; red. apply Int.zero_ext_idem; omega.
-  constructor; red. apply Int.sign_ext_idem; omega.
-  constructor; red. apply Int.zero_ext_idem; omega.
-  constructor; red. apply Int.zero_ext_idem; omega.
-  inv AC; simpl; destruct v; auto with ty.
-  destruct f; inv AC; simpl; destruct v; auto with ty.
-  inv AC; simpl; destruct v; auto with ty.
+  unfold access_mode, Val.load_result. remember Archi.ptr64 as ptr64. 
+  intros until v; intros AC. destruct ty; simpl in AC; try discriminate AC.
+- destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl.
+  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
+  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
+  destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
+- inv AC. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
+- destruct f; inv AC; destruct v; auto with ty.
+- inv AC. unfold Mptr. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
 Qed.
 
 Lemma wt_decode_val:
@@ -1560,19 +1584,26 @@ Lemma wt_decode_val:
   wt_val (decode_val chunk vl) ty.
 Proof.
   intros until vl; intros ACC.
-  destruct ty; simpl in ACC; try discriminate.
-- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val;
+  assert (LR: forall v, wt_val (Val.load_result chunk v) ty) by (eauto using wt_load_result).
+  destruct ty; simpl in ACC; try discriminate. 
+- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val.
   destruct (proj_bytes vl); auto with ty.
   constructor; red. apply Int.sign_ext_idem; omega.
+  destruct (proj_bytes vl); auto with ty.
   constructor; red. apply Int.zero_ext_idem; omega.
+  destruct (proj_bytes vl); auto with ty.
   constructor; red. apply Int.sign_ext_idem; omega.
+  destruct (proj_bytes vl); auto with ty.
   constructor; red. apply Int.zero_ext_idem; omega.
-  apply wt_load_result. auto.
+  destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. 
+  destruct (proj_bytes vl); auto with ty.
   constructor; red. apply Int.zero_ext_idem; omega.
-- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty.
+- inv ACC. unfold decode_val. destruct (proj_bytes vl). auto with ty.
+  destruct Archi.ptr64 eqn:SF; auto with ty. 
 - destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty.
-- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty.
-  apply wt_load_result. auto.
+- inv ACC. unfold decode_val. destruct (proj_bytes vl).
+  unfold Mptr in *. destruct Archi.ptr64 eqn:SF; auto with ty.
+  unfold Mptr in *. destruct Archi.ptr64 eqn:SF; auto with ty.
 Qed.
 
 Lemma wt_deref_loc:
@@ -1604,15 +1635,19 @@ Qed.
 Lemma wt_bool_cast:
   forall ty, wt_bool ty -> wt_cast ty type_bool.
 Proof.
-  unfold wt_bool, wt_cast; unfold classify_bool; intros. destruct ty; simpl in *; try congruence. destruct f; congruence.
+  unfold wt_bool, wt_cast; unfold classify_bool; intros.
+  destruct ty; simpl in *; try congruence;
+  try (destruct Archi.ptr64; congruence).
+  destruct f; congruence.
 Qed.
 
 Lemma wt_cast_self:
   forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2.
 Proof.
   unfold wt_cast; intros. destruct t2; simpl in *; try congruence.
-  destruct i; congruence.
-  destruct f; congruence.
+- apply (wt_cast_int i s a i s a).
+- destruct Archi.ptr64; congruence.
+- destruct f; congruence.
 Qed.
 
 Lemma binarith_type_int32s:
@@ -1672,8 +1707,8 @@ Proof.
 - (* seqor false *) subst. constructor. auto. apply wt_bool_cast; auto.
   red; intros. inv H0; auto with ty.
 - (* condition *) constructor. destruct b; auto. destruct b; auto. red; auto.
-- (* sizeof *) constructor; auto with ty.
-- (* alignof *) constructor; auto with ty.
+- (* sizeof *)  unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty.
+- (* alignof *)  unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty.
 - (* assign *) inversion H5. constructor. eapply pres_sem_cast; eauto.
 - (* assignop *) subst tyres l r. constructor. auto.
   constructor. constructor. eapply wt_deref_loc; eauto.
@@ -2105,7 +2140,7 @@ Proof.
   intros. inv H. econstructor. constructor.
   apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto.
   intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto.
-  instantiate (1 := (Vptr b Int.zero)). rewrite Genv.find_funct_find_funct_ptr. auto.
+  instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto.
 Qed.
 
 End PRESERVATION.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 7228cd75..19518aea 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -12,18 +12,9 @@
 
 (** Compile-time evaluation of initializers for global C variables. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
+Require Import Coqlib Maps Errors.
+Require Import Integers Floats Values AST Memory Globalenvs.
+Require Import Ctypes Cop Csyntax.
 
 Open Scope error_monad_scope.
 
@@ -38,7 +29,7 @@ Open Scope error_monad_scope.
 (** [constval a] evaluates the constant expression [a].
 
 If [a] is a r-value, the returned value denotes:
-- [Vint n], [Vfloat f]: the corresponding number
+- [Vint n], [Vlong n], [Vfloat f], [Vsingle f]: the corresponding number
 - [Vptr id ofs]: address of global variable [id] plus byte offset [ofs]
 - [Vundef]: erroneous expression
 
@@ -88,9 +79,9 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val :=
   | Ecast r ty =>
       do v1 <- constval ce r; do_cast v1 (typeof r) ty
   | Esizeof ty1 ty =>
-      OK (Vint (Int.repr (sizeof ce ty1)))
+      OK (Vptrofs (Ptrofs.repr (sizeof ce ty1)))
   | Ealignof ty1 ty =>
-      OK (Vint (Int.repr (alignof ce ty1)))
+      OK (Vptrofs (Ptrofs.repr (alignof ce ty1)))
   | Eseqand r1 r2 ty =>
       do v1 <- constval ce r1;
       do v2 <- constval ce r2;
@@ -119,7 +110,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val :=
   | Ecomma r1 r2 ty =>
       do v1 <- constval ce r1; constval ce r2
   | Evar x ty =>
-      OK(Vptr x Int.zero)
+      OK(Vptr x Ptrofs.zero)
   | Ederef r ty =>
       constval ce r
   | Efield l f ty =>
@@ -128,7 +119,9 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val :=
           do co <- lookup_composite ce id;
           do delta <- field_offset ce f (co_members co);
           do v <- constval ce l;
-          OK (Val.add v (Vint (Int.repr delta)))
+          OK (if Archi.ptr64
+              then Val.addl v (Vlong (Int64.repr delta))
+              else Val.add v (Vint (Int.repr delta)))
       | Tunion id _ =>
           constval ce l
       | _ =>
@@ -161,11 +154,13 @@ Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res ini
   | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n)
   | Vint n, Tint I16 sg _ => OK(Init_int16 n)
   | Vint n, Tint I32 sg _ => OK(Init_int32 n)
-  | Vint n, Tpointer _ _ => OK(Init_int32 n)
+  | Vint n, Tpointer _ _ => assertion (negb Archi.ptr64); OK(Init_int32 n)
   | Vlong n, Tlong _ _ => OK(Init_int64 n)
+  | Vlong n, Tpointer _ _ => assertion (Archi.ptr64); OK(Init_int64 n)
   | Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
-  | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); OK(Init_addrof id ofs)
+  | Vptr id ofs, Tlong _ _ => assertion (Archi.ptr64); OK(Init_addrof id ofs)
   | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index d5f39d7d..fee25c48 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -12,21 +12,9 @@
 
 (** Compile-time evaluation of initializers for global C variables. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
+Require Import Coqlib Maps.
+Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep.
+Require Import Ctypes Cop Csyntax Csem.
 Require Import Initializers.
 
 Open Scope error_monad_scope.
@@ -77,23 +65,23 @@ Section SIMPLE_EXPRS.
 Variable e: env.
 Variable m: mem.
 
-Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
+Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop :=
   | esl_loc: forall b ofs ty,
       eval_simple_lvalue (Eloc b ofs ty) b ofs
   | esl_var_local: forall x ty b,
       e!x = Some(b, ty) ->
-      eval_simple_lvalue (Evar x ty) b Int.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      eval_simple_lvalue (Evar x ty) b Int.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
       eval_simple_lvalue (Ederef r ty) b ofs
   | esl_field_struct: forall r f ty b ofs id co a delta,
       eval_simple_rvalue r (Vptr b ofs) ->
       typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta ->
-      eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta))
   | esl_field_union: forall r f ty b ofs id a,
       eval_simple_rvalue r (Vptr b ofs) ->
       typeof r = Tunion id a ->
@@ -123,9 +111,9 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       sem_cast v1 (typeof r1) ty m = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
-      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
+      eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1)))
   | esr_alignof: forall ty1 ty,
-      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1)))
+      eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1)))
   | esr_seqand_true: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
       eval_simple_rvalue r2 v2 ->
@@ -418,9 +406,9 @@ Proof.
   (* cast *)
   eapply sem_cast_match; eauto.
   (* sizeof *)
-  constructor.
+  auto.
   (* alignof *)
-  constructor.
+  auto.
   (* seqand *)
   destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2.
   exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
@@ -458,9 +446,10 @@ Proof.
   (* field struct *)
   rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ.
   exploit constval_rvalue; eauto. intro MV. inv MV.
-  simpl. replace x0 with delta by congruence. econstructor; eauto.
-  rewrite ! Int.add_assoc. f_equal. apply Int.add_commut.
-  simpl. auto.
+  replace x0 with delta by congruence. rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)).
+  simpl; destruct Archi.ptr64 eqn:SF;
+  econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs.
+  destruct Archi.ptr64; auto.
   (* field union *)
   rewrite H0 in CV. eauto.
 Qed.
@@ -617,30 +606,36 @@ Proof.
   exploit sem_cast_match; eauto. intros D.
   unfold Genv.store_init_data.
   inv D.
-  (* int *)
-  destruct ty; try discriminate.
-  destruct i0; inv EQ2.
+- (* int *)
+  remember Archi.ptr64 as ptr64.  destruct ty; try discriminate EQ2.
++ destruct i0; inv EQ2.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
   simpl in H2; inv H2. assumption.
   simpl in H2; inv H2. assumption.
-  inv EQ2. simpl in H2; inv H2. assumption.
-  (* long *)
-  destruct ty; inv EQ2. simpl in H2; inv H2. assumption.
-  (* float *)
++ destruct ptr64; inv EQ2. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption.
+- (* Long *)
+  remember Archi.ptr64 as ptr64. destruct ty; inv EQ2.
++ simpl in H2; inv H2. assumption.
++ simpl in H2; unfold Mptr in H2; destruct Archi.ptr64; inv H4. 
+  inv H2; assumption.
+- (* float *)
   destruct ty; try discriminate.
   destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
-  (* single *)
+- (* single *)
   destruct ty; try discriminate.
   destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
-  (* pointer *)
+- (* pointer *)
   unfold inj in H.
-  assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32).
-    destruct ty; inv EQ2; inv H2.
-    destruct i; inv H5. intuition congruence. auto.
+  assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr).
+  { remember Archi.ptr64 as ptr64.
+    destruct ty; inversion EQ2.
+    destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto.
+    subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto.
+    inv H2. auto. }
   destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H.
-  rewrite Int.add_zero in H3. auto.
-  (* undef *)
+  rewrite Ptrofs.add_zero in H3. auto.
+- (* undef *)
   discriminate.
 Qed.
 
@@ -651,19 +646,24 @@ Lemma transl_init_single_size:
   transl_init_single ge ty a = OK data ->
   init_data_size data = sizeof ge ty.
 Proof.
-  intros. monadInv H. destruct x0.
+  intros. monadInv H. remember Archi.ptr64 as ptr64. destruct x0.
 - monadInv EQ2.
 - destruct ty; try discriminate.
   destruct i0; inv EQ2; auto.
-  inv EQ2; auto.
-- destruct ty; inv EQ2; auto.
+  destruct ptr64; inv EQ2. 
+Local Transparent sizeof.
+  unfold sizeof. rewrite <- Heqptr64; auto.
+- destruct ty; inv EQ2; auto. 
+  unfold sizeof. destruct Archi.ptr64; inv H0; auto.
 - destruct ty; try discriminate.
   destruct f0; inv EQ2; auto.
 - destruct ty; try discriminate.
   destruct f0; inv EQ2; auto.
 - destruct ty; try discriminate.
   destruct i0; inv EQ2; auto.
-  inv EQ2; auto.
+  destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto.
+  destruct ptr64; inv EQ2. simpl. rewrite <- Heqptr64; auto.
+  inv EQ2. unfold init_data_size, sizeof. auto.
 Qed.
 
 Notation idlsize := init_data_list_size.
@@ -710,6 +710,7 @@ with tr_init_struct_size:
   sizeof_struct ge pos fl <= sizeof ge ty ->
   idlsize data + pos = sizeof ge ty.
 Proof.
+Local Opaque sizeof.
 - destruct 1; simpl.
 + erewrite transl_init_single_size by eauto. omega.
 + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. 
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 64e52df8..ad7b296a 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -736,9 +736,15 @@ Remark sem_cast_deterministic:
   v1 = v2.
 Proof.
   unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence.
-  destruct v; try congruence.
-  destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H.
-  destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0.
+- destruct v; try congruence.
+  destruct Archi.ptr64; try discriminate.
+  destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)); inv H.
+  destruct (Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i)); inv H0.
+  auto.
+- destruct v; try congruence. 
+  destruct (negb Archi.ptr64); try discriminate.
+  destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)); inv H.
+  destruct (Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i)); inv H0.
   auto.
 Qed.
 
@@ -756,9 +762,13 @@ Qed.
 Lemma static_bool_val_sound:
   forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b.
 Proof.
-  intros until b; unfold bool_val. destruct (classify_bool t); destruct v; auto.
-  intros E. unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool in E.
-  rewrite ! pred_dec_false in E by (apply Mem.perm_empty). discriminate.
+  assert (A: forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false).
+  { unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool; intros.
+    rewrite ! pred_dec_false by (apply Mem.perm_empty). auto. }  
+  intros until b; unfold bool_val.
+  destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto.
+- rewrite A; congruence.
+- simpl; rewrite A; congruence.
 Qed.
 
 Lemma step_makeif:
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 580f02c2..c0086a38 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -40,7 +40,7 @@ Definition is_liftable_var (cenv: compilenv) (a: expr) : option ident :=
 
 Definition make_cast (a: expr) (tto: type) : expr :=
   match classify_cast (typeof a) tto with
-  | cast_case_neutral => a
+  | cast_case_pointer => a
   | cast_case_i2i I32 _ => a
   | cast_case_f2f => a
   | cast_case_s2s => a
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 48a7a773..8ed924e5 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -187,21 +187,23 @@ Lemma val_casted_load_result:
   Val.load_result chunk v = v.
 Proof.
   intros. inversion H; clear H; subst v ty; simpl in H0.
-  destruct sz.
+- destruct sz.
   destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence.
   destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence.
   clear H1. inv H0. auto.
   inversion H0; clear H0; subst chunk. simpl in *.
   destruct (Int.eq n Int.zero); subst n; reflexivity.
-  inv H0; auto.
-  inv H0; auto.
-  inv H0; auto.
-  inv H0; auto.
-  inv H0; auto.
-  inv H0; auto.
-  discriminate.
-  discriminate.
-  discriminate.
+- inv H0; auto.
+- inv H0; auto.
+- inv H0; auto.
+- inv H0. unfold Mptr, Val.load_result; destruct Archi.ptr64; auto. 
+- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto.
+- inv H0. unfold Val.load_result; rewrite H1; auto.
+- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto.
+- inv H0. unfold Val.load_result; rewrite H1; auto.
+- discriminate.
+- discriminate.
+- discriminate.
 Qed.
 
 Lemma val_casted_inject:
@@ -209,7 +211,7 @@ Lemma val_casted_inject:
   Val.inject f v v' -> val_casted v ty -> val_casted v' ty.
 Proof.
   intros. inv H; auto.
-  inv H0; constructor.
+  inv H0; constructor; auto.
   inv H0; constructor.
 Qed.
 
@@ -250,7 +252,7 @@ Proof.
     econstructor; eauto.
   unfold sem_cast, make_cast in *.
   destruct (classify_cast (typeof a) tto); auto.
-  destruct v1; inv H0; auto.
+  destruct v1; destruct Archi.ptr64; inv H0; auto.
   destruct sz2; auto. destruct v1; inv H0; auto.
   destruct v1; inv H0; auto.
   destruct v1; inv H0; auto.
@@ -269,10 +271,19 @@ Lemma cast_typeconv:
   val_casted v ty ->
   sem_cast v ty (typeconv ty) m = Some v.
 Proof.
-  induction 1; simpl; auto.
-- destruct sz; auto.
-- unfold sem_cast. simpl. rewrite dec_eq_true; auto.
+  induction 1; simpl.
+- unfold sem_cast, classify_cast; destruct sz, Archi.ptr64; auto.
+- auto.
+- auto.
+- unfold sem_cast, classify_cast; destruct Archi.ptr64; auto.
+- auto.
+- unfold sem_cast; simpl; rewrite H; auto.
+- unfold sem_cast; simpl; rewrite H; auto.
+- unfold sem_cast; simpl; rewrite H; auto.
+- unfold sem_cast; simpl; rewrite H; auto.
+- unfold sem_cast; simpl. rewrite dec_eq_true; auto.
 - unfold sem_cast. simpl. rewrite dec_eq_true; auto.
+- auto.
 Qed.
 
 Lemma step_Sdebug_temp:
@@ -380,13 +391,13 @@ Lemma match_envs_assign_lifted:
   e!id = Some(b, ty) ->
   val_casted v ty ->
   Val.inject f v tv ->
-  assign_loc ge ty m b Int.zero v m' ->
+  assign_loc ge ty m b Ptrofs.zero v m' ->
   VSet.mem id cenv = true ->
   match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi.
 Proof.
   intros. destruct H. generalize (me_vars0 id); intros MV; inv MV; try congruence.
   rewrite ENV in H0; inv H0. inv H3; try congruence.
-  unfold Mem.storev in H0. rewrite Int.unsigned_zero in H0.
+  unfold Mem.storev in H0. rewrite Ptrofs.unsigned_zero in H0.
   constructor; eauto; intros.
 (* vars *)
   destruct (peq id0 id). subst id0.
@@ -746,7 +757,8 @@ Proof.
   unfold access_mode; intros.
   assert (size_chunk chunk = sizeof ge ty).
   {
-    destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto.
+    destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto;
+    unfold Mptr; simpl; destruct Archi.ptr64; auto.
   }
   omega.
 Qed.
@@ -1019,10 +1031,10 @@ Proof.
   destruct (zeq (sizeof tge ty) 0).
 + (* special case size = 0 *)
   assert (bytes = nil).
-  { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof tge ty)).
+  { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)).
     omega. congruence. }
   subst.
-  destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil)
+  destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil)
   as [tm' SB].
   simpl. red; intros; omegaContradiction.
   exists tm'.
@@ -1038,15 +1050,15 @@ Proof.
   exploit Mem.loadbytes_length; eauto. intros LEN.
   assert (SZPOS: sizeof tge ty > 0).
   { generalize (sizeof_pos tge ty); omega. }
-  assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof tge ty) Cur Nonempty).
+  assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
-  assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof tge ty) Cur Nonempty).
+  assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
     replace (sizeof tge ty) with (Z_of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
     rewrite LEN. apply nat_of_Z_eq. omega.
-  assert (PSRC: Mem.perm m bsrc (Int.unsigned osrc) Cur Nonempty).
+  assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
-  assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty).
+  assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
   exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
   exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
@@ -1449,7 +1461,7 @@ Proof.
   rewrite ENV in H6; inv H6.
   inv H0; try congruence.
   assert (chunk0 = chunk). simpl in H. congruence. subst chunk0.
-  assert (v0 = v). unfold Mem.loadv in H2. rewrite Int.unsigned_zero in H2. congruence. subst v0.
+  assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0.
   exists tv; split; auto. constructor; auto.
   simpl in H; congruence.
   simpl in H; congruence.
@@ -1464,13 +1476,13 @@ Proof.
   rewrite H1.
   exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
   rewrite ENV in H; inv H.
-  exists b'; exists Int.zero; split.
+  exists b'; exists Ptrofs.zero; split.
   apply eval_Evar_local; auto.
   econstructor; eauto.
 (* global var *)
   rewrite H2.
   exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
-  exists l; exists Int.zero; split.
+  exists l; exists Ptrofs.zero; split.
   apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved.
   destruct GLOB as [bound GLOB1]. inv GLOB1.
   econstructor; eauto.
@@ -1484,7 +1496,7 @@ Proof.
   inversion B. subst.
   econstructor; econstructor; split.
   eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto.
-  econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
 (* field union *)
   rewrite <- comp_env_preserved in *.
   exploit eval_simpl_expr; eauto. intros [tv [A B]].
@@ -1721,12 +1733,12 @@ Lemma match_cont_find_funct:
   exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd.
 Proof.
   intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG.
-  inv H1; simpl in H0; try discriminate. destruct (Int.eq_dec ofs1 Int.zero); try discriminate.
+  inv H1; simpl in H0; try discriminate. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); try discriminate.
   subst ofs1.
   assert (f b1 = Some(b1, 0)).
     apply DOMAIN. eapply FUNCTIONS; eauto.
   rewrite H1 in H2; inv H2.
-  rewrite Int.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto.
+  rewrite Ptrofs.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto.
 Qed.
 
 (** Relating execution states *)