Make casts of pointers to _Bool semantically well defined (again).

In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds).  Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL.  Hence, this kind of casts was temporarily given undefined semantics.

This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid.  This reinstates the equivalence between casts to _Bool and comparisons != 0.  The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass.  The pass was lightly modified to work around the issue.

14 files changed, 368 insertions, 323 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7e966ffe..00d77b00 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -645,11 +645,11 @@ Section EXPRS.
 Variable e: env.
 Variable w: world.
 
-Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) :=
+Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) :=
   match vtl, tl with
   | nil, Tnil => Some nil
   | (v1,t1)::vtl, Tcons t1' tl =>
-      do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl)
+      do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl)
   | _, _ => None
   end.
 
@@ -772,7 +772,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Ecast r1 ty =>
       match is_val r1 with
       | Some(v1, ty1) =>
-          do v <- sem_cast v1 ty1 ty;
+          do v <- sem_cast v1 ty1 ty m;
           topred (Rred "red_cast" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Ecast x ty) (step_expr RV r1 m)
@@ -811,7 +811,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
           check type_eq ty1 ty;
-          do v <- sem_cast v2 ty2 ty1;
+          do v <- sem_cast v2 ty2 ty1 m;
           do w',t,m' <- do_assign_loc w ty1 m b ofs v;
           topred (Rred "red_assign" (Eval v ty) m' t)
       | _, _ =>
@@ -856,7 +856,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Eparen r1 tycast ty =>
       match is_val r1 with
       | Some (v1, ty1) =>
-          do v <- sem_cast v1 ty1 tycast;
+          do v <- sem_cast v1 ty1 tycast m;
           topred (Rred "red_paren" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m)
@@ -867,7 +867,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           match classify_fun tyf with
           | fun_case_f tyargs tyres cconv =>
               do fd <- Genv.find_funct ge vf;
-              do vargs <- sem_cast_arguments vtl tyargs;
+              do vargs <- sem_cast_arguments vtl tyargs m;
               check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
               topred (Callred "red_call" fd vargs ty m)
           | _ => stuck
@@ -879,7 +879,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Ebuiltin ef tyargs rargs ty =>
       match is_val_list rargs with
       | Some vtl =>
-          do vargs <- sem_cast_arguments vtl tyargs;
+          do vargs <- sem_cast_arguments vtl tyargs m;
           match do_external ef w vargs m with
           | None => stuck
           | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t)
@@ -915,7 +915,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
       context RV to C ->
       imm_safe_t to (C r) m
   | imm_safe_t_callred: forall to C r m fd args ty,
-      callred ge r fd args ty ->
+      callred ge r m fd args ty ->
       context RV to C ->
       imm_safe_t to (C r) m.
 
@@ -961,7 +961,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
       exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
   | Ecast (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+      exists v, sem_cast v1 ty1 ty m = Some v
   | Eseqand (Eval v1 ty1) r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
   | Eseqor (Eval v1 ty1) r2 ty =>
@@ -970,7 +970,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists b, bool_val v1 ty1 m = Some b
   | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
       exists v, exists m', exists t, exists w',
-      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
       exists t, exists v1, exists w',
       ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w'
@@ -980,18 +980,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) tycast ty =>
-      exists v, sem_cast v1 ty1 tycast = Some v
+      exists v, sem_cast v1 ty1 tycast m = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
          classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
-      /\ cast_arguments rargs tyargs vl
+      /\ cast_arguments m rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs t vres m' w',
-         cast_arguments rargs tyargs vargs
+         cast_arguments m rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
       /\ possible_trace w t w'
   | _ => True
@@ -1028,7 +1028,7 @@ Qed.
 
 Lemma callred_invert:
   forall r fd args ty m,
-  callred ge r fd args ty ->
+  callred ge r m fd args ty ->
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
@@ -1124,7 +1124,7 @@ Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
   match k, rd with
   | LV, Lred _ l' m' => lred ge e a m l' m'
   | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
-  | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m
+  | RV, Callred _ fd args tyres m' => callred ge a m fd args tyres /\ m' = m
   | LV, Stuckred => ~imm_safe_t k a m
   | RV, Stuckred => ~imm_safe_t k a m
   | _, _ => False
@@ -1152,10 +1152,10 @@ Ltac monadInv :=
   end.
 
 Lemma sem_cast_arguments_sound:
-  forall rargs vtl tyargs vargs,
+  forall m rargs vtl tyargs vargs,
   is_val_list rargs = Some vtl ->
-  sem_cast_arguments vtl tyargs = Some vargs ->
-  cast_arguments rargs tyargs vargs.
+  sem_cast_arguments vtl tyargs m = Some vargs ->
+  cast_arguments m rargs tyargs vargs.
 Proof.
   induction rargs; simpl; intros.
   inv H. destruct tyargs; simpl in H0; inv H0. constructor.
@@ -1164,9 +1164,9 @@ Proof.
 Qed.
 
 Lemma sem_cast_arguments_complete:
-  forall al tyl vl,
-  cast_arguments al tyl vl ->
-  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.
+  forall m al tyl vl,
+  cast_arguments m al tyl vl ->
+  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl m = Some vl.
 Proof.
   induction 1.
   exists (@nil (val * type)); auto.
@@ -1396,7 +1396,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* cast *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct (sem_cast v ty' ty) as [v'|] eqn:?...
+  destruct (sem_cast v ty' ty m) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1433,7 +1433,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
-  destruct (sem_cast v2 ty2 ty) as [v|] eqn:?...
+  destruct (sem_cast v2 ty2 ty m) as [v|] eqn:?...
   destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?.
   exploit do_assign_loc_sound; eauto. intros [P Q].
   apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto.
@@ -1478,7 +1478,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* top *)
   destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
   destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
+  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
   destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
   apply topred_ok; auto. red. split; auto. eapply red_call; eauto.
   eapply sem_cast_arguments_sound; eauto.
@@ -1494,7 +1494,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (is_val_list rargs) as [vtl | ] eqn:?.
   exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
+  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
   destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?...
   exploit do_ef_external_sound; eauto. intros [EC PT].
   apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto.
