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

1 files changed, 5 insertions, 1 deletions

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index f2ba2405..d9fb6501 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,