From dcb9f48f51cec5e864565862a700c27df2a1a7e6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 3 Nov 2012 10:36:15 +0000
Subject: 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
---
 cparser/Cprint.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'cparser/Cprint.ml')

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