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, 2 insertions, 2 deletions

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 4054f6e1..3454ddcf 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)