Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

18 files changed, 460 insertions, 249 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d389d0a..e7d8337 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -441,7 +441,13 @@ let z_of_str hex str fst =
 let convertFloat f kind =
   let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in
   match mant with
-    | Z.Z0 -> Float.zero
+    | Z.Z0 ->
+      begin match kind with
+      | FFloat ->
+	  Vsingle (Float.to_single Float.zero)
+      | FDouble | FLongDouble ->
+	  Vfloat Float.zero
+      end
     | Z.Zpos mant ->
 
       let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in
@@ -454,10 +460,10 @@ let convertFloat f kind =
       let base = P.of_int (if f.C.hex then 2 else 10) in
 
       begin match kind with
-	| FFloat ->
-	  Float.build_from_parsed32 base mant exp
-	| FDouble | FLongDouble ->
-	  Float.build_from_parsed64 base mant exp
+      | FFloat ->
+	  Vsingle (Float32.from_parsed base mant exp)
+      | FDouble | FLongDouble ->
+	  Vfloat (Float.from_parsed base mant exp)
       end
 
     | Z.Zneg _ -> assert false
@@ -482,7 +488,7 @@ let rec convertExpr env e =
   | C.EConst(C.CFloat(f, k)) ->
       if k = C.FLongDouble && not !Clflags.option_flongdouble then
         unsupported "'long double' floating-point literal";
-      Eval(Vfloat(convertFloat f k), ty)
+      Eval(convertFloat f k, ty)
   | C.EConst(C.CStr s) ->
       let ty = typeStringLiteral s in
       Evalof(Evar(name_for_string_literal env s, ty), ty)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b41902c..eea1997 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -104,7 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval :=
   match v, t with
   | Vint i, AST.Tint => Some (EVint i)
   | Vfloat f, AST.Tfloat => Some (EVfloat f)
-  | Vfloat f, AST.Tsingle => if Float.is_single_dec f then Some (EVfloatsingle f) else None
+  | Vsingle f, AST.Tsingle => Some (EVsingle f)
   | Vlong n, AST.Tlong => Some (EVlong n)
   | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
   | _, _ => None
@@ -124,7 +124,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
   match ev, t with
   | EVint i, AST.Tint => Some (Vint i)
   | EVfloat f, AST.Tfloat => Some (Vfloat f)
-  | EVfloatsingle f, AST.Tsingle => if Float.is_single_dec f then Some (Vfloat f) else None
+  | EVsingle f, AST.Tsingle => Some (Vsingle f)
   | EVlong n, AST.Tlong => Some (Vlong n)
   | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs)
   | _, _ => None
@@ -133,11 +133,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
 Lemma eventval_of_val_sound:
   forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.
 Proof.
-  intros. destruct v; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  constructor.
-  destruct (Float.is_single_dec f); inv H1. constructor; auto.
+  intros. destruct v; destruct t; simpl in H; inv H; try constructor.
   destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. 
   constructor. apply Genv.invert_find_symbol; auto.
 Qed.
@@ -146,7 +142,6 @@ Lemma eventval_of_val_complete:
   forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
 Proof.
   induction 1; simpl; auto.
-  rewrite pred_dec_true; auto.
   rewrite (Genv.find_invert_symbol _ _ H). auto. 
 Qed.
 
@@ -170,11 +165,7 @@ Qed.
 Lemma val_of_eventval_sound:
   forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.
 Proof.
-  intros. destruct ev; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  constructor.
-  destruct (Float.is_single_dec f); inv H1. constructor; auto.
+  intros. destruct ev; destruct t; simpl in H; inv H; try constructor.
   destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
   constructor. auto.
 Qed.
@@ -182,7 +173,7 @@ Qed.
 Lemma val_of_eventval_complete:
   forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
 Proof.
-  induction 1; simpl; auto. rewrite pred_dec_true; auto. rewrite H; auto.
+  induction 1; simpl; auto. rewrite H; auto.
 Qed.
 
 (** Volatile memory accesses. *)
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index f2ba240..d9fb650 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -47,7 +47,8 @@ Require Import Cop.
 
 Inductive expr : Type :=
   | Econst_int: int -> type -> expr       (**r integer literal *)
-  | Econst_float: float -> type -> expr   (**r float literal *)
+  | Econst_float: float -> type -> expr   (**r double float literal *)
+  | Econst_single: float32 -> type -> expr (**r single float literal *)
   | Econst_long: int64 -> type -> expr    (**r long integer literal *)
   | Evar: ident -> type -> expr           (**r variable *)
   | Etempvar: ident -> type -> expr       (**r temporary variable *)
@@ -69,6 +70,7 @@ Definition typeof (e: expr) : type :=
   match e with
   | Econst_int _ ty => ty
   | Econst_float _ ty => ty
+  | Econst_single _ ty => ty
   | Econst_long _ ty => ty
   | Evar _ ty => ty
   | Etempvar _ ty => ty
@@ -352,6 +354,8 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Econst_int i ty) (Vint i)
   | eval_Econst_float:   forall f ty,
       eval_expr (Econst_float f ty) (Vfloat f)
+  | eval_Econst_single:   forall f ty,
+      eval_expr (Econst_single f ty) (Vsingle f)
   | eval_Econst_long:   forall i ty,
       eval_expr (Econst_long i ty) (Vlong i)
   | eval_Etempvar:  forall id ty v,
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 8ecf498..ae6ec56 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -70,6 +70,8 @@ Definition transl_constant (cst: Csharpminor.constant): constant :=
       Ointconst n
   | Csharpminor.Ofloatconst n =>
       Ofloatconst n
+  | Csharpminor.Osingleconst n =>
+      Osingleconst n
   | Csharpminor.Olongconst n =>
       Olongconst n
   end.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index dba445d..3bf790c 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1299,8 +1299,15 @@ Proof.
   inv H; inv H0; simpl; TrivialExists.
   inv H; inv H0; simpl; TrivialExists.
   inv H; inv H0; simpl; TrivialExists.
-  inv H0; simpl in H; inv H. simpl. destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists.
-  inv H0; simpl in H; inv H. simpl. destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.to_int f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.to_intu f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_int f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_intu f0); simpl in *; inv H1. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H; inv H0; simpl; TrivialExists.
@@ -1308,10 +1315,12 @@ Proof.
   inv H; inv H0; simpl; TrivialExists.
   inv H; inv H0; simpl; TrivialExists.
   inv H; inv H0; simpl; TrivialExists.
-  inv H0; simpl in H; inv H. simpl. destruct (Float.longoffloat f0); simpl in *; inv H1. TrivialExists.
-  inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.to_long f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.to_longu f0); simpl in *; inv H1. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_long f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_longu f0); simpl in *; inv H1. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
 Qed.
@@ -1361,6 +1370,10 @@ Proof.
   inv H; inv H0; inv H1; TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int64.eq i0 Int64.zero
       || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists.
@@ -1392,6 +1405,8 @@ Proof.
   simpl; auto.
 (* cmpf *)
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
+(* cmpfs *)
+  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
 (* cmpl *)
   unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H.
   econstructor; split. simpl; eauto. apply val_inject_val_of_bool.
@@ -1470,6 +1485,7 @@ Proof.
   destruct cst; simpl; intros; inv H. 
   exists (Vint i); auto.
   exists (Vfloat f0); auto.
+  exists (Vsingle f0); auto.
   exists (Vlong i); auto.
 Qed.
 
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 83fe772..ff43cbd 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -74,17 +74,25 @@ Inductive incr_or_decr : Type := Incr | Decr.
 Inductive classify_cast_cases : Type :=
   | cast_case_neutral                   (**r int|pointer -> int32|pointer *)
   | cast_case_i2i (sz2:intsize) (si2:signedness)   (**r int -> int *)
-  | cast_case_f2f (sz2:floatsize)                  (**r float -> float *)
-  | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *)
-  | cast_case_f2i (sz2:intsize) (si2:signedness)   (**r float -> int *)
+  | cast_case_f2f                                  (**r double -> double *)
+  | cast_case_s2s                                  (**r single -> single *)
+  | cast_case_f2s                                  (**r double -> single *)
+  | cast_case_s2f                                  (**r single -> double *)
+  | cast_case_i2f (si1: signedness)                (**r int -> double *)
+  | cast_case_i2s (si1: signedness)                (**r int -> single *)
+  | cast_case_f2i (sz2:intsize) (si2:signedness)   (**r double -> int *)
+  | cast_case_s2i (sz2:intsize) (si2:signedness)   (**r single -> int *)
   | cast_case_l2l                       (**r long -> long *)
   | cast_case_i2l (si1: signedness)     (**r int -> long *)
   | cast_case_l2i (sz2: intsize) (si2: signedness) (**r long -> int *)
-  | cast_case_l2f (si1: signedness) (sz2: floatsize) (**r long -> float *)
-  | cast_case_f2l (si2: signedness)     (**r float -> long *)
-  | cast_case_f2bool                    (**r float -> bool *)
-  | cast_case_l2bool                    (**r long -> bool *)
-  | cast_case_p2bool                    (**r pointer -> bool *)
+  | cast_case_l2f (si1: signedness)                (**r long -> double *)
+  | cast_case_l2s (si1: signedness)                (**r long -> single *)
+  | cast_case_f2l (si2:signedness)                 (**r double -> long *)
+  | cast_case_s2l (si2:signedness)                 (**r single -> long *)
+  | cast_case_f2bool                               (**r double -> bool *)
+  | cast_case_s2bool                               (**r single -> bool *)
+  | cast_case_l2bool                               (**r long -> bool *)
+  | cast_case_p2bool                               (**r pointer -> bool *)
   | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *)
   | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *)
   | cast_case_void                                 (**r any -> void *)
@@ -93,19 +101,27 @@ Inductive classify_cast_cases : Type :=
 Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   match tto, tfrom with
   | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
-  | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool
+  | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool
+  | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool
   | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
   | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
-  | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2
-  | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2
-  | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2
+  | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2
+  | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2
+  | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f
+  | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s
+  | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
+  | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
+  | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
+  | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
   | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
   | Tlong _ _, Tlong _ _ => cast_case_l2l
   | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
   | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
   | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
-  | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2
-  | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2
+  | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2
+  | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2
+  | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1
+  | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1
   | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
   | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
   | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
@@ -128,24 +144,28 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
   end.
 
-Definition cast_int_float (si: signedness) (sz: floatsize) (i: int) : float :=
-  match si, sz with
-  | Signed, F64 => Float.floatofint i
-  | Unsigned, F64 => Float.floatofintu i
-  | Signed, F32 => Float.singleofint i
-  | Unsigned, F32 => Float.singleofintu i
+Definition cast_int_float (si: signedness) (i: int) : float :=
+  match si with
+  | Signed => Float.of_int i
+  | Unsigned => Float.of_intu i
   end.
 
 Definition cast_float_int (si : signedness) (f: float) : option int :=
   match si with
-  | Signed => Float.intoffloat f
-  | Unsigned => Float.intuoffloat f
+  | Signed => Float.to_int f
+  | Unsigned => Float.to_intu f
   end.
 
-Definition cast_float_float (sz: floatsize) (f: float) : float :=
-  match sz with
-  | F32 => Float.singleoffloat f
-  | F64 => f
+Definition cast_int_single (si: signedness) (i: int) : float32 :=
+  match si with
+  | Signed => Float32.of_int i
+  | Unsigned => Float32.of_intu i
+  end.
+
+Definition cast_single_int (si : signedness) (f: float32) : option int :=
+  match si with
+  | Signed => Float32.to_int f
+  | Unsigned => Float32.to_intu f
   end.
 
 Definition cast_int_long (si: signedness) (i: int) : int64 :=
@@ -154,18 +174,28 @@ Definition cast_int_long (si: signedness) (i: int) : int64 :=
   | Unsigned => Int64.repr (Int.unsigned i)
   end.
 
-Definition cast_long_float (si: signedness) (sz: floatsize) (i: int64) : float :=
-  match si, sz with
-  | Signed, F64 => Float.floatoflong i
-  | Unsigned, F64 => Float.floatoflongu i
-  | Signed, F32 => Float.singleoflong i
-  | Unsigned, F32 => Float.singleoflongu i
+Definition cast_long_float (si: signedness) (i: int64) : float :=
+  match si with
+  | Signed => Float.of_long i
+  | Unsigned => Float.of_longu i
+  end.
+
+Definition cast_long_single (si: signedness) (i: int64) : float32 :=
+  match si with
+  | Signed => Float32.of_long i
+  | Unsigned => Float32.of_longu i
   end.
 
 Definition cast_float_long (si : signedness) (f: float) : option int64 :=
   match si with
-  | Signed => Float.longoffloat f
-  | Unsigned => Float.longuoffloat f
+  | Signed => Float.to_long f
+  | Unsigned => Float.to_longu f
+  end.
+
+Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
+  match si with
+  | Signed => Float32.to_long f
+  | Unsigned => Float32.to_longu f
   end.
 
 Definition sem_cast (v: val) (t1 t2: type) : option val :=
@@ -180,14 +210,34 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
       | Vint i => Some (Vint (cast_int_int sz2 si2 i))
       | _ => None
       end
-  | cast_case_f2f sz2 =>
+  | cast_case_f2f =>
+      match v with
+      | Vfloat f => Some (Vfloat f)
+      | _ => None
+      end
+  | cast_case_s2s =>
+      match v with
+      | Vsingle f => Some (Vsingle f)
+      | _ => None
+      end
+  | cast_case_s2f =>
       match v with
-      | Vfloat f => Some (Vfloat (cast_float_float sz2 f))
+      | Vsingle f => Some (Vfloat (Float.of_single f))
       | _ => None
       end
-  | cast_case_i2f si1 sz2 =>
+  | cast_case_f2s =>
       match v with
-      | Vint i => Some (Vfloat (cast_int_float si1 sz2 i))
+      | Vfloat f => Some (Vsingle (Float.to_single f))
+      | _ => None
+      end
+  | cast_case_i2f si1 =>
+      match v with
+      | Vint i => Some (Vfloat (cast_int_float si1 i))
+      | _ => None
+      end
+  | cast_case_i2s si1 =>
+      match v with
+      | Vint i => Some (Vsingle (cast_int_single si1 i))
       | _ => None
       end
   | cast_case_f2i sz2 si2 =>
@@ -199,12 +249,27 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
           end
       | _ => None
       end
