Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)

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

1 files changed, 10 insertions, 10 deletions

diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 2924c3d4..2548f3b9 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -45,16 +45,16 @@ let const pp = function
         | IUInt -> fprintf pp "U"
         | _ -> ()
       end
-  | CFloat(v, fk, s) ->
-      if s <> "" then
-        fprintf pp "%s" s
-      else begin
-        fprintf pp "%.18g" v;
-        match fk with
-        | FFloat -> fprintf pp "F"
-        | FLongDouble -> fprintf pp "L"
-        | _ -> ()
-      end
+  | CFloat(v, fk) ->
+    if v.hex then
+      fprintf pp "0x%s.%sP%s" v.intPart v.fracPart v.exp
+    else
+      fprintf pp "%s.%sE%s" v.intPart v.fracPart v.exp;
+    begin match fk with
+      | FFloat -> fprintf pp "F"
+      | FLongDouble -> fprintf pp "L"
+      | FDouble -> ()
+    end
   | CStr s ->
       fprintf pp "\"";
       for i = 0 to String.length s - 1 do