From 8968126573bbf34dd4741566f8c911d4279e8107 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 11:45:17 +0200
Subject: [PATCH] [wp] type utilities
---
src/plugins/wp/ctypes.ml | 7 +++++--
src/plugins/wp/ctypes.mli | 2 ++
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 303790f3b75..1511490737d 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 7efea62f13c..c6dbf0bd409 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
--
GitLab