+  | cast_case_s2i sz2 si2 =>
+      match v with
+      | Vsingle f =>
+          match cast_single_int si2 f with
+          | Some i => Some (Vint (cast_int_int sz2 si2 i))
+          | None => None
+          end
+      | _ => None
+      end
   | cast_case_f2bool =>
       match v with
       | Vfloat f =>
           Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one))
       | _ => None
       end
+  | cast_case_s2bool =>
+      match v with
+      | Vsingle f =>
+          Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one))
+      | _ => None
+      end
   | cast_case_p2bool =>
       match v with
       | Vint i => Some (Vint (cast_int_int IBool Signed i))
@@ -232,9 +297,14 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
           Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
       | _ => None
       end
-  | cast_case_l2f si1 sz2 =>
+  | cast_case_l2f si1 =>
+      match v with
+      | Vlong i => Some (Vfloat (cast_long_float si1 i))
+      | _ => None
+      end
+  | cast_case_l2s si1 =>
       match v with
-      | Vlong i => Some (Vfloat (cast_long_float si1 sz2 i))
+      | Vlong i => Some (Vsingle (cast_long_single si1 i))
       | _ => None
       end
   | cast_case_f2l si2 =>
@@ -246,6 +316,15 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
           end
       | _ => None
       end
+  | cast_case_s2l si2 =>
+      match v with
+      | Vsingle f =>
+          match cast_single_long si2 f with
+          | Some i => Some (Vlong i)
+          | None => None
+          end
+      | _ => None
+      end
   | cast_case_struct id1 fld1 id2 fld2 =>
       match v with
       | Vptr b ofs =>
@@ -271,7 +350,8 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
 
 Inductive classify_bool_cases : Type :=
   | bool_case_i                           (**r integer *)
-  | bool_case_f                           (**r float *)
+  | bool_case_f                           (**r double float *)
+  | bool_case_s                           (**r single float *)
   | bool_case_p                           (**r pointer *)
   | bool_case_l                           (**r long *)
   | bool_default.
@@ -280,7 +360,8 @@ Definition classify_bool (ty: type) : classify_bool_cases :=
   match typeconv ty with
   | Tint _ _ _ => bool_case_i
   | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p
-  | Tfloat _ _ => bool_case_f
+  | Tfloat F64 _ => bool_case_f
+  | Tfloat F32 _ => bool_case_s
   | Tlong _ _ => bool_case_l
   | _ => bool_default
   end.
@@ -302,6 +383,11 @@ Definition bool_val (v: val) (t: type) : option bool :=
       | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero))
       | _ => None
       end
+  | bool_case_s =>
+      match v with
+      | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero))
+      | _ => None
+      end
   | bool_case_p =>
       match v with
       | Vint n => Some (negb (Int.eq n Int.zero))
@@ -333,6 +419,11 @@ Definition sem_notbool (v: val) (ty: type) : option val :=
       | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
       | _ => None
       end
+  | bool_case_s =>
+      match v with
+      | Vsingle f => Some (Val.of_bool (Float32.cmp Ceq f Float32.zero))
+      | _ => None
+      end
   | bool_case_p =>
       match v with
       | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
@@ -351,7 +442,8 @@ Definition sem_notbool (v: val) (ty: type) : option val :=
 
 Inductive classify_neg_cases : Type :=
   | neg_case_i(s: signedness)              (**r int *)
-  | neg_case_f(sz: floatsize)              (**r float *)
+  | neg_case_f                             (**r double float *)
+  | neg_case_s                             (**r single float *)
   | neg_case_l(s: signedness)              (**r long *)
   | neg_default.
 
@@ -359,7 +451,8 @@ Definition classify_neg (ty: type) : classify_neg_cases :=
   match ty with
   | Tint I32 Unsigned _ => neg_case_i Unsigned
   | Tint _ _ _ => neg_case_i Signed
-  | Tfloat sz _ => neg_case_f sz
+  | Tfloat F64 _ => neg_case_f
+  | Tfloat F32 _ => neg_case_s
   | Tlong si _ => neg_case_l si
   | _ => neg_default
   end.
@@ -371,11 +464,16 @@ Definition sem_neg (v: val) (ty: type) : option val :=
       | Vint n => Some (Vint (Int.neg n))
       | _ => None
       end
-  | neg_case_f sz =>
+  | neg_case_f =>
       match v with
       | Vfloat f => Some (Vfloat (Float.neg f))
       | _ => None
       end
+  | neg_case_s =>
+      match v with
+      | Vsingle f => Some (Vsingle (Float32.neg f))
+      | _ => None
+      end
   | neg_case_l sg =>
       match v with
       | Vlong n => Some (Vlong (Int64.neg n))
@@ -388,17 +486,22 @@ Definition sem_absfloat (v: val) (ty: type) : option val :=
   match classify_neg ty with
   | neg_case_i sg =>
       match v with
-      | Vint n => Some (Vfloat (Float.abs (cast_int_float sg F64 n)))
+      | Vint n => Some (Vfloat (Float.abs (cast_int_float sg n)))
       | _ => None
       end
-  | neg_case_f sz =>
+  | neg_case_f =>
       match v with
       | Vfloat f => Some (Vfloat (Float.abs f))
       | _ => None
       end
+  | neg_case_s =>
+      match v with
+      | Vsingle f => Some (Vfloat (Float.abs (Float.of_single f)))
+      | _ => None
+      end
   | neg_case_l sg =>
       match v with
-      | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg F64 n)))
+      | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg n)))
       | _ => None
       end
   | neg_default => None
@@ -446,7 +549,8 @@ Definition sem_notint (v: val) (ty: type): option val :=
 Inductive binarith_cases: Type :=
   | bin_case_i (s: signedness)         (**r at int type *)
   | bin_case_l (s: signedness)         (**r at long int type *)
-  | bin_case_f (sz: floatsize)         (**r at float type *)
+  | bin_case_f                         (**r at double float type *)
+  | bin_case_s                         (**r at single float type *)
   | bin_default.                       (**r error *)
 
 Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
@@ -458,31 +562,24 @@ Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
   | Tlong _ _, Tlong _ _ => bin_case_l Unsigned
   | Tlong sg _, Tint _ _ _ => bin_case_l sg
   | Tint _ _ _, Tlong sg _ => bin_case_l sg
-  | Tfloat F32 _, Tfloat F32 _ => bin_case_f F32
-  | Tfloat _ _, Tfloat _ _ => bin_case_f F64
-  | Tfloat sz _, (Tint _ _ _ | Tlong _ _) => bin_case_f sz
-  | (Tint _ _ _ | Tlong _ _), Tfloat sz _ => bin_case_f sz
+  | Tfloat F32 _, Tfloat F32 _ => bin_case_s
+  | Tfloat _ _, Tfloat _ _ => bin_case_f
+  | Tfloat F64 _, (Tint _ _ _ | Tlong _ _) => bin_case_f
+  | (Tint _ _ _ | Tlong _ _), Tfloat F64 _ => bin_case_f
+  | Tfloat F32 _, (Tint _ _ _ | Tlong _ _) => bin_case_s
+  | (Tint _ _ _ | Tlong _ _), Tfloat F32 _ => bin_case_s
   | _, _ => bin_default
   end.
 