@@ -1514,7 +1514,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* paren *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct (sem_cast v ty' tycast) as [v'|] eqn:?...
+  destruct (sem_cast v ty' tycast m) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1607,7 +1607,7 @@ Qed.
 
 Lemma callred_topred:
   forall a fd args ty m,
-  callred ge a fd args ty ->
+  callred ge a m fd args ty ->
   exists rule, step_expr RV a m = topred (Callred rule fd args ty m).
 Proof.
   induction 1; simpl.
@@ -1961,7 +1961,7 @@ Definition do_step (w: world) (s: state) : list transition :=
             then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m)
             else ret "step_for_false" (State f Sskip k e m)
         | Kreturn k =>
-            do v' <- sem_cast v ty f.(fn_return);
+            do v' <- sem_cast v ty f.(fn_return) m;
             do m' <- Mem.free_list m (blocks_of_env ge e);
             ret "step_return_2" (Returnstate v' (call_cont k) m')
         | Kswitch1 sl k =>
@@ -2165,7 +2165,7 @@ Proof with (unfold ret; eauto with coqlib).
   apply extensionality; auto.
 (* callred *)
   unfold do_step; rewrite NOTVAL.
-  exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e).
+  exploit callred_topred; eauto. instantiate (1 := w). instantiate (1 := e).
   intros (rule & STEP). exists rule.
   change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)).
   apply in_map.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 8722da69..086f4654 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -412,7 +412,7 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Ebinop op a1 a2 ty) v
   | eval_Ecast:   forall a ty v1 v,
       eval_expr a v1 ->
-      sem_cast v1 (typeof a) ty = Some v ->
+      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)))
@@ -464,7 +464,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop :=
       eval_exprlist nil Tnil nil
   | eval_Econs:   forall a bl ty tyl v1 v2 vl,
       eval_expr a v1 ->
-      sem_cast v1 (typeof a) ty = Some v2 ->
+      sem_cast v1 (typeof a) ty m = Some v2 ->
       eval_exprlist bl tyl vl ->
       eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl).
 
@@ -580,7 +580,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_assign:   forall f a1 a2 k e le m loc ofs v2 v m',
       eval_lvalue e le m a1 loc ofs ->
       eval_expr e le m a2 v2 ->
-      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
+      sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
       assign_loc ge (typeof a1) m loc ofs v m' ->
       step (State f (Sassign a1 a2) k e le m)
         E0 (State f Sskip k e le m')
@@ -647,7 +647,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Returnstate Vundef (call_cont k) m')
   | step_return_1: forall f a k e le m v v' m',
       eval_expr e le m a v ->
-      sem_cast v (typeof a) f.(fn_return) = Some v' ->
+      sem_cast v (typeof a) f.(fn_return) m = Some v' ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn (Some a)) k e le m)
         E0 (Returnstate v' (call_cont k) m')
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index ee653d50..92457586 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -60,11 +60,11 @@ Definition outcome_switch (out: outcome) : outcome :=
   | o => o
   end.
 
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop :=
   match out, t with
   | Out_normal, Tvoid => v = Vundef
   | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v
+  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t m = Some v
   | _, _ => False
   end.
 
@@ -81,7 +81,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
   | exec_Sassign:   forall e le m a1 a2 loc ofs v2 v m',
       eval_lvalue ge e le m a1 loc ofs ->
       eval_expr ge e le m a2 v2 ->
-      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
+      sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
       assign_loc ge (typeof a1) m loc ofs v m' ->
       exec_stmt e le m (Sassign a1 a2)
                E0 le m' Out_normal
@@ -168,7 +168,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
       bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out ->
-      outcome_result_value out f.(fn_return) vres ->
+      outcome_result_value out f.(fn_return) vres m3 ->
       Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index b4784028..8b3421e8 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -130,7 +130,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | _, _ => cast_case_default
   end.
 
-(** Semantics of casts.  [sem_cast v1 t1 t2 = Some v2] if value [v1],
+(** Semantics of casts.  [sem_cast v1 t1 t2 m = Some v2] if value [v1],
   viewed with static type [t1], can be converted  to type [t2],
   resulting in value [v2].  *)
 
@@ -198,7 +198,7 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
   | Unsigned => Float32.to_longu f
   end.
 
-Definition sem_cast (v: val) (t1 t2: type) : option val :=
+Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
   match classify_cast t1 t2 with
   | cast_case_neutral =>
       match v with
@@ -273,6 +273,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
   | 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 =>
@@ -586,13 +587,13 @@ Definition sem_binarith
     (sem_long: signedness -> int64 -> int64 -> option val)
     (sem_float: float -> float -> option val)
     (sem_single: float32 -> float32 -> option val)
-    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
+    (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val :=
   let c := classify_binarith t1 t2 in
   let t := binarith_type c in
-  match sem_cast v1 t1 t with
+  match sem_cast v1 t1 t m with
   | None => None
   | Some v1' =>
-  match sem_cast v2 t2 t with
+  match sem_cast v2 t2 t m with
   | None => None
   | Some v2' =>
   match c with
@@ -637,7 +638,7 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | _, _ => add_default
   end.
 
-Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+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
@@ -671,7 +672,7 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
         (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2)))
         (fun n1 n2 => Some(Vfloat(Float.add n1 n2)))
         (fun n1 n2 => Some(Vsingle(Float32.add n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** *** Subtraction *)
@@ -690,7 +691,7 @@ Definition classify_sub (ty1: type) (ty2: type) :=
   | _, _ => sub_default
   end.
 
-Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+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
@@ -722,20 +723,20 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
         (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2)))
         (fun n1 n2 => Some(Vfloat(Float.sub n1 n2)))
         (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** *** Multiplication, division, modulus *)
 
-Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.mul n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2)))
     (fun n1 n2 => Some(Vfloat(Float.mul n1 n2)))
     (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
       match sg with
@@ -759,9 +760,9 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       end)
     (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
     (fun n1 n2 => Some(Vsingle(Float32.div n1 n2)))
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
       match sg with
@@ -785,31 +786,31 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       end)
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.and n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.or n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.xor n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
 (** *** Shifts *)
 
