Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


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

1 files changed, 10 insertions, 4 deletions

diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 1a19f710..1ca13ff8 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -15,25 +15,31 @@
 
 (* A type-checker for Cminor *)
 
+(* FIXME: proper support for type Tsingle *)
+
 open Printf
 open Datatypes
 open Camlcoq
 open AST
+open PrintAST
 open Integers
 open Cminor
 
 exception Error of string
 
-let name_of_typ = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long"
-
 type ty = Base of typ | Var of ty option ref
 
 let newvar () = Var (ref None)
 let tint = Base Tint
 let tfloat = Base Tfloat
 let tlong = Base Tlong
+let tsingle = Base Tsingle
 
-let ty_of_typ = function Tint -> tint | Tfloat -> tfloat | Tlong -> tlong
+let ty_of_typ = function
+  | Tint -> tint
+  | Tfloat -> tfloat
+  | Tlong -> tlong
+  | Tsingle -> tsingle
 
 let ty_of_sig_args tyl = List.map ty_of_typ tyl
 
@@ -47,7 +53,7 @@ let unify t1 t2 =
   | Base b1, Base b2 ->
       if b1 <> b2 then
         raise (Error (sprintf "Expected type %s, actual type %s\n"
-                              (name_of_typ b1) (name_of_typ b2)))
+                              (name_of_type b1) (name_of_type b2)))
   | Base b, Var r -> r := Some (Base b)
   | Var r, Base b -> r := Some (Base b)
   | Var r1, Var r2 -> r1 := Some (Var r2)