-(** The static type of the result. *)
-
-Definition binarith_result_type (c: binarith_cases) : option type :=
-  match c with
-  | bin_case_i sg => Some(Tint I32 sg noattr)
-  | bin_case_l sg => Some(Tlong sg noattr)
-  | bin_case_f sz => Some(Tfloat sz noattr)
-  | bin_default   => None
-  end.
-
-(** The type at which the computation is done.  Both arguments are
-  converted to this type before the actual computation.  *)
+(** The static type of the result. Both arguments are converted to this type
+    before the actual computation. *)
 
 Definition binarith_type (c: binarith_cases) : type :=
   match c with
   | bin_case_i sg => Tint I32 sg noattr
   | bin_case_l sg => Tlong sg noattr
-  | bin_case_f sz => Tfloat F64 noattr
+  | bin_case_f    => Tfloat F64 noattr
+  | bin_case_s    => Tfloat F32 noattr
   | bin_default   => Tvoid
   end.
 
@@ -490,6 +587,7 @@ Definition sem_binarith
     (sem_int: signedness -> int -> int -> option val)
     (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 :=
   let c := classify_binarith t1 t2 in
   let t := binarith_type c in
@@ -505,11 +603,16 @@ Definition sem_binarith
       | Vint n1, Vint n2 => sem_int sg n1 n2
       | _,  _ => None
       end
-  | bin_case_f sz =>
+  | bin_case_f =>
       match v1', v2' with
       | Vfloat n1, Vfloat n2 => sem_float n1 n2
       | _,  _ => None
       end
+  | bin_case_s =>
+      match v1', v2' with
+      | Vsingle n1, Vsingle n2 => sem_single n1 n2
+      | _,  _ => None
+      end
   | bin_case_l sg =>
       match v1', v2' with
       | Vlong n1, Vlong n2 => sem_long sg n1 n2
@@ -569,6 +672,7 @@ Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
         (fun sg n1 n2 => Some(Vint(Int.add n1 n2)))
         (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
   end.
 
@@ -617,6 +721,7 @@ Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
         (fun sg n1 n2 => Some(Vint(Int.sub n1 n2)))
         (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
   end.
  
@@ -627,6 +732,7 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
     (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.
 
 Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
@@ -652,6 +758,7 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
           then None else Some(Vlong(Int64.divu n1 n2))
       end)
     (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
+    (fun n1 n2 => Some(Vsingle(Float32.div n1 n2)))
     v1 t1 v2 t2.
 
 Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
@@ -677,6 +784,7 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
           then None else Some(Vlong(Int64.modu n1 n2))
       end)
     (fun n1 n2 => None)
+    (fun n1 n2 => None)
     v1 t1 v2 t2.
 
 Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
@@ -684,6 +792,7 @@ Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
     (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.
 
 Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
@@ -691,6 +800,7 @@ Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
     (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.
 
 Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
@@ -698,6 +808,7 @@ Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
     (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.
 
 (** *** Shifts *)
@@ -818,6 +929,8 @@ Definition sem_cmp (c:comparison)
             Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end)))
         (fun n1 n2 =>
             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
   end.
 
@@ -946,7 +1059,9 @@ Proof.
   inv H0; inv H; TrivialInject.
 - econstructor; eauto. 
 - destruct (cast_float_int si2 f0); inv H1; TrivialInject.
+- destruct (cast_single_int si2 f0); inv H1; TrivialInject.
 - destruct (cast_float_long si2 f0); inv H1; TrivialInject.
+- destruct (cast_single_long si2 f0); inv H1; TrivialInject.
 - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
 - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
 - econstructor; eauto.
@@ -976,18 +1091,19 @@ Definition optval_self_injects (ov: option val) : Prop :=
   end.
 
 Remark sem_binarith_inject:
-  forall sem_int sem_long sem_float v1 t1 v2 t2 v v1' v2',
-  sem_binarith sem_int sem_long sem_float v1 t1 v2 t2 = Some v ->
+  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 ->
   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)) ->
-  exists v', sem_binarith sem_int sem_long sem_float v1' t1 v2' t2 = Some v' /\ val_inject f v v'.
+  (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'.
 Proof.
   intros. 
   assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v).
   {
-    intros. subst ov; simpl in H6. destruct v0; contradiction || constructor.
+    intros. subst ov; simpl in H7. destruct v0; contradiction || constructor.
   }
   unfold sem_binarith in *.
   set (c := classify_binarith t1 t2) in *.
@@ -1093,6 +1209,7 @@ Proof.
             || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I.
   destruct (Int64.eq n2 Int64.zero); exact I.
   exact I.
+  exact I.
 - (* mod *)
   eapply sem_binarith_inject; eauto; intros.
   destruct sg.
@@ -1104,6 +1221,7 @@ Proof.
             || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I.
   destruct (Int64.eq n2 Int64.zero); exact I.
   exact I.
+  exact I.
 - (* and *)
   eapply sem_binarith_inject; eauto; intros; exact I.
 - (* or *)
@@ -1168,7 +1286,8 @@ Proof.
     match t with
     | Tint _ _ _ => bool_case_i
     | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
-    | Tfloat _ _ => bool_case_f
+    | Tfloat F64 _ => bool_case_f
+    | Tfloat F32 _ => bool_case_s
     | Tlong _ _ => bool_case_l
     | _ => bool_default
     end).
@@ -1178,7 +1297,14 @@ Proof.
   unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
   destruct (Int.eq i0 Int.zero); auto.
   destruct (Int64.eq i Int64.zero); auto.
+  destruct f; auto.
+  destruct f; auto.
+  destruct f; auto.
+  destruct f; auto.
   destruct (Float.cmp Ceq f0 Float.zero); auto.
+  destruct f; auto.
+  destruct (Float32.cmp Ceq f0 Float32.zero); auto.
+  destruct f; auto.
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
@@ -1360,8 +1486,8 @@ Qed.
 
 Lemma classify_binarith_arithmetic_conversion:
   forall t1 t2,
-  binarith_result_type (classify_binarith (proj_type t1) (proj_type t2)) =
-  Some (proj_type (usual_arithmetic_conversion t1 t2)).
+  binarith_type (classify_binarith (proj_type t1) (proj_type t2)) =
+  proj_type (usual_arithmetic_conversion t1 t2).
 Proof.
   destruct t1; destruct t2; try reflexivity.
 - destruct it; destruct it0; reflexivity.
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 4b2e915..d37fa81 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -33,7 +33,8 @@ Require Import Smallstep.
 
 Inductive constant : Type :=
   | Ointconst: int -> constant          (**r integer constant *)
-  | Ofloatconst: float -> constant      (**r floating-point constant *)
+  | Ofloatconst: float -> constant      (**r double-precision floating-point constant *)
+  | Osingleconst: float32 -> constant   (**r single-precision floating-point constant *)
   | Olongconst: int64 -> constant.      (**r long integer constant *)
 
 Definition unary_operation : Type := Cminor.unary_operation.
@@ -253,6 +254,7 @@ Definition eval_constant (cst: constant) : option val :=
   match cst with
   | Ointconst n => Some (Vint n)
   | Ofloatconst n => Some (Vfloat n)
+  | Osingleconst n => Some (Vsingle n)
   | Olongconst n => Some (Vlong n)
   end.
 
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 685fa71..cedfd8b 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -50,16 +50,25 @@ Open Local Scope error_monad_scope.
 
 Definition make_intconst (n: int) :=  Econst (Ointconst n).
 
+Definition make_longconst (f: int64) :=  Econst (Olongconst f).
+
 Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
-Definition make_longconst (f: int64) :=  Econst (Olongconst f).
+Definition make_singleconst (f: float32) :=  Econst (Osingleconst f).
 
-Definition make_floatofint (e: expr) (sg: signedness) (sz: floatsize) :=
-  match sg, sz with
-  | Signed, F64 => Eunop Ofloatofint e
-  | Unsigned, F64 => Eunop Ofloatofintu e
-  | Signed, F32 => Eunop Osingleoffloat (Eunop Ofloatofint e)
-  | Unsigned, F32 => Eunop Osingleoffloat (Eunop Ofloatofintu e)
+Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e.
+Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e.
+
+Definition make_floatofint (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Ofloatofint e
+  | Unsigned => Eunop Ofloatofintu e
+  end.
+
+Definition make_singleofint (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Osingleofint e
+  | Unsigned => Eunop Osingleofintu e
   end.
 
 Definition make_intoffloat (e: expr) (sg: signedness) :=
@@ -68,18 +77,28 @@ Definition make_intoffloat (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Ointuoffloat e
   end.
 
+Definition make_intofsingle (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Ointofsingle e
+  | Unsigned => Eunop Ointuofsingle e
+  end.
+
 Definition make_longofint (e: expr) (sg: signedness) :=
   match sg with
   | Signed => Eunop Olongofint e
   | Unsigned => Eunop Olongofintu e
   end.
 
-Definition make_floatoflong (e: expr) (sg: signedness) (sz: floatsize) :=
-  match sg, sz with
-  | Signed, F64 => Eunop Ofloatoflong e
-  | Unsigned, F64 => Eunop Ofloatoflongu e
-  | Signed, F32 => Eunop Osingleoflong e
-  | Unsigned, F32 => Eunop Osingleoflongu e
+Definition make_floatoflong (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Ofloatoflong e
+  | Unsigned => Eunop Ofloatoflongu e
+  end.
+
+Definition make_singleoflong (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Osingleoflong e
+  | Unsigned => Eunop Osingleoflongu e
   end.
 
 Definition make_longoffloat (e: expr) (sg: signedness) :=
@@ -88,11 +107,18 @@ Definition make_longoffloat (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Olonguoffloat e
   end.
 
+Definition make_longofsingle (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Olongofsingle e
+  | Unsigned => Eunop Olonguofsingle e
+  end.
+
 Definition make_cmp_ne_zero (e: expr) :=
   match e with
   | Ebinop (Ocmp c) e1 e2 => e
   | Ebinop (Ocmpu c) e1 e2 => e
   | Ebinop (Ocmpf c) e1 e2 => e
+  | Ebinop (Ocmpfs c) e1 e2 => e
   | Ebinop (Ocmpl c) e1 e2 => e
   | Ebinop (Ocmplu c) e1 e2 => e
   | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
@@ -111,25 +137,27 @@ Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
   | IBool, _ => make_cmp_ne_zero e
   end.
 
-Definition make_cast_float (e: expr) (sz: floatsize) :=
-  match sz with
-  | F32 => Eunop Osingleoffloat e
-  | F64 => e
-  end.
-
 Definition make_cast (from to: type) (e: expr) :=
   match classify_cast from to with
   | cast_case_neutral => OK e
   | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
-  | cast_case_f2f sz2 => OK (make_cast_float e sz2)
-  | cast_case_i2f si1 sz2 => OK (make_floatofint e si1 sz2)
+  | cast_case_f2f => OK e
+  | cast_case_s2s => OK e
+  | cast_case_f2s => OK (make_singleoffloat e)
+  | cast_case_s2f => OK (make_floatofsingle e)
+  | cast_case_i2f si1 => OK (make_floatofint e si1)
+  | cast_case_i2s si1 => OK (make_singleofint e si1)
   | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
+  | cast_case_s2i sz2 si2 => OK (make_cast_int (make_intofsingle e si2) sz2 si2)
   | cast_case_l2l => OK e
   | cast_case_i2l si1 => OK (make_longofint e si1)
   | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
-  | cast_case_l2f si1 sz2 => OK (make_floatoflong e si1 sz2)
+  | cast_case_l2f si1 => OK (make_floatoflong e si1)
+  | cast_case_l2s si1 => OK (make_singleoflong e si1)
   | cast_case_f2l si2 => OK (make_longoffloat e si2)
+  | cast_case_s2l si2 => OK (make_longofsingle e si2)
   | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
+  | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero))
   | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
   | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
   | cast_case_struct id1 fld1 id2 fld2 => OK e
@@ -145,6 +173,7 @@ Definition make_boolean (e: expr) (ty: type) :=
   match classify_bool ty with
   | bool_case_i => make_cmp_ne_zero e
   | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
+  | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)
   | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
   | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)
   | bool_default => e   (**r should not happen *)
@@ -156,6 +185,7 @@ Definition make_notbool (e: expr) (ty: type) :=
   match classify_bool ty with
   | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero))
   | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
+  | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero))
   | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
   | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero))
   | _ => Error (msg "Cshmgen.make_notbool")