@@ -931,7 +932,7 @@ Definition sem_cmp (c:comparison)
             Some(Val.of_bool(Float.cmp c n1 n2)))
         (fun n1 n2 =>
             Some(Val.of_bool(Float32.cmp c n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** ** Function applications *)
@@ -988,14 +989,14 @@ Definition sem_binary_operation
     (v1: val) (t1: type) (v2: val) (t2:type)
     (m: mem): option val :=
   match op with
-  | Oadd => sem_add cenv v1 t1 v2 t2
-  | Osub => sem_sub cenv v1 t1 v2 t2
-  | Omul => sem_mul v1 t1 v2 t2
-  | Omod => sem_mod v1 t1 v2 t2
-  | Odiv => sem_div v1 t1 v2 t2
-  | Oand => sem_and v1 t1 v2 t2
-  | Oor  => sem_or v1 t1 v2 t2
-  | Oxor  => sem_xor v1 t1 v2 t2
+  | Oadd => sem_add cenv v1 t1 v2 t2 m
+  | Osub => sem_sub cenv v1 t1 v2 t2 m
+  | Omul => sem_mul v1 t1 v2 t2 m
+  | Omod => sem_mod v1 t1 v2 t2 m
+  | Odiv => sem_div v1 t1 v2 t2 m
+  | Oand => sem_and v1 t1 v2 t2 m
+  | Oor  => sem_or v1 t1 v2 t2 m
+  | Oxor  => sem_xor v1 t1 v2 t2 m
   | Oshl => sem_shl v1 t1 v2 t2
   | Oshr  => sem_shr v1 t1 v2 t2
   | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
@@ -1006,10 +1007,10 @@ Definition sem_binary_operation
   | Oge => sem_cmp Cge v1 t1 v2 t2 m
   end.
 
-Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) :=
+Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) :=
   match id with
-  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s
-  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s
+  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s m
+  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s m
   end.
 
 Definition incrdecr_type (ty: type) :=
@@ -1074,11 +1075,11 @@ Ltac TrivialInject :=
   | _ => idtac
   end.
 
-Lemma sem_cast_inject:
+Lemma sem_cast_inj:
   forall v1 ty1 ty v tv1,
-  sem_cast v1 ty1 ty = Some v ->
+  sem_cast v1 ty1 ty m = Some v ->
   Val.inject f v1 tv1 ->
-  exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv.
+  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.
@@ -1087,6 +1088,8 @@ Proof.
 - 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.
 - econstructor; eauto.
@@ -1119,13 +1122,13 @@ Definition optval_self_injects (ov: option val) : Prop :=
 
 Remark sem_binarith_inject:
   forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2',
-  sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v ->
+  sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m = Some v ->
   Val.inject f v1 v1' -> Val.inject f v2 v2' ->
   (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) ->
   (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_float n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_single n1 n2)) ->
-  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'.
+  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m' = Some v' /\ Val.inject f v v'.
 Proof.
   intros.
   assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v).
@@ -1135,10 +1138,10 @@ Proof.
   unfold sem_binarith in *.
   set (c := classify_binarith t1 t2) in *.
   set (t := binarith_type c) in *.
-  destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate.
-  destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate.
-  exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1).
-  exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2).
+  destruct (sem_cast v1 t1 t m) as [w1|] eqn:C1; try discriminate.
+  destruct (sem_cast v2 t2 t m) as [w2|] eqn:C2; try discriminate.
+  exploit (sem_cast_inj v1); eauto. intros (w1' & C1' & INJ1).
+  exploit (sem_cast_inj v2); eauto. intros (w2' & C2' & INJ2).
   rewrite C1'; rewrite C2'.
   destruct c; inv INJ1; inv INJ2; discriminate || eauto.
 Qed.
@@ -1282,6 +1285,17 @@ Qed.
 
 End GENERIC_INJECTION.
 
+Lemma sem_cast_inject:
+  forall f v1 ty1 ty m v tv1 tm,
+  sem_cast v1 ty1 ty m = Some v ->
+  Val.inject f v1 tv1 ->
+  Mem.inject f m tm ->
+  exists tv, sem_cast tv1 ty1 ty tm = Some tv /\ Val.inject f v tv.
+Proof.
+  intros. eapply sem_cast_inj; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+Qed.
+
 Lemma sem_unary_operation_inject:
   forall f m m' op v1 ty1 v tv1,
   sem_unary_operation op v1 ty1 m = Some v ->
@@ -1321,20 +1335,16 @@ Qed.
 (** * Some properties of operator semantics *)
 
 (** This section collects some common-sense properties about the type
-  classification and semantic functions above.  These properties are
-  not used in the CompCert semantics preservation proofs, but increase
+  classification and semantic functions above.  Some properties are used
+  in the CompCert semantics preservation proofs.  Others are not, but increase
   confidence in the specification and its relation with the ISO C99 standard. *)
 
 (** Relation between Boolean value and casting to [_Bool] type. *)
 
 Lemma cast_bool_bool_val:
   forall v t m,
