diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-09 15:55:07 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-09 15:55:07 +0100 |
commit | 32205e08619fa8fce63caaf46a289d1868982a0a (patch) | |
tree | c13fa64981785902f68009ec7a8170496cf5a7a9 | |
parent | 251bd245dd2709ffd553a2dec48e05853acc0cf7 (diff) | |
download | compcert-32205e08619fa8fce63caaf46a289d1868982a0a.tar.gz compcert-32205e08619fa8fce63caaf46a289d1868982a0a.zip |
More tweaking of module 'open'
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
-rw-r--r-- | cfrontend/C2C.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f2fbf255..6a33c48d 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -16,6 +16,8 @@ open C open Camlcoq +open Floats +open Values open Ctypes open Csyntax @@ -366,8 +368,8 @@ let globals_for_strings globs = let constant_size_t a = match Initializers.constval_cast !comp_env a Ctyping.size_t with - | Errors.OK(Values.Vint n) -> Some(Integers.Int.unsigned n) - | Errors.OK(Values.Vlong n) -> Some(Integers.Int64.unsigned n) + | Errors.OK(Vint n) -> Some(Integers.Int.unsigned n) + | Errors.OK(Vlong n) -> Some(Integers.Int64.unsigned n) | _ -> None let make_builtin_memcpy args = @@ -444,7 +446,7 @@ let make_builtin_va_arg env ty e = "__compcert_va_composite" ty e | _ -> unsupported "va_arg at this type"; - Eval(Values.Vint(coqint_of_camlint 0l), type_int32s) + Eval(Vint(coqint_of_camlint 0l), type_int32s) (** ** Translation functions *) @@ -630,9 +632,9 @@ let convertFloat f kind = | Z.Z0 -> begin match kind with | FFloat -> - Ctyping.econst_single (Floats.Float.to_single Floats.Float.zero) + Ctyping.econst_single (Float.to_single Float.zero) | FDouble | FLongDouble -> - Ctyping.econst_float Floats.Float.zero + Ctyping.econst_float Float.zero end | Z.Zpos mant -> @@ -647,11 +649,11 @@ let convertFloat f kind = begin match kind with | FFloat -> - let f = Floats.Float32.from_parsed base mant exp in + let f = Float32.from_parsed base mant exp in checkFloatOverflow f "float"; Ctyping.econst_single f | FDouble | FLongDouble -> - let f = Floats.Float.from_parsed base mant exp in + let f = Float.from_parsed base mant exp in checkFloatOverflow f "double"; Ctyping.econst_float f end @@ -660,7 +662,7 @@ let convertFloat f kind = (** Expressions *) -let ezero = Eval(Values.Vint(coqint_of_camlint 0l), type_int32s) +let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function | Errors.OK e -> e |