@@ -164,16 +194,18 @@ Definition make_notbool (e: expr) (ty: type) :=
 Definition make_neg (e: expr) (ty: type) :=
   match classify_neg ty with
   | neg_case_i _ => OK (Eunop Onegint e)
-  | neg_case_f _ => OK (Eunop Onegf e)
+  | neg_case_f => OK (Eunop Onegf e)
+  | neg_case_s => OK (Eunop Onegfs e)
   | neg_case_l _ => OK (Eunop Onegl e)
   | _ => Error (msg "Cshmgen.make_neg")
   end.
 
 Definition make_absfloat (e: expr) (ty: type) :=
   match classify_neg ty with
-  | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg F64))
-  | neg_case_f _ => OK (Eunop Oabsf e)
-  | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg F64))
+  | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg))
+  | neg_case_f => OK (Eunop Oabsf e)
+  | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e))
+  | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg))
   | _ => Error (msg "Cshmgen.make_absfloat")
   end.
 
@@ -186,7 +218,7 @@ Definition make_notint (e: expr) (ty: type) :=
 
 (** Binary operators *)
 
-Definition make_binarith (iop iopu fop lop lopu: binary_operation)
+Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
                          (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   let c := classify_binarith ty1 ty2 in
   let ty := binarith_type c in
@@ -195,7 +227,8 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation)
   match c with
   | bin_case_i Signed => OK (Ebinop iop e1' e2')
   | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
-  | bin_case_f _ => OK (Ebinop fop e1' e2')
+  | bin_case_f => OK (Ebinop fop e1' e2')
+  | bin_case_s => OK (Ebinop sop e1' e2')
   | bin_case_l Signed => OK (Ebinop lop e1' e2')
   | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
   | bin_default => Error (msg "Cshmgen.make_binarith")
@@ -216,7 +249,7 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
   | add_default =>
-      make_binarith Oadd Oadd Oaddf Oaddl Oaddl e1 ty1 e2 ty2
+      make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
   end.
 
 Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -231,14 +264,14 @@ Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
-      make_binarith Osub Osub Osubf Osubl Osubl e1 ty1 e2 ty2
+      make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
   end.
 
 Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  make_binarith Omul Omul Omulf Omull Omull e1 ty1 e2 ty2.
+  make_binarith Omul Omul Omulf Omulfs Omull Omull e1 ty1 e2 ty2.
 
 Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  make_binarith Odiv Odivu Odivf Odivl Odivlu e1 ty1 e2 ty2.
