aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-07-26 15:06:11 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-07-26 15:06:11 +0200
commitc7832c32253cdc2123313731c7cbbace4fc8332c (patch)
treee5581bd68a8c8219191877d22226c565c11928af /debug
parent5b6027e5444dfe6a3d02673770347bb4e7fc0658 (diff)
downloadcompcert-kvx-c7832c32253cdc2123313731c7cbbace4fc8332c.tar.gz
compcert-kvx-c7832c32253cdc2123313731c7cbbace4fc8332c.zip
Use asprintf instead of printing to a buffer.
Diffstat (limited to 'debug')
-rw-r--r--debug/DebugInformation.ml7
1 files changed, 2 insertions, 5 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 471318af..dfde9136 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -53,13 +53,10 @@ let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7
(* Translate a C.typ to a string needed for hashing *)
let typ_to_string ty =
- let buf = Buffer.create 7 in
- let chan = Format.formatter_of_buffer buf in
Cprint.print_debug_idents := true;
- Cprint.typ chan ty;
+ let s = Format.asprintf "%a" Cprint.typ ty in
Cprint.print_debug_idents := false;
- Format.pp_print_flush chan ();
- Buffer.contents buf
+ s
(* Helper functions for the attributes *)
let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile]