From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: 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 --- cfrontend/C2C.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d389d0a..e7d8337 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -441,7 +441,13 @@ let z_of_str hex str fst = let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in match mant with - | Z.Z0 -> Float.zero + | Z.Z0 -> + begin match kind with + | FFloat -> + Vsingle (Float.to_single Float.zero) + | FDouble | FLongDouble -> + Vfloat Float.zero + end | Z.Zpos mant -> let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in @@ -454,10 +460,10 @@ let convertFloat f kind = let base = P.of_int (if f.C.hex then 2 else 10) in begin match kind with - | FFloat -> - Float.build_from_parsed32 base mant exp - | FDouble | FLongDouble -> - Float.build_from_parsed64 base mant exp + | FFloat -> + Vsingle (Float32.from_parsed base mant exp) + | FDouble | FLongDouble -> + Vfloat (Float.from_parsed base mant exp) end | Z.Zneg _ -> assert false @@ -482,7 +488,7 @@ let rec convertExpr env e = | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point literal"; - Eval(Vfloat(convertFloat f k), ty) + Eval(convertFloat f k, ty) | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in Evalof(Evar(name_for_string_literal env s, ty), ty) -- cgit v1.2.3