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, 12 insertions, 9 deletions

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