-  match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with
-  | Some v', Some b => v' = Val.of_bool b
-  | Some v', None => False
-  | None, _ => True
-  end.
-Proof.
+  sem_cast v t (Tint IBool Signed noattr) m =
+  match bool_val v t m with None => None | Some b => Some(Val.of_bool b) end.
   intros.
   assert (A: classify_bool t =
     match t with
@@ -1360,8 +1370,11 @@ Proof.
   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 (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
 Qed.
 
 (** Relation between Boolean value and Boolean negation. *)
@@ -1376,6 +1389,119 @@ Proof.
   destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
 Qed.
 
+(** Properties of values obtained by casting to a given type. *)
+
+Inductive val_casted: val -> type -> Prop :=
+  | val_casted_int: forall sz si attr n,
+      cast_int_int sz si n = n ->
+      val_casted (Vint n) (Tint sz si attr)
+  | val_casted_float: forall attr n,
+       val_casted (Vfloat n) (Tfloat F64 attr)
+  | val_casted_single: forall attr n,
+       val_casted (Vsingle n) (Tfloat F32 attr)
+  | val_casted_long: forall si attr n,
+      val_casted (Vlong n) (Tlong si attr)
+  | 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)
+  | val_casted_ptr_int: forall b ofs si attr,
+      val_casted (Vptr b ofs) (Tint I32 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,
+      val_casted (Vptr b ofs) (Tunion id attr)
+  | val_casted_void: forall v,
+      val_casted v Tvoid.
+
+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.
+  intros. destruct sz; simpl; auto.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
+  destruct (Int.eq i Int.zero); auto.
+Qed.
+
+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.
+Qed.
+
+(** 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.
+Qed.
+
+Lemma cast_idempotent:
+  forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> sem_cast v' ty' ty' m = Some v'.
+Proof.
+  intros. apply cast_val_casted. eapply cast_val_is_casted; eauto.
+Qed.
+
 (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *)
 
 Module ArithConv.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 539b6826..30e6200d 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -187,12 +187,12 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement :=
 
 (** Extract the values from a list of function arguments *)
 
-Inductive cast_arguments: exprlist -> typelist -> list val -> Prop :=
+Inductive cast_arguments (m: mem): exprlist -> typelist -> list val -> Prop :=
   | cast_args_nil:
-      cast_arguments Enil Tnil nil
+      cast_arguments m Enil Tnil nil
   | cast_args_cons: forall v ty el targ1 targs v1 vl,
-      sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl ->
-      cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
+      sem_cast v ty targ1 m = Some v1 -> cast_arguments m el targs vl ->
+      cast_arguments m (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
 
 (** ** Reduction semantics for expressions *)
 
@@ -249,7 +249,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m
         E0 (Eval v ty) m
   | red_cast: forall ty v1 ty1 m v,
-      sem_cast v1 ty1 ty = Some v ->
+      sem_cast v1 ty1 ty m = Some v ->
       rred (Ecast (Eval v1 ty1) ty) m
         E0 (Eval v ty) m
   | red_seqand_true: forall v1 ty1 r2 ty m,
@@ -279,7 +279,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ealignof ty1 ty) m
         E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m
   | red_assign: forall b ofs ty1 v2 ty2 m v t m',
-      sem_cast v2 ty2 ty1 = Some v ->
+      sem_cast v2 ty2 ty1 m = Some v ->
       assign_loc ty1 m b ofs v t m' ->
       rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m
          t (Eval v ty1) m'
@@ -303,11 +303,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ecomma (Eval v ty1) r2 ty) m
         E0 r2 m
   | red_paren: forall v1 ty1 ty2 ty m v,
-      sem_cast v1 ty1 ty2 = Some v ->
+      sem_cast v1 ty1 ty2 m = Some v ->
       rred (Eparen (Eval v1 ty1) ty2 ty) m
         E0 (Eval v ty) m
   | red_builtin: forall ef tyargs el ty m vargs t vres m',
-      cast_arguments el tyargs vargs ->
+      cast_arguments m el tyargs vargs ->
       external_call ef ge vargs m t vres m' ->
       rred (Ebuiltin ef tyargs el ty) m
          t (Eval vres ty) m'.
@@ -316,13 +316,13 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
 (** Head reduction for function calls.
     (More exactly, identification of function calls that can reduce.) *)
 
-Inductive callred: expr -> fundef -> list val -> type -> Prop :=
-  | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs,
+Inductive callred: expr -> mem -> fundef -> list val -> type -> Prop :=
+  | red_call: forall vf tyf m tyargs tyres cconv el ty fd vargs,
       Genv.find_funct ge vf = Some fd ->
-      cast_arguments el tyargs vargs ->
+      cast_arguments m el tyargs vargs ->
       type_of_fundef fd = Tfunction tyargs tyres cconv ->
       classify_fun tyf = fun_case_f tyargs tyres cconv ->
-      callred (Ecall (Eval vf tyf) el ty)
+      callred (Ecall (Eval vf tyf) el ty) m
               fd vargs ty.
 
 (** Reduction contexts.  In accordance with C's nondeterministic semantics,
@@ -429,17 +429,14 @@ Inductive imm_safe: kind -> expr -> mem -> Prop :=
       context RV to C ->
       imm_safe to (C e) m
   | imm_safe_callred: forall to C e m fd args ty,
-      callred e fd args ty ->
+      callred e m fd args ty ->
       context RV to C ->
       imm_safe to (C e) m.
 
-(* An expression is not stuck if none of the potential redexes contained within
-   is immediately stuck. *)
-(*
 Definition not_stuck (e: expr) (m: mem) : Prop :=
   forall k C e' ,
-  context k RV C -> e = C e' -> not_imm_stuck k e' m.
-*)
+  context k RV C -> e = C e' -> imm_safe k e' m.
+
 End EXPR.
 
 (** ** Transition semantics. *)
@@ -597,7 +594,7 @@ Inductive estep: state -> trace -> state -> Prop :=
           t (ExprState f (C a') k e m')
 
   | step_call: forall C f a k e m fd vargs ty,
-      callred a fd vargs ty ->
+      callred a m fd vargs ty ->
       context RV RV C ->
       estep (ExprState f (C a) k e m)
          E0 (Callstate fd vargs (Kcall f e C ty k) m)
@@ -709,7 +706,7 @@ Inductive sstep: state -> trace -> state -> Prop :=
       sstep (State f (Sreturn (Some x)) k e m)
          E0 (ExprState f x (Kreturn k) e  m)
   | step_return_2:  forall f v1 ty k e m v2 m',
-      sem_cast v1 ty f.(fn_return) = Some v2 ->
+      sem_cast v1 ty f.(fn_return) m = Some v2 ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
       sstep (ExprState f (Eval v1 ty) (Kreturn k) e m)
          E0 (Returnstate v2 (call_cont k) m')
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index e25e21c9..4f067fad 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -255,7 +255,7 @@ Lemma make_cast_correct:
   forall e le m a b v ty1 ty2 v',
   make_cast ty1 ty2 a = OK b ->
   eval_expr ge e le m a v ->
-  sem_cast v ty1 ty2 = Some v' ->
+  sem_cast v ty1 ty2 m = Some v' ->
   eval_expr ge e le m b v'.
 Proof.
   intros. unfold make_cast, sem_cast in *;
@@ -302,6 +302,12 @@ Proof.
   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 *)
@@ -394,6 +400,16 @@ Qed.
 
 Definition binary_constructor_correct
     (make: expr -> type -> expr -> type -> res expr)
+    (sem: val -> type -> val -> type -> mem -> option val): Prop :=
+  forall a tya b tyb c va vb v e le m,
+  sem va tya vb tyb m = Some v ->
+  make a tya b tyb = OK c ->
+  eval_expr ge e le m a va ->
+  eval_expr ge e le m b vb ->
+  eval_expr ge e le m c v.
+
+Definition shift_constructor_correct
+    (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> type -> val -> type -> option val): Prop :=
   forall a tya b tyb c va vb v e le m,
   sem va tya vb tyb = Some v ->
@@ -433,8 +449,8 @@ Proof.
   set (cls := classify_binarith tya tyb) in *.
   set (ty := binarith_type cls) in *.
   monadInv MAKE.
-  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
-  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
   exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
   exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
   destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
@@ -456,8 +472,8 @@ Proof.
   set (cls := classify_binarith tya tyb) in *.
   set (ty := binarith_type cls) in *.
   monadInv MAKE.
-  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
-  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
   exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
   exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
   destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
@@ -578,7 +594,7 @@ Proof.
   apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.
 Qed.
 
-Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl.
+Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl.
 Proof.
   red; unfold make_shl, sem_shl, sem_shift;
   intros until m; intros SEM MAKE EV1 EV2;
@@ -597,7 +613,7 @@ Proof.
   unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto.
 Qed.
 
-Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
+Lemma make_shr_correct: shift_constructor_correct make_shr sem_shr.
 Proof.
   red; unfold make_shr, sem_shr, sem_shift;
   intros until m; intros SEM MAKE EV1 EV2;
@@ -619,15 +635,9 @@ Proof.
   unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
 Qed.
 
-Lemma make_cmp_correct:
-  forall cmp a tya b tyb c va vb v e le m,
-  sem_cmp cmp va tya vb tyb m = Some v ->
-  make_cmp cmp a tya b tyb = OK c ->
-  eval_expr ge e le m a va ->
-  eval_expr ge e le m b vb ->
-  eval_expr ge e le m c v.
+Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp).
 Proof.
-  unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
+  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.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b3cbacca..2650e0a8 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -130,7 +130,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ebinop op r1 r2 ty) v
   | esr_cast: forall ty r1 v1 v,
       eval_simple_rvalue r1 v1 ->
-      sem_cast v1 (typeof r1) ty = Some v ->
+      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)))
@@ -141,7 +141,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
       eval_simple_list Enil Tnil nil
   | esrl_cons: forall r rl ty tyl v vl v',
