diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
commit | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch) | |
tree | 2f59373790d8ce3a5df66ef7a692271cf0666c6c /cfrontend/C2C.ml | |
parent | 00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff) | |
download | compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.tar.gz compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.zip |
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
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r-- | cfrontend/C2C.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d389d0a8..e7d83377 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) |