+  make_binarith Odiv Odivu Odivf Odivfs Odivl Odivlu e1 ty1 e2 ty2.
 
 Definition make_binarith_int (iop iopu lop lopu: binary_operation)
                              (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -251,7 +284,7 @@ Definition make_binarith_int (iop iopu lop lopu: binary_operation)
   | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
   | bin_case_l Signed => OK (Ebinop lop e1' e2')
   | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
-  | bin_case_f _ | bin_default => Error (msg "Cshmgen.make_binarith_int")
+  | bin_case_f | bin_case_s | bin_default => Error (msg "Cshmgen.make_binarith_int")
   end.
 
 Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -294,7 +327,9 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
   | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2))
   | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2)
   | cmp_default =>
-      make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2
+      make_binarith
+        (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c)
+        e1 ty1 e2 ty2
   end.
 
 (** [make_load addr ty_res] loads a value of type [ty_res] from
@@ -374,6 +409,8 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
       OK(make_intconst n)
   | Clight.Econst_float n _ =>
       OK(make_floatconst n)
+  | Clight.Econst_single n _ =>
+      OK(make_singleconst n)
   | Clight.Econst_long n _ =>
       OK(make_longconst n)
   | Clight.Evar id ty =>
@@ -454,8 +491,9 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist)
   | a1 :: a2, Tnil =>
       (* Tolerance for calls to K&R or variadic functions *)
       do ta1 <- transl_expr a1;
+      do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1;
       do ta2 <- transl_arglist a2 Tnil;
-      OK (ta1 :: ta2)
+      OK (ta1' :: ta2)
   | _, _ =>
       Error(msg "Cshmgen.transl_arglist: arity mismatch")
   end.
@@ -470,7 +508,7 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
       typ_of_type ty1 :: typlist_of_arglist a2 ty2
   | a1 :: a2, Tnil =>
       (* Tolerance for calls to K&R or variadic functions *)
-      typ_of_type_default (typeof a1) :: typlist_of_arglist a2 Tnil
+      typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil
   end.
 
 (** * Translation of statements *)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 15c4e4c..a977e0f 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -159,6 +159,13 @@ Proof.
   intros. unfold make_floatconst. econstructor. reflexivity. 
 Qed.
 
+Lemma make_singleconst_correct:
+  forall n e le m,
+  eval_expr ge e le m (make_singleconst n) (Vsingle n).
+Proof.
+  intros. unfold make_singleconst. econstructor. reflexivity. 
+Qed.
+
 Lemma make_longconst_correct:
   forall n e le m,
   eval_expr ge e le m (make_longconst n) (Vlong n).
@@ -166,62 +173,35 @@ Proof.
   intros. unfold make_floatconst. econstructor. reflexivity. 
 Qed.
 
-Lemma make_floatofint_correct:
-  forall a n sg sz e le m,
-  eval_expr ge e le m a (Vint n) ->
-  eval_expr ge e le m (make_floatofint a sg sz) (Vfloat(cast_int_float sg sz n)).
+Lemma make_singleoffloat_correct:
+  forall a n e le m,
+  eval_expr ge e le m a (Vfloat n) ->
+  eval_expr ge e le m (make_singleoffloat a) (Vsingle (Float.to_single n)).
 Proof.
-  intros. unfold make_floatofint, cast_int_float.
-  destruct sz.
-  destruct sg. 
-  rewrite Float.singleofint_floatofint. econstructor. econstructor; eauto. simpl; reflexivity. auto.
-  rewrite Float.singleofintu_floatofintu. econstructor. econstructor; eauto. simpl; reflexivity. auto.
-  destruct sg; econstructor; eauto. 
+  intros. econstructor. eauto. auto.
 Qed.
 
-Lemma make_intoffloat_correct:
-  forall e le m a sg f i,
-  eval_expr ge e le m a (Vfloat f) ->
-  cast_float_int sg f = Some i ->
-  eval_expr ge e le m (make_intoffloat a sg) (Vint i).
+Lemma make_floatofsingle_correct:
+  forall a n e le m,
+  eval_expr ge e le m a (Vsingle n) ->
+  eval_expr ge e le m (make_floatofsingle a) (Vfloat (Float.of_single n)).
 Proof.
-  unfold cast_float_int, make_intoffloat; intros.
-  destruct sg; econstructor; eauto; simpl; rewrite H0; auto.
+  intros. econstructor. eauto. auto.
 Qed.
 
-Lemma make_longofint_correct:
+Lemma make_floatofint_correct:
   forall a n sg e le m,
   eval_expr ge e le m a (Vint n) ->
-  eval_expr ge e le m (make_longofint a sg) (Vlong(cast_int_long sg n)).
+  eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)).
 Proof.
-  intros. unfold make_longofint, cast_int_long. 
+  intros. unfold make_floatofint, cast_int_float.
   destruct sg; econstructor; eauto. 
 Qed.
 
-Lemma make_floatoflong_correct:
-  forall a n sg sz e le m,
-  eval_expr ge e le m a (Vlong n) ->
-  eval_expr ge e le m (make_floatoflong a sg sz) (Vfloat(cast_long_float sg sz n)).
-Proof.
-  intros. unfold make_floatoflong, cast_int_long. 
-  destruct sg; destruct sz; econstructor; eauto. 
-Qed.
-
-Lemma make_longoffloat_correct:
-  forall e le m a sg f i,
-  eval_expr ge e le m a (Vfloat f) ->
-  cast_float_long sg f = Some i ->
-  eval_expr ge e le m (make_longoffloat a sg) (Vlong i).
-Proof.
-  unfold cast_float_long, make_longoffloat; intros.
-  destruct sg; econstructor; eauto; simpl; rewrite H0; auto.
-Qed.
-
 Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct
-             make_floatofint_correct make_intoffloat_correct
-             make_longofint_correct
-             make_floatoflong_correct make_longoffloat_correct
-             eval_Eunop eval_Ebinop: cshm.
+             make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct
+             make_floatofint_correct: cshm.
+Hint Constructors eval_expr eval_exprlist: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
 Lemma make_cmp_ne_zero_correct:
@@ -248,6 +228,9 @@ Proof.
   inv H. econstructor; eauto. rewrite H6. decEq. decEq. 
   simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
   inv H. econstructor; eauto. rewrite H6. decEq. decEq. 
+  simpl in H6. unfold Val.cmpfs in H6.
+  destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. 
+  inv H. econstructor; eauto. rewrite H6. decEq. decEq. 
   simpl in H6. unfold Val.cmpl in H6.
   destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. 
   inv H. econstructor; eauto. rewrite H6. decEq. decEq. 
@@ -268,16 +251,7 @@ Proof.
   apply make_cmp_ne_zero_correct; auto.
 Qed.
 
-Lemma make_cast_float_correct:
-  forall e le m a n sz,
-  eval_expr ge e le m a (Vfloat n) ->
-  eval_expr ge e le m (make_cast_float a sz) (Vfloat (cast_float_float sz n)).
-Proof.
-  intros. unfold make_cast_float, cast_float_float. 
-  destruct sz. eauto with cshm. auto.
-Qed.
-
-Hint Resolve make_cast_int_correct make_cast_float_correct: cshm.
+Hint Resolve make_cast_int_correct: cshm.
 
 Lemma make_cast_correct:
   forall e le m a b v ty1 ty2 v',