-      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v ->
+      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v ->
       eval_simple_list rl tyl vl ->
       eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl).
 
@@ -283,7 +283,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       eval_simple_rvalue e m r v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m = Some v' ->
       assign_loc ge (typeof l) m b ofs v' t m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
@@ -295,7 +295,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       deref_loc ge (typeof l) m b ofs t1 v1 ->
       eval_simple_rvalue e m r v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m = Some v4 ->
       assign_loc ge (typeof l) m b ofs v4 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -310,7 +310,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with
       | None => True
       | Some v3 =>
-          match sem_cast v3 tyres (typeof l) with
+          match sem_cast v3 tyres (typeof l) m with
           | None => True
           | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
           end
@@ -323,8 +323,8 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t1 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m = Some v3 ->
       assign_loc ge ty m b ofs v3 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -335,10 +335,10 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t v1 ->
-      match sem_incrdecr ge id v1 ty with
+      match sem_incrdecr ge id v1 ty m with
       | None => True
       | Some v2 =>
-          match sem_cast v2 (incrdecr_type ty) ty with
+          match sem_cast v2 (incrdecr_type ty) ty m with
           | None => True
           | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
           end
@@ -357,7 +357,7 @@ Inductive estep: state -> trace -> state -> Prop :=
   | step_paren: forall f C r tycast ty k e m v1 v,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r v1 ->
-      sem_cast v1 (typeof r) tycast = Some v ->
+      sem_cast v1 (typeof r) tycast m = Some v ->
       estep (ExprState f (C (Eparen r tycast ty)) k e m)
          E0 (ExprState f (C (Eval v ty)) k e m)
 
@@ -472,7 +472,7 @@ Proof.
 Qed.
 
 Lemma callred_kind:
-  forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV.
+  forall a m fd args ty, callred ge a m fd args ty -> expr_kind a = RV.
 Proof.
   induction 1; auto.
 Qed.
@@ -540,7 +540,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
       exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
   | Ecast (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+      exists v, sem_cast v1 ty1 ty m = Some v
   | Eseqand (Eval v1 ty1) r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
   | Eseqor (Eval v1 ty1) r2 ty =>
@@ -549,7 +549,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists b, bool_val v1 ty1 m = Some b
   | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
       exists v, exists m', exists t,
-      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m'
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
       exists t, exists v1,
       ty = ty1
@@ -561,18 +561,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) ty2 ty =>
-      exists v, sem_cast v1 ty1 ty2 = Some v
+      exists v, sem_cast v1 ty1 ty2 m = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
          classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
-      /\ cast_arguments rargs tyargs vl
+      /\ cast_arguments m rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs, exists t, exists vres, exists m',
-         cast_arguments rargs tyargs vargs
+         cast_arguments m rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
   | _ => True
   end.
@@ -608,7 +608,7 @@ Qed.
 
 Lemma callred_invert:
   forall r fd args ty m,
-  callred ge r fd args ty ->
+  callred ge r m fd args ty ->
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
@@ -893,7 +893,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop :=
 Lemma eval_simple_list_implies:
   forall rl tyl vl,
   eval_simple_list e m rl tyl vl ->
-  exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
+  exists vl', cast_arguments m (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
 Proof.
   induction 1.
   exists (@nil val); split. constructor. constructor.
@@ -905,7 +905,7 @@ Lemma can_eval_simple_list:
   forall rl vl,
   eval_simple_list' rl vl ->
   forall tyl vl',
-  cast_arguments (rval_list vl rl) tyl vl' ->
+  cast_arguments m (rval_list vl rl) tyl vl' ->
   eval_simple_list e m rl tyl vl'.
 Proof.
   induction 1; simpl; intros.
@@ -1234,9 +1234,9 @@ Proof.
   left; apply step_rred; auto. econstructor; eauto.
   set (op := match id with Incr => Oadd | Decr => Osub end).
   assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m =
-              sem_incrdecr ge id v1 (typeof l)).
+              sem_incrdecr ge id v1 (typeof l) m).
     destruct id; auto.
-  destruct (sem_incrdecr ge id v1 (typeof l)) as [v2|].
+  destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|].
   eapply star_left.
   left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   econstructor; eauto.
@@ -1329,7 +1329,7 @@ Proof.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
   destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
-  destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?.
+  destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
   destruct H2 as [t2 [m' D]].
   econstructor; econstructor; eapply step_assignop; eauto.
@@ -1343,8 +1343,8 @@ Proof.
   exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto.
   intros [b1 [ofs [E1 S1]]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
-  destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?.
-  destruct (sem_cast v2 (incrdecr_type ty) ty) as [v3|] eqn:?.
+  destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?.
+  destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')).
   destruct H0 as [t2 [m' D]].
   econstructor; econstructor; eapply step_postincr; eauto.
@@ -1498,7 +1498,7 @@ Proof.
   econstructor; econstructor; eauto.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1511,7 +1511,7 @@ Proof.
   (* assignop stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1526,8 +1526,8 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1539,8 +1539,8 @@ Proof.
   rewrite Heqo; auto.
   (* postincr stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1641,11 +1641,11 @@ Definition outcome_switch (out: outcome) : outcome :=
   | o => o
   end.
 
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Prop :=
   match out, t with
   | Out_normal, Tvoid => v = Vundef
   | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v
+  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty m = Some v
   | _, _ => False
   end.
 
@@ -1697,7 +1697,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some true ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v ->
+      sem_cast v2 (typeof a2) type_bool m'' = Some v ->
       eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
@@ -1707,7 +1707,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some false ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v ->
+      sem_cast v2 (typeof a2) type_bool m'' = Some v ->
       eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
@@ -1717,7 +1717,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some b ->
       eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' ->
-      sem_cast v' (typeof (if b then a2 else a3)) ty = Some v ->
+      sem_cast v' (typeof (if b then a2 else a3)) ty m'' = Some v ->
       eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty)
   | eval_sizeof: forall e m ty' ty,
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
@@ -1727,7 +1727,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
       eval_simple_lvalue ge e m2 l' b ofs ->
       eval_simple_rvalue ge e m2 r' v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m2 = Some v' ->
       assign_loc ge (typeof l) m2 b ofs v' t3 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty)
@@ -1738,7 +1738,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       deref_loc ge (typeof l) m2 b ofs t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m2 = Some v4 ->
       assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty)
@@ -1746,8 +1746,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' ->
       eval_simple_lvalue ge e m1 l' b ofs ->
       deref_loc ge ty m1 b ofs t2 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m1 = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 ->
       assign_loc ge ty m1 b ofs v3 t3 m2 ->
       ty = typeof l ->
       eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty)
@@ -1901,7 +1901,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       exec_stmt e m2 f.(fn_body) t m3 out ->
-      outcome_result_value out f.(fn_return) vres ->
+      outcome_result_value out f.(fn_return) vres m3 ->
       Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index aa320f20..f59fb396 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1370,7 +1370,7 @@ Qed.
 Hint Resolve pres_cast_int_int: ty.
 
 Lemma pres_sem_cast:
-  forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2.
+  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).
@@ -1385,7 +1385,10 @@ Proof.
 - 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.
 Qed.
 
 Lemma pres_sem_binarith:
@@ -1394,7 +1397,7 @@ Lemma pres_sem_binarith:
     (sem_long: signedness -> int64 -> int64 -> option val)
     (sem_float: float -> float -> option val)
     (sem_single: float32 -> float32 -> option val)
-    v1 ty1 v2 ty2 v ty msg,
+    v1 ty1 v2 ty2 m v ty msg,
     (forall sg n1 n2,
      match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
     (forall sg n1 n2,
@@ -1403,14 +1406,14 @@ Lemma pres_sem_binarith:
      match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) ->
     (forall n1 n2,
      match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) ->
-    sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 = Some v ->
+    sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 m = Some v ->
     binarith_type ty1 ty2 msg = OK ty ->
     wt_val v ty.
 Proof with (try discriminate).
   intros. unfold sem_binarith, binarith_type in *.
   set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *.
-  destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1...
-  destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2...
+  destruct (sem_cast v1 ty1 ty' m) as [v1'|] eqn:CAST1...
+  destruct (sem_cast v2 ty2 ty' m) as [v2'|] eqn:CAST2...
   DestructCases.
 - specialize (H s i i0). rewrite H3 in H.
   destruct v; auto with ty; contradiction.
@@ -1426,12 +1429,12 @@ Lemma pres_sem_binarith_int:
   forall
     (sem_int: signedness -> int -> int -> option val)
     (sem_long: signedness -> int64 -> int64 -> option val)
-    v1 ty1 v2 ty2 v ty msg,
+    v1 ty1 v2 ty2 m v ty msg,
     (forall sg n1 n2,
      match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
     (forall sg n1 n2,
      match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) ->
-    sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 = Some v ->
+    sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 m = Some v ->
     binarith_int_type ty1 ty2 msg = OK ty ->
     wt_val v ty.
 Proof.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index b1a39c64..7228cd75 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -47,7 +47,7 @@ If [a] is a l-value, the returned value denotes:
 *)
 
 Definition do_cast (v: val) (t1 t2: type) : res val :=
-  match sem_cast v t1 t2 with
+  match sem_cast v t1 t2 Mem.empty with
   | Some v' => OK v'
   | None => Error(msg "undefined cast")
   end.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 9c662f5e..e6fcad8c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -120,7 +120,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ebinop op r1 r2 ty) v
   | esr_cast: forall ty r1 v1 v,
       eval_simple_rvalue r1 v1 ->
-      sem_cast v1 (typeof r1) ty = Some v ->
+      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)))
@@ -129,7 +129,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | 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 ->
-      sem_cast v2 (typeof r2) type_bool = Some v3 ->
+      sem_cast v2 (typeof r2) type_bool m = Some v3 ->
       eval_simple_rvalue (Eseqand r1 r2 ty) v3
   | esr_seqand_false: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
@@ -137,7 +137,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_seqor_false: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
       eval_simple_rvalue r2 v2 ->
-      sem_cast v2 (typeof r2) type_bool = Some v3 ->
+      sem_cast v2 (typeof r2) type_bool m = Some v3 ->
       eval_simple_rvalue (Eseqor r1 r2 ty) v3
   | esr_seqor_true: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
@@ -145,13 +145,13 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_condition: forall r1 r2 r3 ty v v1 b v',
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b ->
       eval_simple_rvalue (if b then r2 else r3) v' ->
-      sem_cast v' (typeof (if b then r2 else r3)) ty = Some v ->
+      sem_cast v' (typeof (if b then r2 else r3)) ty m = Some v ->
       eval_simple_rvalue (Econdition r1 r2 r3 ty) v
   | esr_comma: forall r1 r2 ty v1 v,
       eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v ->
       eval_simple_rvalue (Ecomma r1 r2 ty) v
   | esr_paren: forall r tycast ty v v',
