diff --git a/src/cil.ml b/src/cil.ml
index d5a0e20a0..8e326d92c 100755
--- a/src/cil.ml
+++ b/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) ->
diff --git a/src/cil.mli b/src/cil.mli
index 0008daa6c..20ce96f15 100644
--- a/src/cil.mli
+++ b/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)].
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 245cce191..b7c4a2149 100644
--- a/src/frontc/cabs2cil.ml
+++ b/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