From 076e0afe29e6feb6a40b621e2dd458ed0b13f373 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 9 Jun 2022 16:43:30 +0200
Subject: [PATCH] [Kernel] avoid recursion and fix layout of debug
pretty-printers
---
src/kernel_services/ast_printing/cil_types_debug.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index b486c47ae63..e4ce5c819f9 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -43,7 +43,7 @@ let print_full_varinfo = false
let print_full_fundec = false
let print_full_spec = false
-let pp_list fmt = Pretty_utils.pp_list fmt ~sep:", " ~pre:"[" ~last:"]" ~suf:"" ~empty:"[]"
+let pp_list fmt = Pretty_utils.pp_list fmt ~sep:"; " ~pre:"[" ~suf:"]" ~empty:"[]"
let pp_option fmt = Pretty_utils.pp_opt ~none:"None" ~pre:"Some(" ~suf:")" fmt
let pp_ref pp fmt r = Format.fprintf fmt "Ref(%a)" pp !r
let pp_pair fmt1 fmt2 = Pretty_utils.pp_pair ~pre:"(" ~sep:", " ~suf:")" fmt1 fmt2
@@ -350,7 +350,7 @@ and pp_varinfo fmt varinfo =
vdescrpure=%a;\
vghost=%a;\
vsource=%a;\
- vlogic_var_assoc=%a;\
+ vlogic_var_assoc=%s;\
}"
pp_string varinfo.vname
pp_string varinfo.vorig_name
@@ -370,7 +370,8 @@ and pp_varinfo fmt varinfo =
pp_bool varinfo.vdescrpure
pp_bool varinfo.vghost
pp_bool varinfo.vsource
- (pp_option pp_logic_var) varinfo.vlogic_var_assoc
+ (* the code below prevents infinite recursion *)
+ (if varinfo.vlogic_var_assoc = None then "None" else "Some " ^ (Option.get varinfo.vlogic_var_assoc).lv_name)
else
Format.fprintf fmt "{vname=%a;vid=%a}"
pp_string varinfo.vname
--
GitLab