-      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' ->
+      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast m = Some v' ->
       eval_simple_rvalue (Eparen r tycast ty) v'.
 
 End SIMPLE_EXPRS.
@@ -355,14 +355,16 @@ Proof.
 Qed.
 
 Lemma sem_cast_match:
-  forall v1 ty1 ty2 v2 v1' v2',
-  sem_cast v1 ty1 ty2 = Some v2 ->
+  forall v1 ty1 ty2 m v2 v1' v2',
+  sem_cast v1 ty1 ty2 m = Some v2 ->
   do_cast v1' ty1 ty2 = OK v2' ->
   Val.inject inj v1' v1 ->
   Val.inject inj v2' v2.
 Proof.
-  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0.
-  exploit sem_cast_inject. eexact E. eauto.
+  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2 Mem.empty) as [v2''|] eqn:E; inv H0.
+  exploit (sem_cast_inj inj Mem.empty m).
+  intros. rewrite mem_empty_not_weak_valid_pointer in H2. discriminate.
+  eexact E. eauto.
   intros [v' [A B]]. congruence.
 Qed.
 
@@ -605,7 +607,7 @@ Theorem transl_init_single_steps:
   forall ty a data f m v1 ty1 m' v chunk b ofs m'',
   transl_init_single ge ty a = OK data ->
   star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
-  sem_cast v1 ty1 ty = Some v ->
+  sem_cast v1 ty1 ty m' = Some v ->
   access_mode ty = By_value chunk ->
   Mem.store chunk m' b ofs v = Some m'' ->
   Genv.store_init_data ge m b ofs data = Some m''.
@@ -760,7 +762,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
   | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
       star step ge (ExprState dummy_function a Kstop empty_env m)
                 E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
-      sem_cast v1 ty1 ty = Some v ->
+      sem_cast v1 ty1 ty m' = Some v ->
       access_mode ty = By_value chunk ->
       Mem.store chunk m' b ofs v = Some m'' ->
       exec_init m b ofs ty (Init_single a) m''
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index a5a6ad66..a3af8114 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -114,7 +114,7 @@ Fixpoint eval_simpl_expr (a: expr) : option val :=
   | Ecast b ty =>
       match eval_simpl_expr b with
       | None => None
-      | Some v => sem_cast v (typeof b) ty
+      | Some v => sem_cast v (typeof b) ty Mem.empty
       end
   | _ => None
   end.
@@ -327,10 +327,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       let ty2 := Csyntax.typeof r2 in
       match dst with
       | For_val | For_set _ =>
-          do t <- gensym ty2;
+          do t <- gensym ty1;
           ret (finish dst
-                 (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil)
-                 (Ecast (Etempvar t ty2) ty1))
+                 (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil)
+                 (Etempvar t ty1))
       | For_effects =>
           ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil,
                dummy_expr)
@@ -342,12 +342,12 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl3, a3) <- transl_valof ty1 a1;
       match dst with
       | For_val | For_set _ =>
-          do t <- gensym tyres;
+          do t <- gensym ty1;
           ret (finish dst
                  (sl1 ++ sl2 ++ sl3 ++
-                  Sset t (Ebinop op a3 a2 tyres) ::
-                  make_assign a1 (Etempvar t tyres) :: nil)
-                 (Ecast (Etempvar t tyres) ty1))
+                  Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
+                  make_assign a1 (Etempvar t ty1) :: nil)
+                 (Etempvar t ty1))
       | For_effects =>
           ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil,
                dummy_expr)
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 0c7c9ce7..8baa7d46 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -752,12 +752,27 @@ Qed.
 
 (** Semantics of smart constructors *)
 
+Remark sem_cast_deterministic:
+  forall v ty ty' m1 v1 m2 v2,
+  sem_cast v ty ty' m1 = Some v1 ->
+  sem_cast v ty ty' m2 = Some v2 ->
+  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.
+  auto.
+Qed.
+
 Lemma eval_simpl_expr_sound:
   forall e le m a v, eval_expr tge e le m a v ->
   match eval_simpl_expr a with Some v' => v' = v | None => True end.
 Proof.
   induction 1; simpl; auto.
-  destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto.
+  destruct (eval_simpl_expr a); auto. subst.
+  destruct (sem_cast v1 (typeof a) ty Mem.empty) as [v'|] eqn:C; auto.
+  eapply sem_cast_deterministic; eauto.
   inv H; simpl; auto.
 Qed.
 
@@ -811,7 +826,7 @@ Lemma step_make_assign:
   Csem.assign_loc ge ty m b ofs v t m' ->
   eval_lvalue tge e le m a1 b ofs ->
   eval_expr tge e le m a2 v2 ->
-  sem_cast v2 (typeof a2) ty = Some v ->
+  sem_cast v2 (typeof a2) ty m = Some v ->
   typeof a1 = ty ->
   step1 tge (State f (make_assign a1 a2) k e le m)
           t (State f Sskip k e le m').
@@ -1649,18 +1664,19 @@ Proof.
   (* for value *)
   exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto.
+    eapply tr_expr_invariant with (le' := PTree.set t0 v' le). eauto.
     intros. apply PTree.gso. intuition congruence.
   intros [SL1 [TY1 EV1]].
   subst; simpl Kseqlist.
   econstructor; split.
   left. eapply plus_left. constructor.
-  eapply star_left. constructor. eauto.
+  eapply star_left. constructor. econstructor. eauto. rewrite <- TY2; eauto. 
   eapply star_left. constructor.
   apply star_one. eapply step_make_assign; eauto.
-  constructor. apply PTree.gss. reflexivity. reflexivity. traceEq.
+  constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. 
+  reflexivity. reflexivity. traceEq.
   econstructor. auto. apply S.
-  apply tr_val_gen. auto. intros. econstructor; eauto. constructor.
+  apply tr_val_gen. auto. intros. constructor.
   rewrite H4; auto. apply PTree.gss.
   intros. apply PTree.gso. intuition congruence.
   auto. auto.
@@ -1692,7 +1708,7 @@ Proof.
   exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto.
   intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto.
+    eapply tr_expr_invariant with (le := le) (le' := PTree.set t v4 le'). eauto.
     intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence.
   intros [? [? EV1'']].
   subst; simpl Kseqlist.
@@ -1700,13 +1716,14 @@ Proof.
   left. rewrite app_ass. rewrite Kseqlist_app.
   eapply star_plus_trans. eexact EXEC.
   simpl. eapply plus_four. econstructor. econstructor.
-    econstructor. eexact EV3. eexact EV2.
+    econstructor. econstructor. eexact EV3. eexact EV2.
     rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto.
+    eassumption.
   econstructor. eapply step_make_assign; eauto.
-    constructor. apply PTree.gss.
+    constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto.
     reflexivity. traceEq.
   econstructor. auto. apply S.
-  apply tr_val_gen. auto. intros. econstructor; eauto. constructor.
+  apply tr_val_gen. auto. intros. constructor.
   rewrite H10; auto. apply PTree.gss.
   intros. rewrite PTree.gso. apply INV.
   red; intros; elim H10; auto.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 4077d7df..b94465a1 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -222,10 +222,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       ty2 = Csyntax.typeof e2 ->
       tr_expr le dst (Csyntax.Eassign e1 e2 ty)
                    (sl1 ++ sl2 ++
-                    Sset t a2 ::
-                    make_assign a1 (Etempvar t ty2) ::
-                    final dst (Ecast (Etempvar t ty2) ty1))
-                   (Ecast (Etempvar t ty2) ty1) tmp
+                    Sset t (Ecast a2 ty1) ::
+                    make_assign a1 (Etempvar t ty1) ::
+                    final dst (Etempvar t ty1))
+                   (Etempvar t ty1) tmp
   | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
@@ -246,10 +246,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       ty1 = Csyntax.typeof e1 ->
       tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty)
                    (sl1 ++ sl2 ++ sl3 ++
-                    Sset t (Ebinop op a3 a2 tyres) ::
-                    make_assign a1 (Etempvar t tyres) ::
-                    final dst (Ecast (Etempvar t tyres) ty1))
-                   (Ecast (Etempvar t tyres) ty1) tmp
+                    Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
+                    make_assign a1 (Etempvar t ty1) ::
+                    final dst (Etempvar t ty1))
+                   (Etempvar t ty1) tmp
   | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_rvalof ty1 a1 sl2 a2 tmp2 ->