@@ -288,14 +262,40 @@ Lemma make_cast_correct:
 Proof.
   intros. unfold make_cast, sem_cast in *;
   destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm.
+  (* single -> int *)
+  unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. 
   (* float -> int *)
-  destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. eauto with cshm.
+  destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2.
+  apply make_cast_int_correct. 
+  unfold cast_float_int in E. unfold make_intoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
+  (* single -> int *)
+  destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2.
+  apply make_cast_int_correct. 
+  unfold cast_single_int in E. unfold make_intofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
+  (* long -> int *)
+  unfold make_longofint, cast_int_long. destruct si1; eauto with cshm.
+  (* long -> float *)
+  unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm.
+  (* long -> single *)
+  unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm.
   (* float -> long *)
-  destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. eauto with cshm.
+  destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2.
+  unfold cast_float_long in E. unfold make_longoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
+  (* single -> long *)
+  destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2.
+  unfold cast_single_long in E. unfold make_longofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
   (* float -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
   destruct (Float.cmp Ceq f Float.zero); auto.
+  (* single -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq.
+  destruct (Float32.cmp Ceq f Float32.zero); auto.
   (* long -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp.
@@ -327,6 +327,10 @@ Proof.
   econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
   unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. 
   destruct (Float.cmp Cne f Float.zero); constructor. 
+(* single *)
+  econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
+  unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. 
+  destruct (Float32.cmp Cne f Float32.zero); constructor. 
 (* pointer *)
   econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
   unfold Val.cmpu, Val.cmpu_bool. simpl.
@@ -357,6 +361,9 @@ Lemma make_absfloat_correct:
 Proof.
   unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1;
   destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
+  unfold make_floatoflong, cast_long_float. destruct s.
+  econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. 
+  econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. 
 Qed.
 
 Lemma make_notbool_correct:
@@ -396,7 +403,8 @@ Section MAKE_BIN.
 Variable sem_int: signedness -> int -> int -> option val.
 Variable sem_long: signedness -> int64 -> int64 -> option val.
 Variable sem_float: float -> float -> option val.
-Variables iop iopu fop lop lopu: binary_operation.
+Variable sem_single: float32 -> float32 -> option val.
+Variables iop iopu fop sop lop lopu: binary_operation.
 
 Hypothesis iop_ok:
   forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y.
@@ -408,11 +416,13 @@ Hypothesis lopu_ok:
   forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y.
 Hypothesis fop_ok:
   forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y.
+Hypothesis sop_ok:
+  forall x y m, eval_binop sop (Vsingle x) (Vsingle y) m = sem_single x y.
 
 Lemma make_binarith_correct:
   binary_constructor_correct
-    (make_binarith iop iopu fop lop lopu)
-    (sem_binarith sem_int sem_long sem_float).
+    (make_binarith iop iopu fop sop lop lopu)
+    (sem_binarith sem_int sem_long sem_float sem_single).
 Proof.
   red; unfold make_binarith, sem_binarith;
   intros until m; intros SEM MAKE EV1 EV2.
@@ -429,12 +439,13 @@ Proof.
 - destruct s; inv H0; econstructor; eauto with cshm. 
   rewrite lop_ok; auto. rewrite lopu_ok; auto.
 - erewrite <- fop_ok in SEM; eauto with cshm.
+- erewrite <- sop_ok in SEM; eauto with cshm.
 Qed.
 
 Lemma make_binarith_int_correct:
   binary_constructor_correct
     (make_binarith_int iop iopu lop lopu)
-    (sem_binarith sem_int sem_long (fun x y => None)).
+    (sem_binarith sem_int sem_long (fun x y => None) (fun x y => None)).
 Proof.
   red; unfold make_binarith_int, sem_binarith;
   intros until m; intros SEM MAKE EV1 EV2.
@@ -930,6 +941,8 @@ Proof.
   apply make_intconst_correct.
 (* const float *)
   apply make_floatconst_correct.
+(* const single *)
+  apply make_singleconst_correct.
 (* const long *)
   apply make_longconst_correct.
 (* temp var *)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 41d0dcb..c437a6b 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -196,6 +196,18 @@ Definition typeconv (ty: type) : type :=
   | _                   => remove_attributes ty
   end.
 
+(** Default conversion for arguments to an unprototyped or variadic function.
+  Like [typeconv] but also converts single floats to double floats. *)
+
+Definition default_argument_conversion (ty: type) : type :=
+  match ty with
+  | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr
+  | Tfloat _ _          => Tfloat F64 noattr
+  | Tarray t sz a       => Tpointer t noattr
+  | Tfunction _ _ _     => Tpointer ty noattr
+  | _                   => remove_attributes ty
+  end.
+
 (** * Operations over types *)
 
 (** Alignment of a type, in bytes. *)
@@ -723,12 +735,3 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
 Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
   mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
 
-(** Like [typ_of_type], but apply default argument promotion. *)
-
-Definition typ_of_type_default (t: type) : AST.typ :=
-  match t with
-  | Tfloat _ _ => AST.Tfloat
-  | Tlong _ _ => AST.Tlong
-  | _ => AST.Tint
-  end.
-
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 4054f6e..3454ddc 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -55,7 +55,7 @@ Fixpoint constval (a: expr) : res val :=
   match a with
   | Eval v ty =>
       match v with
-      | Vint _ | Vfloat _ | Vlong _ => OK v
+      | Vint _ | Vfloat _ | Vsingle _ | Vlong _ => OK v
       | Vptr _ _ | Vundef => Error(msg "illegal constant")
       end
   | Evalof l ty =>
@@ -156,7 +156,7 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   | Vint n, Tpointer _ _ => OK(Init_int32 n)
   | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n)
   | Vlong n, Tlong _ _ => OK(Init_int64 n)
-  | Vfloat f, Tfloat F32 _ => OK(Init_float32 f)
+  | Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
   | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
   | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index f11901d..16004fc 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -506,6 +506,9 @@ Proof.
   (* float *)
   destruct ty; try discriminate. 
   destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
+  (* single *)
+  destruct ty; try discriminate. 
+  destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
   (* pointer *)
   unfold inj in H.
   assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32).
@@ -525,20 +528,18 @@ Lemma transl_init_single_size:
   Genv.init_data_size data = sizeof ty.
 Proof.
   intros. monadInv H. destruct x0. 
-  monadInv EQ2.
-  destruct ty; try discriminate. 
+- monadInv EQ2.
+- destruct ty; try discriminate. 
   destruct i0; inv EQ2; auto.
   inv EQ2; auto.
   inv EQ2; auto.
-  destruct ty; inv EQ2; auto.
-  destruct ty; try discriminate.
+- destruct ty; inv EQ2; auto.
+- destruct ty; try discriminate.
   destruct f0; inv EQ2; auto.
-  destruct ty; try discriminate.
-  destruct i0; auto.
-  inv EQ2.
-  inv EQ2.
-  inv EQ2; auto.
-  inv EQ2.
+- destruct ty; try discriminate.
+  destruct f0; inv EQ2; auto.
+- destruct ty; try discriminate.
+  destruct i0; inv EQ2; auto.
   inv EQ2; auto.
   inv EQ2; auto.
 Qed.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 49705c4..c5a6e6e 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -43,6 +43,7 @@ let rec precedence = function
   | Efield _ -> (16, LtoR)
   | Econst_int _ -> (16, NA)
   | Econst_float _ -> (16, NA)
+  | Econst_single _ -> (16, NA)
   | Econst_long _ -> (16, NA)
   | Eunop _ -> (15, RtoL)
   | Eaddrof _ -> (15, RtoL)
@@ -82,6 +83,8 @@ let rec expr p (prec, e) =
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst_float(f, _) ->
       fprintf p "%F" (camlfloat_of_coqfloat f)
+  | Econst_single(f, _) ->
+      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
   | Econst_long(n, Tlong(Unsigned, _)) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Econst_long(n, _) ->
@@ -269,6 +272,7 @@ let rec collect_expr e =
   match e with
   | Econst_int _ -> ()
   | Econst_float _ -> ()
+  | Econst_single _ -> ()
   | Econst_long _ -> ()
   | Evar _ -> ()
   | Etempvar _ -> ()
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 9441d71..4e0ee7f 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -191,6 +191,8 @@ let print_typed_value p v ty =
       fprintf p "%ld" (camlint_of_coqint n)
   | Vfloat f, _ ->
       fprintf p "%F" (camlfloat_of_coqfloat f)
+  | Vsingle f, _ ->
+      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
   | Vlong n, Tlong(Unsigned, _) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Vlong n, _ ->
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index f9aa8db..05d9c86 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -116,6 +116,7 @@ Function eval_simpl_expr (a: expr) : option val :=
   match a with
   | Econst_int n _ => Some(Vint n)
   | Econst_float n _ => Some(Vfloat n)
+  | Econst_single n _ => Some(Vsingle n)
   | Econst_long n _ => Some(Vlong n)
   | Ecast b ty => 
       match eval_simpl_expr b with
@@ -242,6 +243,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       ret (finish dst nil (Econst_int n ty))
   | Csyntax.Eval (Vfloat n) ty =>
       ret (finish dst nil (Econst_float n ty))
+  | Csyntax.Eval (Vsingle n) ty =>
+      ret (finish dst nil (Econst_single n ty))
   | Csyntax.Eval (Vlong n) ty =>
       ret (finish dst nil (Econst_long n ty))
   | Csyntax.Eval _ ty =>
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 3dae7ab..1ef2e76 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -799,6 +799,10 @@ Opaque makeif.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
+  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 *)
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 2956508..9c52928 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -45,7 +45,8 @@ Definition make_cast (a: expr) (tto: type) : expr :=
   match classify_cast (typeof a) tto with
   | cast_case_neutral => a
   | cast_case_i2i I32 _ => a
