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, 3 insertions, 0 deletions

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 =>