@@ -375,8 +375,7 @@ Qed.
   between Csyntax values and Cminor expressions: in the case of
   [tr_expr], the Cminor expression must not depend on memory,
   while in the case of [tr_top] it can depend on the current memory
-  state.  This special case is extended to values occurring under
-  one or several [Csyntax.Eparen]. *)
+  state. *)
 
 Section TR_TOP.
 
@@ -389,19 +388,9 @@ Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list
   | tr_top_val_val: forall v ty a tmp,
       typeof a = ty -> eval_expr ge e le m a v ->
       tr_top For_val (Csyntax.Eval v ty) nil a tmp
-(*
-  | tr_top_val_set: forall t tyl v ty a any tmp,
-      typeof a = ty -> eval_expr ge e le m a v ->
-      tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp
-*)
   | tr_top_base: forall dst r sl a tmp,
       tr_expr le dst r sl a tmp ->
       tr_top dst r sl a tmp.
-(*
-  | tr_top_paren_test: forall tyl t r ty sl a tmp,
-      tr_top (For_set (ty :: tyl) t) r sl a tmp ->
-      tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp.
-*)
 
 End TR_TOP.
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index a47036bf..a86e3a01 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -201,97 +201,7 @@ Proof.
   xomegaContradiction.
 Qed.
 
-(** Properties of values obtained by casting to a given type. *)
-
-Inductive val_casted: val -> type -> Prop :=
-  | val_casted_int: forall sz si attr n,
-      cast_int_int sz si n = n ->
-      val_casted (Vint n) (Tint sz si attr)
-  | val_casted_float: forall attr n,
-       val_casted (Vfloat n) (Tfloat F64 attr)
-  | val_casted_single: forall attr n,
-       val_casted (Vsingle n) (Tfloat F32 attr)
-  | val_casted_long: forall si attr n,
-      val_casted (Vlong n) (Tlong si attr)
-  | 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)
-  | val_casted_ptr_int: forall b ofs si attr,
-      val_casted (Vptr b ofs) (Tint I32 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,
-      val_casted (Vptr b ofs) (Tunion id attr)
-  | val_casted_void: forall v,
-      val_casted v Tvoid.
-
-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.
-  intros. destruct sz; simpl; auto.
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
-  destruct (Int.eq i Int.zero); auto.
-Qed.
-
-Lemma cast_val_is_casted:
-  forall v ty ty' v', sem_cast v ty ty' = 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.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); 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.
-(* impossible cases *)
-  discriminate.
-  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.
-Qed.
+(** Properties of values resulting from a cast *)
 
 Lemma val_casted_load_result:
   forall v ty chunk,
@@ -316,15 +226,6 @@ Proof.
   discriminate.
 Qed.
 
-Lemma cast_val_casted:
-  forall v ty, val_casted v ty -> sem_cast v ty ty = 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.
-Qed.
-
 Lemma val_casted_inject:
   forall f v v' ty,
   Val.inject f v v' -> val_casted v ty -> val_casted v' ty.
@@ -363,7 +264,7 @@ Qed.
 Lemma make_cast_correct:
   forall e le m a v1 tto v2,
   eval_expr tge e le m a v1 ->
-  sem_cast v1 (typeof a) tto = Some v2 ->
+  sem_cast v1 (typeof a) tto m = Some v2 ->
   eval_expr tge e le m (make_cast a tto) v2.
 Proof.
   intros.
@@ -386,9 +287,9 @@ Qed.
 (** Debug annotations. *)
 
 Lemma cast_typeconv:
-  forall v ty,
+  forall v ty m,
   val_casted v ty ->
-  sem_cast v ty (typeconv ty) = Some v.
+  sem_cast v ty (typeconv ty) m = Some v.
 Proof.
   induction 1; simpl; auto.
 - destruct sz; auto.
@@ -423,7 +324,7 @@ Qed.
 Lemma step_Sset_debug:
   forall f id ty a k e le m v v',
   eval_expr tge e le m a v ->
-  sem_cast v (typeof a) ty = Some v' ->
+  sem_cast v (typeof a) ty m = Some v' ->
   plus step2 tge (State f (Sset_debug id ty a) k e le m)
               E0 (State f Sskip k e (PTree.set id v' le) m).
 Proof.