Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8

6 files changed, 214 insertions, 162 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 75f5eb3e..d830ada6 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -194,12 +194,28 @@ let builtins_generic = {
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
     "__builtin_bswap16",
       (TInt(IUShort, []), [TInt(IUShort, [])], false);
+    "__builtin_clz",
+      (TInt(IInt, []), [TInt(IUInt, [])], false);
+    "__builtin_clzl",
+      (TInt(IInt, []), [TInt(IULong, [])], false);
+    "__builtin_clzll",
+      (TInt(IInt, []), [TInt(IULongLong, [])], false);
+    "__builtin_ctz",
+      (TInt(IInt, []), [TInt(IUInt, [])], false);
+    "__builtin_ctzl",
+      (TInt(IInt, []), [TInt(IULong, [])], false);
+    "__builtin_ctzll",
+      (TInt(IInt, []), [TInt(IULongLong, [])], false);
     (* Floating-point absolute value *)
     "__builtin_fabs",
     (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    "__builtin_fabsf",
+    (TFloat(FFloat, []), [TFloat(FFloat, [])], false);
     (* Float arithmetic *)
     "__builtin_fsqrt",
     (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    "__builtin_sqrt",
+    (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     (* Block copy *)
     "__builtin_memcpy_aligned",
          (TVoid [],
@@ -1540,7 +1556,7 @@ let convertProgram p =
         let p' =
           { prog_defs = gl2;
             prog_public = public_globals gl2;
-            prog_main = intern_string "main";
+            prog_main = intern_string !Clflags.main_function_name;
             prog_types = typs;
             prog_comp_env = ce } in
         Diagnostics.check_errors ();
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 44660718..22ab2b5a 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -49,13 +49,15 @@ let process_use_section_pragma classname id =
 
 (* #pragma reserve_register *)
 
+let reserved_registers = ref ([]: Machregs.mreg list)
+
 let process_reserve_register_pragma name =
-  match Machregsaux.register_by_name name with
+  match Machregsnames.register_by_name name with
   | None ->
       C2C.error "unknown register in `reserve_register' pragma"
   | Some r ->
-      if Machregsaux.can_reserve_register r then
-        IRC.reserved_registers := r :: !IRC.reserved_registers
+      if Conventions1.is_callee_save r then
+        reserved_registers := r :: !reserved_registers
       else
         C2C.error "cannot reserve this register (not a callee-save)"
 
@@ -84,5 +86,8 @@ let process_pragma name =
   | _ ->
       false
 
+let reset () =
+  reserved_registers := []
+
 let initialize () =
   C2C.process_pragma_hook := process_pragma
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index beca056f..cfb2b584 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -270,6 +270,9 @@ let rec expr p (prec, e) =
   | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
       fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]"
         (P.to_int kind) (extern_atom txt) exprlist (false,args)
+  | Ebuiltin(EF_builtin(name, _), _, args, _) ->
+      fprintf p "%s@[<hov 1>(%a)@]"
+                (camlstring_of_coqstring name) exprlist (true, args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
   | Eparen(a1, tycast, ty) ->
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 7cdff468..c7e57a54 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -268,8 +268,13 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl2, a2) <- transl_expr For_val r2;
       ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty))
   | Csyntax.Ecast r1 ty =>
-      do (sl1, a1) <- transl_expr For_val r1;
-      ret (finish dst sl1 (Ecast a1 ty))
+      match dst with
+      | For_val | For_set _ =>
+          do (sl1, a1) <- transl_expr For_val r1;
+          ret (finish dst sl1 (Ecast a1 ty))
+      | For_effects =>
+          transl_expr For_effects r1
+      end
   | Csyntax.Eseqand r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       match dst with
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index ee1df409..9a3f32ec 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -145,18 +145,18 @@ Proof.
   assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil).
     intros. destruct H; subst dst; auto.
   apply tr_expr_exprlist; intros; simpl in *; try discriminate; auto.
-  rewrite H0; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct H1; congruence.
-  destruct (andb_prop _ _ H6). inv H1.
+- rewrite H0; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct H1; congruence.
+- destruct (andb_prop _ _ H6). inv H1.
     rewrite H0; eauto. simpl; auto.
     unfold chunk_for_volatile_type in H9.
     destruct (type_is_volatile (Csyntax.typeof e1)); simpl in H8; congruence.
-  rewrite H0; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct (andb_prop _ _ H6). rewrite H0; auto.
+- rewrite H0; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct (andb_prop _ _ H6). rewrite H0; auto.
 Qed.
 
 Lemma tr_simple_expr_nil:
@@ -234,11 +234,11 @@ Proof.
 Opaque makeif.
   intros e m.
   apply (eval_simple_rvalue_lvalue_ind ge e m); intros until tmps; intros TR; inv TR.
-(* value *)
+- (* value *)
   auto.
-  auto.
-  exists a0; auto.
-(* rvalof *)
+- auto.
+- exists a0; auto.
+- (* rvalof *)
   inv H7; try congruence.
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
@@ -248,53 +248,55 @@ Opaque makeif.
     exploit deref_loc_translated; eauto. unfold chunk_for_volatile_type; rewrite H2. tauto.
   destruct dst; auto.
   econstructor. split. simpl; eauto. auto.
-(* addrof *)
+- (* addrof *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Eaddrof' a1 ty) (Vptr b ofs)) by (apply eval_Eaddrof'; auto).
   assert (typeof (Eaddrof' a1 ty) = ty) by (apply typeof_Eaddrof').
   destruct dst; auto. simpl; econstructor; eauto.  
-(* unop *)
+- (* unop *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Eunop op a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* binop *)
+- (* binop *)
   exploit H0; eauto. intros [A [B C]].
   exploit H2; eauto. intros [D [E F]].
   subst sl1 sl2; simpl.
   assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. rewrite comp_env_preserved; congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* cast *)
+- (* cast effects *)
+  exploit H0; eauto.
+- (* cast val *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* sizeof *)
+- (* sizeof *)
   rewrite <- comp_env_preserved.
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
   exists (Esizeof ty1 ty). split. auto. split. auto. constructor.
-(* alignof *)
+- (* alignof *)
   rewrite <- comp_env_preserved.
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
   exists (Ealignof ty1 ty). split. auto. split. auto. constructor.
-(* var local *)
+- (* var local *)
   split; auto. split; auto. apply eval_Evar_local; auto.
-(* var global *)
+- (* var global *)
   split; auto. split; auto. apply eval_Evar_global; auto.
     rewrite symbols_preserved; auto.
-(* deref *)
+- (* deref *)
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split. rewrite typeof_Ederef'; auto. apply eval_Ederef'; auto. 
-(* field struct *)
+- (* field struct *)
   rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto.
-(* field union *)
+- (* field union *)
   rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto.
@@ -408,43 +410,43 @@ Ltac UNCHANGED :=
   (*generalize compat_dest_change; intro CDC.*)
   apply leftcontext_leftcontextlist_ind; intros.
 
-(* base *)
+- (* base *)
   TR. rewrite <- app_nil_end; auto. red; auto.
   intros. rewrite <- app_nil_end; auto.
-(* deref *)
+- (* deref *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* field *)
+- (* field *)
   inv H1.
   exploit H0. eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* rvalof *)
+- (* rvalof *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. red; eauto.
   intros. rewrite <- app_ass; econstructor; eauto.
   exploit typeof_context; eauto. congruence.
-(* addrof *)
+- (* addrof *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* unop *)
+- (* unop *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* binop left *)
+- (* binop left *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-(* binop right *)
+- (* binop right *)
   inv H2.
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
@@ -452,14 +454,19 @@ Ltac UNCHANGED :=
   red; auto.
   intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor; eauto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-(* cast *)
+- (* cast *)
   inv H1.
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
-  TR. subst sl1; rewrite app_ass; eauto. auto.
+  TR. eauto. auto. 
+  intros. econstructor; eauto.
++ (* generic *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. auto. 
   intros. rewrite <- app_ass. econstructor; eauto.
-(* seqand *)
+- (* seqand *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -467,15 +474,15 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-  auto. auto. auto. auto.
-  (* for set *)
+  auto. auto. auto.
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -483,9 +490,9 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* seqor *)
+- (* seqor *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -493,15 +500,15 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-  auto. auto. auto. auto.
-  (* for set *)
+  auto. auto. auto.
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -509,9 +516,9 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* condition *)
+- (* condition *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -520,7 +527,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -529,7 +536,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -538,16 +545,16 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto. auto.
-(* assign left *)
+- (* assign left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -556,9 +563,9 @@ Ltac UNCHANGED :=
   auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
   auto.
-(* assign right *)
+- (* assign right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -567,7 +574,7 @@ Ltac UNCHANGED :=
   econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -577,9 +584,9 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
-(* assignop left *)
+- (* assignop left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -587,7 +594,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   symmetry; eapply typeof_context; eauto. eauto.
   auto. auto. auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -595,9 +602,9 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
-(* assignop right *)
+- (* assignop right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -605,7 +612,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. eauto. auto. auto. auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -613,35 +620,35 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
-(* postincr *)
+- (* postincr *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   symmetry; eapply typeof_context; eauto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   eapply typeof_context; eauto.
-(* call left *)
+- (* call left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_exprlist_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. auto. apply S; auto.
   eapply tr_exprlist_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* call right *)
+- (* call right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
@@ -650,7 +657,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
@@ -660,42 +667,42 @@ Ltac UNCHANGED :=
   auto. eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto.
   auto. auto. auto. auto.
-(* builtin *)
+- (* builtin *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
   red; auto.
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   apply S; auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
   red; auto.
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   auto. apply S; auto. auto. auto.
-(* comma *)
+- (* comma *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-(* paren *)
+- (* paren *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. red; auto.
   intros. econstructor; eauto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. auto.
   intros. econstructor; eauto.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. auto.
   intros. econstructor; eauto.
-(* cons left *)
+- (* cons left *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
@@ -703,7 +710,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_exprlist_invariant; eauto.  UNCHANGED.
   auto. auto. auto.
-(* cons right *)
+- (* cons right *)
   inv H2.
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 95e3957c..98425311 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -108,7 +108,12 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le dst (Csyntax.Ebinop op e1 e2 ty)
                    (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty))
                    (Ebinop op a1 a2 ty) tmp
-  | tr_cast: forall le dst e1 ty sl1 a1 tmp,
+  | tr_cast_effects: forall le e1 ty sl1 a1 any tmp,
+      tr_expr le For_effects e1 sl1 a1 tmp ->
+      tr_expr le For_effects (Csyntax.Ecast e1 ty)
+                   sl1
+                   any tmp
+  | tr_cast_val: forall le dst e1 ty sl1 a1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp ->
       tr_expr le dst (Csyntax.Ecast e1 ty)
                    (sl1 ++ final dst (Ecast a1 ty))
@@ -767,58 +772,69 @@ Lemma transl_meets_spec:
     exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g').
 Proof.
   apply expr_exprlist_ind; simpl add_dest; intros.
-(* val *)
+- (* val *)
   simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym.
 Opaque makeif.
-- intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-- intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-- intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-- intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-(* var *)
-- monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
-(* field *)
-- monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
+- (* var *)
+  monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
+- (* field *)
+  monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* valof *)
-- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- (* valof *)
+  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
-(* deref *)
-- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- (* deref *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* addrof *)
-- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- (* addrof *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto.
-(* unop *)
-- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- (* unop *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* binop *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* binop *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
-(* cast *)
-- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
-  econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* seqand *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* cast *)
+  destruct dst.
++ (* for value *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; apply tr_expr_add_dest.
+  rewrite (app_nil_end sl).
+  apply tr_cast_val with (dst := For_val); auto.
++ (* for effects *)
+  exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; eapply tr_cast_effects; eauto.
++ (* for set *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; apply tr_expr_add_dest.
+  apply tr_cast_val with (dst := For_set sd); auto.
+- (* seqand *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
@@ -826,23 +842,23 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_set; eauto with gensym.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* seqor *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* seqor *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
@@ -850,23 +866,23 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_set; eauto with gensym.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* condition *)
-- monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
+- (* condition *)
+  monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   exploit H1; eauto with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
@@ -877,14 +893,14 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit H1; eauto. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   intros; eapply tr_condition_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for test *)
++ (* for test *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   exploit H1; eauto 10 with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
@@ -895,70 +911,70 @@ Opaque makeif.
   apply contained_cons; eauto with gensym.
   apply contained_app; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* sizeof *)
-- monadInv H. UseFinish.
+- (* sizeof *)
+  monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
-(* alignof *)
-- monadInv H. UseFinish.
+- (* alignof *)
+  monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
-(* assign *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* assign *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split.
   intros. eapply tr_assign_val with (dst := For_val); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x1 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. simpl.
   intros. eapply tr_assign_val with (dst := For_set sd); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-(* assignop *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* assignop *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
   destruct dst; monadInv EQ3; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
   intros. eapply tr_assignop_val with (dst := For_val); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
   repeat rewrite app_ass. simpl.
   intros. eapply tr_assignop_val with (dst := For_set sd); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-(* postincr *)
-- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- (* postincr *)
+  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   eauto with gensym.
-  (* for set *)
++ (* for set *)
   repeat rewrite app_ass; simpl.
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
-(* comma *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* comma *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
@@ -967,47 +983,47 @@ Opaque makeif.
   simpl. eapply incl_tran. 2: apply add_dest_incl. auto with gensym.
   destruct dst; simpl; auto with gensym.
   apply contained_app; eauto with gensym.
-(* call *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* call *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split.
   econstructor; eauto with gensym. congruence.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x1 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-(* builtin *)
-- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- (* builtin *)
+  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists tmp1; split.
   econstructor; eauto with gensym.
   auto.
-  (* for set *)
++ (* for set *)
   exists (x0 :: tmp1); split.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
-(* loc *)
-- monadInv H.
-(* paren *)
-- monadInv H0.
-(* nil *)
-- monadInv H; exists (@nil ident); split; auto with gensym. constructor.
-(* cons *)
-- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- (* loc *)
+  monadInv H.
+- (* paren *)
+  monadInv H0.
+- (* nil *)
+  monadInv H; exists (@nil ident); split; auto with gensym. constructor.
+- (* cons *)
+  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.