-  | cast_case_f2f F64 => a
+  | cast_case_f2f => a
+  | cast_case_s2s => a
   | cast_case_l2l => a
   | cast_case_struct _ _ _ _ => a
   | cast_case_union _ _ _ _ => a
@@ -59,6 +60,7 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
   match a with
   | Econst_int _ _ => a
   | Econst_float _ _ => a
+  | Econst_single _ _ => a
   | Econst_long _ _ => a
   | Evar id ty => if VSet.mem id cenv then Etempvar id ty else Evar id ty
   | Etempvar id ty => Etempvar id ty
@@ -157,6 +159,7 @@ Fixpoint addr_taken_expr (a: expr): VSet.t :=
   match a with
   | Econst_int _ _ => VSet.empty
   | Econst_float _ _ => VSet.empty
+  | Econst_single _ _ => VSet.empty
   | Econst_long _ _ => VSet.empty
   | Evar id ty => VSet.empty
   | Etempvar id ty => VSet.empty
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 6eec8cc..6024de4 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -189,9 +189,10 @@ 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 sz attr n,
-      cast_float_float sz n = n ->
-      val_casted (Vfloat n) (Tfloat sz 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,
@@ -220,14 +221,6 @@ Proof.
   destruct (Int.eq i Int.zero); auto.
 Qed.
 
-Remark cast_float_float_idem:
-  forall sz f, cast_float_float sz (cast_float_float sz f) = cast_float_float sz f.
-Proof.
-  intros; destruct sz; simpl.
-  apply Float.singleoffloat_idem; auto.
-  auto.
-Qed.
-
 Lemma cast_val_is_casted:
   forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'.
 Proof.
@@ -235,28 +228,32 @@ Proof.
 (* void *)
   constructor.
 (* int *)
-  destruct i; destruct ty; simpl in H; try discriminate; destruct v; inv H.
+  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_float_int s f0); inv H1.   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_float_int s f0); inv H1.   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_float_int s f0); inv H1. constructor. auto.
-  constructor. auto.
-  constructor.
+  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; auto.
-  constructor; auto.
+  constructor.
   constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
   constructor. simpl. destruct (Int64.eq i Int64.zero); auto.
-  constructor. simpl. destruct (Float.cmp Ceq f0 Float.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; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
@@ -266,23 +263,17 @@ Proof.
   constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
   constructor; auto.
 (* long *)
-  destruct ty; try discriminate.
+  destruct ty; try (destruct f); try discriminate.
   destruct v; inv H. constructor.
   destruct v; inv H. constructor.
-  destruct v; try discriminate. destruct (cast_float_long s f0); 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.
   destruct v; inv H. constructor.
 (* float *)
-  destruct ty; simpl in H; try discriminate; destruct v; inv H.
-  constructor. unfold cast_float_float, cast_int_float.
-  destruct f; destruct s; auto.
-  rewrite Float.singleofint_floatofint. apply Float.singleoffloat_idem.
-  rewrite Float.singleofintu_floatofintu. apply Float.singleoffloat_idem.
-  constructor. unfold cast_float_float, cast_long_float.
-  destruct f; destruct s; auto. apply Float.singleoflong_idem. apply Float.singleoflongu_idem.
-  constructor. apply cast_float_float_idem.
+  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 *)
@@ -310,7 +301,8 @@ Proof.
   clear H1. inv H0. auto.
   inversion H0; clear H0; subst chunk. simpl in *. 
   destruct (Int.eq n Int.zero); subst n; reflexivity.
-  destruct sz; inversion H0; clear H0; subst chunk; simpl in *; congruence.
+  inv H0; auto.
+  inv H0; auto.
   inv H0; auto.
   inv H0; auto.
   inv H0; auto.
@@ -327,7 +319,6 @@ Lemma cast_val_casted:
 Proof.
   intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto.
   destruct sz; congruence.
-  congruence.
   unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
   unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
 Qed.
@@ -373,7 +364,8 @@ Proof.
   destruct (classify_cast (typeof a) tto); auto.
   destruct v1; inv H0; auto.
   destruct sz2; auto. destruct v1; inv H0; auto.
-  destruct sz2; auto. destruct v1; inv H0; auto.
+  destruct v1; inv H0; auto.
+  destruct v1; inv H0; auto.
   destruct v1; inv H0; auto.
   destruct v1; try discriminate.
   destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
@@ -1416,6 +1408,7 @@ Proof.
 (* const *)
   exists (Vint i); split; auto. constructor.
   exists (Vfloat f0); split; auto. constructor.
+  exists (Vsingle f0); split; auto. constructor.
   exists (Vlong i); split; auto. constructor.
 (* tempvar *)
   exploit me_temps; eauto. intros [[tv [A B]] C].