Keep string representation in AReal for printing again

src/cil.ml

@@ -323,7 +323,7 @@ and attributes = attribute list
 (** The type of parameters in attributes *)
 and attrparam =
   | AInt of int                          (** An integer constant *)
-  | AReal of float                       (** A floating-point constant *)
+  | AReal of float * string option       (** A floating-point constant *)
   | AStr of string                       (** A string constant *)
   | ACons of string * attrparam list       (** Constructed attributes. These
                                              are printed [foo(a1,a2,...,an)].
@@ -4393,7 +4393,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     let level = getParenthLevelAttrParam a in
     match a with
     | AInt n -> num n
-    | AReal f -> text (string_of_float f)
+    | AReal (_, Some s) -> text s
+    | AReal (f, None) -> text (string_of_float f)
     | AStr s -> text ("\"" ^ escape_string s ^ "\"")
     | ACons(s, []) -> text s
     | ACons(s,al) ->

src/cil.mli

@@ -317,7 +317,7 @@ and attributes = attribute list
 (** The type of parameters of attributes *)
 and attrparam =
   | AInt of int                          (** An integer constant *)
-  | AReal of float                       (** A floating-point constant *)
+  | AReal of float * string option       (** A floating-point constant *)
   | AStr of string                       (** A string constant *)
   | ACons of string * attrparam list       (** Constructed attributes. These
                                              are printed [foo(a1,a2,...,an)].

src/frontc/cabs2cil.ml

@@ -2929,7 +2929,7 @@ and doAttr (a: A.attribute) : attribute list =
           end
         | A.CONSTANT (A.CONST_FLOAT str) -> begin
             match float_of_string_opt str with
-            | Some f -> AReal f
+            | Some f -> AReal (f, Some str)
             | None -> E.s (error "Invalid attribute constant: %s")
           end
         | A.CALL(A.VARIABLE n, args) -> begin