diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 303790f3b75d254f3e616e6b92cfa919eafbe3fb..1511490737dca9c73d0586cd5b47119abeb27fab 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -226,6 +226,9 @@ let pp_object fmt = function
   | C_comp _ -> Format.pp_print_string fmt "obj-struct/union"
   | C_array _ -> Format.pp_print_string fmt "obj-array"
 
+let i_name = i_memo (Pretty_utils.to_string pp_int)
+let f_name = f_memo (Pretty_utils.to_string pp_float)
+
 (* -------------------------------------------------------------------------- *)
 (* --- Array Info                                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -525,8 +528,8 @@ let promote a1 a2 =
            "promotion between arithmetics and pointer types"
 
 let rec basename = function
-  | C_int i -> Format.asprintf "%a" pp_int i
-  | C_float f -> Format.asprintf "%a" pp_float f
+  | C_int i -> i_name i
+  | C_float f -> f_name f
   | C_pointer _ -> "pointer"
   | C_comp c -> c.cname
   | C_array a ->
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 7efea62f13c30e9323b335affd29df2e7ebfa7af..c6dbf0bd4098686f600d1cd41ebc28d2b78e8beb 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -142,6 +142,8 @@ val pp_int : Format.formatter -> c_int -> unit
 val pp_float : Format.formatter -> c_float -> unit
 val pp_object : Format.formatter -> c_object -> unit
 
+val i_name : c_int -> string
+val f_name : c_float -> string
 val basename : c_object -> string
 val compare : c_object -> c_object -> int
 val equal : c_object -> c_object -> bool