diff --git a/infer/src/IR/PredSymb.ml b/infer/src/IR/PredSymb.ml
index cef625a00..73e8401a1 100644
--- a/infer/src/IR/PredSymb.ml
+++ b/infer/src/IR/PredSymb.ml
@@ -257,5 +257,7 @@ let to_string pe = function
"WONT_LEAK"
+let pp pe fmt a = F.pp_print_string fmt (to_string pe a)
+
(** dump an attribute *)
-let d_attribute (a: t) = L.add_print_action (L.PTattribute, Obj.repr a)
+let d_attribute (a: t) = L.add_print_with_pe pp a
diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml
index 98d98fbbe..3afc0352d 100644
--- a/infer/src/IR/Procdesc.ml
+++ b/infer/src/IR/Procdesc.ml
@@ -168,7 +168,7 @@ module Node = struct
(** Print extended instructions for the node,
highlighting the given subinstruction if present *)
- let pp_instrs pe0 ~sub_instrs instro fmt node =
+ let pp_instrs pe0 ~sub_instrs ~instro fmt node =
if sub_instrs then
let pe =
match instro with None -> pe0 | Some instr -> Pp.extend_colormap pe0 (Obj.repr instr) Red
@@ -196,7 +196,7 @@ module Node = struct
(** Dump extended instructions for the node *)
let d_instrs ~(sub_instrs: bool) (curr_instr: Sil.instr option) (node: t) =
- L.add_print_action (L.PTnode_instrs, Obj.repr (sub_instrs, curr_instr, node))
+ L.add_print_with_pe ~color:Pp.Green (pp_instrs ~sub_instrs ~instro:curr_instr) node
(** Return a description of the cfg node *)
@@ -216,7 +216,7 @@ module Node = struct
| Join_node ->
"Join"
in
- let pp fmt = F.fprintf fmt "%s@.%a" str (pp_instrs pe None ~sub_instrs:true) node in
+ let pp fmt = F.fprintf fmt "%s@.%a" str (pp_instrs pe ~instro:None ~sub_instrs:true) node in
F.asprintf "%t" pp
end
diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli
index d9af63426..dc78d0e2c 100644
--- a/infer/src/IR/Procdesc.mli
+++ b/infer/src/IR/Procdesc.mli
@@ -99,7 +99,8 @@ module Node : sig
val pp_id : Format.formatter -> id -> unit
(** Pretty print a node id *)
- val pp_instrs : Pp.env -> sub_instrs:bool -> Sil.instr option -> Format.formatter -> t -> unit
+ val pp_instrs :
+ Pp.env -> sub_instrs:bool -> instro:Sil.instr option -> Format.formatter -> t -> unit
(** Print extended instructions for the node,
highlighting the given subinstruction if present *)
end
diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml
index 01cf294d6..63ab99412 100644
--- a/infer/src/IR/Pvar.ml
+++ b/infer/src/IR/Pvar.ml
@@ -97,7 +97,7 @@ let pp pe f pv =
(** Dump a program variable. *)
-let d (pvar: t) = L.add_print_action (L.PTpvar, Obj.repr pvar)
+let d (pvar: t) = L.add_print_with_pe pp pvar
let get_name pv = pv.pv_name
diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml
index d644f0d15..db8c462cc 100644
--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@@ -274,13 +274,13 @@ let pp_exp_printenv pe0 f e0 =
(** dump an expression. *)
-let d_exp (e: Exp.t) = L.add_print_action (L.PTexp, Obj.repr e)
+let d_exp (e: Exp.t) = L.add_print_with_pe pp_exp_printenv e
(** Pretty print a list of expressions. *)
let pp_exp_list pe f expl = Pp.seq (pp_exp_printenv pe) f expl
(** dump a list of expressions. *)
-let d_exp_list (el: Exp.t list) = L.add_print_action (L.PTexp_list, Obj.repr el)
+let d_exp_list (el: Exp.t list) = L.add_print_with_pe pp_exp_list el
let pp_texp pe f = function
| Exp.Sizeof {typ; nbytes; dynamic_length; subtype} ->
@@ -304,7 +304,7 @@ let pp_texp_full pe f = function
(** Dump a type expression with all the details. *)
-let d_texp_full (te: Exp.t) = L.add_print_action (L.PTtexp_full, Obj.repr te)
+let d_texp_full (te: Exp.t) = L.add_print_with_pe pp_texp_full te
(** Pretty print an offset *)
let pp_offset pe f = function
@@ -328,7 +328,7 @@ let rec pp_offset_list pe f = function
(** Dump a list of offsets *)
-let d_offset_list (offl: offset list) = L.add_print_action (L.PToff_list, Obj.repr offl)
+let d_offset_list (offl: offset list) = L.add_print_with_pe pp_offset_list offl
let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t
@@ -430,7 +430,7 @@ let add_with_block_parameters_flag instr =
let is_block_pvar pvar = Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar))
(** Dump an instruction. *)
-let d_instr (i: instr) = L.add_print_action (L.PTinstr, Obj.repr i)
+let d_instr (i: instr) = L.add_print_with_pe ~color:Pp.Green pp_instr i
let pp_atom pe0 f a =
let pe, changed = color_pre_wrapper pe0 f a in
@@ -449,7 +449,7 @@ let pp_atom pe0 f a =
(** dump an atom *)
-let d_atom (a: atom) = L.add_print_action (L.PTatom, Obj.repr a)
+let d_atom (a: atom) = L.add_print_with_pe pp_atom a
let pp_lseg_kind f = function Lseg_NE -> F.pp_print_string f "ne" | Lseg_PE -> ()
@@ -881,13 +881,10 @@ let pp_hpara_dll pe f = pp_hpara_dll_env pe None f
let pp_hpred pe f = pp_hpred_env pe None f
(** dump a strexp. *)
-let d_sexp (se: strexp) = L.add_print_action (L.PTsexp, Obj.repr se)
-
-(** Pretty print a list of expressions. *)
-let pp_sexp_list pe f sel = (Pp.seq (fun f se -> (pp_sexp pe) f se)) f sel
+let d_sexp (se: strexp) = L.add_print_with_pe pp_sexp se
(** dump a hpred. *)
-let d_hpred (hpred: hpred) = L.add_print_action (L.PThpred, Obj.repr hpred)
+let d_hpred (hpred: hpred) = L.add_print_with_pe pp_hpred hpred
(** {2 Functions for traversing SIL data types} *)
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index 96cd0103f..976c00d1a 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -270,21 +270,12 @@ val pp_texp_full : Pp.env -> F.formatter -> Exp.t -> unit
val d_texp_full : Exp.t -> unit
(** Dump a type expression with all the details. *)
-val pp_exp_list : Pp.env -> F.formatter -> Exp.t list -> unit
-(** Pretty print a list of expressions. *)
-
val d_exp_list : Exp.t list -> unit
(** Dump a list of expressions. *)
-val pp_offset : Pp.env -> F.formatter -> offset -> unit
-(** Pretty print an offset *)
-
val offset_to_string : offset -> string
(** Convert an offset to a string *)
-val pp_offset_list : Pp.env -> F.formatter -> offset list -> unit
-(** Pretty print a list of offsets *)
-
val d_offset_list : offset list -> unit
(** Dump a list of offsets *)
@@ -318,9 +309,6 @@ val pp_sexp : Pp.env -> F.formatter -> strexp -> unit
val d_sexp : strexp -> unit
(** Dump a strexp. *)
-val pp_sexp_list : Pp.env -> F.formatter -> strexp list -> unit
-(** Pretty print a strexp list. *)
-
val pp_hpred : Pp.env -> F.formatter -> hpred -> unit
(** Pretty print a hpred. *)
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 9ffdc464a..aa553be81 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -490,10 +490,13 @@ module Name = struct
end
(** dump a type with all the details. *)
-let d_full (t: t) = L.add_print_action (L.PTtyp_full, Obj.repr t)
+let d_full (t: t) = L.add_print_with_pe pp_full t
(** dump a list of types. *)
-let d_list (tl: t list) = L.add_print_action (L.PTtyp_list, Obj.repr tl)
+let d_list (tl: t list) =
+ let pp pe = Pp.seq (pp pe) in
+ L.add_print_with_pe pp tl
+
let name typ = match typ.desc with Tstruct name -> Some name | _ -> None
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index 9cdf240d6..78eec5d2f 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -75,7 +75,7 @@ let procedure_should_be_analyzed proc_name =
type global_state =
{ abs_val: int
; abstraction_rules: Abs.rules
- ; delayed_prints: L.print_action list
+ ; delayed_prints: L.delayed_prints
; footprint_mode: bool
; html_formatter: F.formatter
; name_generator: Ident.NameGenerator.t
diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml
index a67b1aa4f..e3186f3d3 100644
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@@ -163,164 +163,12 @@ end
(* =============== END of module NodesHtml =============== *)
(* =============== Printing functions =============== *)
-(** Execute the delayed print actions *)
-let force_delayed_print fmt =
- let pe_default = if Config.write_html then Pp.html Black else Pp.text in
- function
- | L.PTatom, a ->
- let a : Sil.atom = Obj.obj a in
- Sil.pp_atom pe_default fmt a
- | L.PTattribute, a ->
- let a : PredSymb.t = Obj.obj a in
- F.pp_print_string fmt (PredSymb.to_string pe_default a)
- | L.PTdecrease_indent, n ->
- let n : int = Obj.obj n in
- for _ = 1 to n do F.fprintf fmt "@]" done
- | L.PTexp, e ->
- let e : Exp.t = Obj.obj e in
- Sil.pp_exp_printenv pe_default fmt e
- | L.PTexp_list, el ->
- let el : Exp.t list = Obj.obj el in
- Sil.pp_exp_list pe_default fmt el
- | L.PThpred, hpred ->
- let hpred : Sil.hpred = Obj.obj hpred in
- Sil.pp_hpred pe_default fmt hpred
- | L.PTincrease_indent, n ->
- let n : int = Obj.obj n in
- F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
- | L.PTinstr, i ->
- let i : Sil.instr = Obj.obj i in
- if Config.write_html then
- F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
- (Sil.pp_instr (Pp.html Green))
- i Io_infer.Html.pp_end_color ()
- else Sil.pp_instr Pp.text fmt i
- | L.PTinstr_list, il ->
- let il : Instrs.not_reversed_t = Obj.obj il in
- if Config.write_html then
- F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
- (Instrs.pp (Pp.html Green))
- il Io_infer.Html.pp_end_color ()
- else Instrs.pp Pp.text fmt il
- | L.PTjprop_list, shallow_jpl ->
- let (shallow: bool), (jpl: Prop.normal BiabductionSummary.Jprop.t list) =
- Obj.obj shallow_jpl
- in
- BiabductionSummary.Jprop.pp_list pe_default ~shallow fmt jpl
- | L.PTjprop_short, jp ->
- let jp : Prop.normal BiabductionSummary.Jprop.t = Obj.obj jp in
- BiabductionSummary.Jprop.pp_short pe_default fmt jp
- | L.PTloc, loc ->
- let loc : Location.t = Obj.obj loc in
- Location.pp fmt loc
- | L.PTnode_instrs, b_n ->
- let (b: bool), (io: Sil.instr option), (n: Procdesc.Node.t) = Obj.obj b_n in
- if Config.write_html then
- F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
- (Procdesc.Node.pp_instrs (Pp.html Green) io ~sub_instrs:b)
- n Io_infer.Html.pp_end_color ()
- else Procdesc.Node.pp_instrs Pp.text io ~sub_instrs:b fmt n
- | L.PToff, off ->
- let off : Sil.offset = Obj.obj off in
- Sil.pp_offset pe_default fmt off
- | L.PToff_list, offl ->
- let offl : Sil.offset list = Obj.obj offl in
- Sil.pp_offset_list pe_default fmt offl
- | L.PTpathset, ps ->
- let ps : Paths.PathSet.t = Obj.obj ps in
- F.fprintf fmt "%a@\n" (Paths.PathSet.pp pe_default) ps
- | L.PTpi, pi ->
- let pi : Sil.atom list = Obj.obj pi in
- Prop.pp_pi pe_default fmt pi
- | L.PTpath, path ->
- let path : Paths.Path.t = Obj.obj path in
- Paths.Path.pp fmt path
- | L.PTprop, p ->
- let p : Prop.normal Prop.t = Obj.obj p in
- Prop.pp_prop pe_default fmt p
- | L.PTproplist, x ->
- let (p: Prop.normal Prop.t), (pl: Prop.normal Prop.t list) = Obj.obj x in
- Propgraph.pp_proplist pe_default "PROP" (p, false) fmt pl
- | L.PTprop_list_with_typ, plist ->
- let pl : Prop.normal Prop.t list = Obj.obj plist in
- Prop.pp_proplist_with_typ pe_default fmt pl
- | L.PTprop_with_typ, p ->
- let p : Prop.normal Prop.t = Obj.obj p in
- Prop.pp_prop_with_typ pe_default fmt p
- | L.PTpvar, pvar ->
- let pvar : Pvar.t = Obj.obj pvar in
- Pvar.pp pe_default fmt pvar
- | L.PTsexp, se ->
- let se : Sil.strexp = Obj.obj se in
- Sil.pp_sexp pe_default fmt se
- | L.PTsexp_list, sel ->
- let sel : Sil.strexp list = Obj.obj sel in
- Sil.pp_sexp_list pe_default fmt sel
- | L.PTsigma, sigma ->
- let sigma : Sil.hpred list = Obj.obj sigma in
- Prop.pp_sigma pe_default fmt sigma
- | L.PTspec, spec ->
- let spec : Prop.normal BiabductionSummary.spec = Obj.obj spec in
- BiabductionSummary.pp_spec
- (if Config.write_html then Pp.html Blue else Pp.text)
- None fmt spec
- | L.PTstr, s ->
- let s : string = Obj.obj s in
- F.pp_print_string fmt s
- | L.PTstr_color, s ->
- let (s: string), (c: Pp.color) = Obj.obj s in
- if Config.write_html then
- F.fprintf fmt "%a%s%a" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color ()
- else F.pp_print_string fmt s
- | L.PTstrln, s ->
- let s : string = Obj.obj s in
- F.fprintf fmt "%s@\n" s
- | L.PTstrln_color, s ->
- let (s: string), (c: Pp.color) = Obj.obj s in
- if Config.write_html then
- F.fprintf fmt "%a%s%a@\n" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color ()
- else F.fprintf fmt "%s@\n" s
- | L.PTsub, sub ->
- let sub : Sil.subst = Obj.obj sub in
- Prop.pp_sub pe_default fmt sub
- | L.PTtexp_full, te ->
- let te : Exp.t = Obj.obj te in
- Sil.pp_texp_full pe_default fmt te
- | L.PTtyp_full, t ->
- let t : Typ.t = Obj.obj t in
- Typ.pp_full pe_default fmt t
- | L.PTtyp_list, tl ->
- let tl : Typ.t list = Obj.obj tl in
- Pp.seq (Typ.pp pe_default) fmt tl
- | L.PTerror, s ->
- let s : string = Obj.obj s in
- if Config.write_html then
- F.fprintf fmt "%aERROR: %s%a" Io_infer.Html.pp_start_color Pp.Red s
- Io_infer.Html.pp_end_color ()
- else F.fprintf fmt "ERROR: %s" s
- | L.PTwarning, s ->
- let s : string = Obj.obj s in
- if Config.write_html then
- F.fprintf fmt "%aWARNING: %s%a" Io_infer.Html.pp_start_color Pp.Orange s
- Io_infer.Html.pp_end_color ()
- else F.fprintf fmt "WARNING: %s" s
- | L.PTinfo, s ->
- let s : string = Obj.obj s in
- if Config.write_html then
- F.fprintf fmt "%aINFO: %s%a" Io_infer.Html.pp_start_color Pp.Blue s
- Io_infer.Html.pp_end_color ()
- else F.fprintf fmt "INFO: %s" s
-
-
-(** Set printer hook as soon as this module is loaded *)
-let () = L.printer_hook := force_delayed_print
-
(** Execute the delayed print actions *)
let force_delayed_prints () =
Config.forcing_delayed_prints := true ;
F.fprintf !curr_html_formatter "@?" ;
(* flush html stream *)
- List.iter ~f:(force_delayed_print !curr_html_formatter) (List.rev (L.get_delayed_prints ())) ;
+ L.force_delayed_prints !curr_html_formatter (L.get_delayed_prints ()) ;
F.fprintf !curr_html_formatter "@?" ;
L.reset_delayed_prints () ;
Config.forcing_delayed_prints := false
@@ -337,7 +185,7 @@ let start_session ~pp_name node (loc: Location.t) proc_name session source =
then
F.fprintf !curr_html_formatter "%a%a%a" Io_infer.Html.pp_start_color
Pp.Green
- (Procdesc.Node.pp_instrs (Pp.html Green) None ~sub_instrs:true)
+ (Procdesc.Node.pp_instrs (Pp.html Green) ~instro:None ~sub_instrs:true)
node Io_infer.Html.pp_end_color () ;
F.fprintf !curr_html_formatter "%a%a %t" Io_infer.Html.pp_hline ()
(Io_infer.Html.pp_session_link source ~with_name:true [".."] ~proc_name)
diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml
index 60895692c..1e5bfefe5 100644
--- a/infer/src/base/Logging.ml
+++ b/infer/src/base/Logging.ml
@@ -348,61 +348,78 @@ let setup_log_file () =
============================================================"
-(** type of printable elements *)
-type print_type =
- | PTatom
- | PTattribute
- | PTdecrease_indent
- | PTexp
- | PTexp_list
- | PThpred
- | PTincrease_indent
- | PTinstr
- | PTinstr_list
- | PTjprop_list
- | PTjprop_short
- | PTloc
- | PTnode_instrs
- | PToff
- | PToff_list
- | PTpath
- | PTprop
- | PTproplist
- | PTprop_list_with_typ
- | PTprop_with_typ
- | PTpvar
- | PTspec
- | PTstr
- | PTstr_color
- | PTstrln
- | PTstrln_color
- | PTpathset
- | PTpi
- | PTsexp
- | PTsexp_list
- | PTsigma
- | PTtexp_full
- | PTsub
- | PTtyp_full
- | PTtyp_list
- | PTwarning
- | PTerror
- | PTinfo
-
(** delayable print action *)
-type print_action = print_type * Obj.t (** data to be printed *)
+type print_action =
+ | PTdecrease_indent: int -> print_action
+ | PTincrease_indent: int -> print_action
+ | PTstr: string -> print_action
+ | PTstr_color: string * Pp.color -> print_action
+ | PTstrln: string -> print_action
+ | PTstrln_color: string * Pp.color -> print_action
+ | PTwarning: string -> print_action
+ | PTerror: string -> print_action
+ | PTinfo: string -> print_action
+ | PT_generic: (Format.formatter -> 'a -> unit) * 'a -> print_action
+ | PT_generic_with_pe:
+ Pp.color option * (Pp.env -> Format.formatter -> 'a -> unit) * 'a
+ -> print_action
+
+type delayed_prints = print_action list
let delayed_actions = ref []
-(** hook for the current printer of delayed print actions *)
-let printer_hook = ref (fun _ -> Die.(die InternalError) "uninitialized printer hook")
+let pp_with_html_color color pp fmt x =
+ F.fprintf fmt "%a" (Pp.color_string color) pp x
+
+
+let pp_maybe_with_color color pp fmt x =
+ if Config.write_html then pp fmt x else pp_with_html_color color pp fmt x
+
+
+(** Execute the delayed print actions *)
+let force_delayed_print fmt = function
+ | PTdecrease_indent n ->
+ for _ = 1 to n do F.fprintf fmt "@]" done
+ | PTincrease_indent n ->
+ F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
+ | PTstr s ->
+ F.pp_print_string fmt s
+ | PTstr_color (s, c) ->
+ pp_maybe_with_color c F.pp_print_string fmt s
+ | PTstrln s ->
+ F.fprintf fmt "%s@\n" s
+ | PTstrln_color (s, c) ->
+ F.fprintf fmt "%a@\n" (pp_maybe_with_color c F.pp_print_string) s
+ | PTerror s ->
+ pp_maybe_with_color Pp.Red (fun fmt -> F.fprintf fmt "ERROR: %s") fmt s
+ | PTwarning s ->
+ pp_maybe_with_color Pp.Orange (fun fmt -> F.fprintf fmt "WARNING: %s") fmt s
+ | PTinfo s ->
+ pp_maybe_with_color Pp.Blue (fun fmt -> F.fprintf fmt "INFO: %s") fmt s
+ | PT_generic (pp, x) ->
+ pp fmt x
+ | PT_generic_with_pe (None, pp, x) ->
+ let pe_default = if Config.write_html then Pp.html Black else Pp.text in
+ pp pe_default fmt x
+ | PT_generic_with_pe (Some color, pp, x) ->
+ if Config.write_html then pp_with_html_color color (pp (Pp.html color)) fmt x
+ else pp Pp.text fmt x
+
+
+let force_delayed_prints fmt rev_delayed_prints =
+ rev_delayed_prints |> List.rev |> List.iter ~f:(force_delayed_print fmt)
+
(** extend the current print log *)
let add_print_action pact =
if Config.write_html then delayed_actions := pact :: !delayed_actions
else if not Config.only_cheap_debug then
- Option.iter !log_file ~f:(function file_fmt, _ -> !printer_hook file_fmt pact)
+ Option.iter !log_file ~f:(function file_fmt, _ -> force_delayed_print file_fmt pact)
+
+
+let add_print pp x = add_print_action (PT_generic (pp, x))
+let add_print_with_pe ?color pp x = add_print_action (PT_generic_with_pe (color, pp, x))
(** reset the delayed print actions *)
let reset_delayed_prints () = delayed_actions := []
@@ -414,38 +431,38 @@ let get_delayed_prints () = !delayed_actions
let set_delayed_prints new_delayed_actions = delayed_actions := new_delayed_actions
(** dump a string *)
-let d_str (s: string) = add_print_action (PTstr, Obj.repr s)
+let d_str (s: string) = add_print_action (PTstr s)
(** dump a string with the given color *)
-let d_str_color (c: Pp.color) (s: string) = add_print_action (PTstr_color, Obj.repr (s, c))
+let d_str_color (c: Pp.color) (s: string) = add_print_action (PTstr_color (s, c))
(** dump an error string *)
-let d_error (s: string) = add_print_action (PTerror, Obj.repr s)
+let d_error (s: string) = add_print_action (PTerror s)
(** dump a warning string *)
-let d_warning (s: string) = add_print_action (PTwarning, Obj.repr s)
+let d_warning (s: string) = add_print_action (PTwarning s)
(** dump an info string *)
-let d_info (s: string) = add_print_action (PTinfo, Obj.repr s)
+let d_info (s: string) = add_print_action (PTinfo s)
(** dump a string plus newline *)
-let d_strln (s: string) = add_print_action (PTstrln, Obj.repr s)
+let d_strln (s: string) = add_print_action (PTstrln s)
(** dump a string plus newline with the given color *)
-let d_strln_color (c: Pp.color) (s: string) = add_print_action (PTstrln_color, Obj.repr (s, c))
+let d_strln_color (c: Pp.color) (s: string) = add_print_action (PTstrln_color (s, c))
(** dump a newline *)
-let d_ln () = add_print_action (PTstrln, Obj.repr "")
+let d_ln () = add_print_action (PTstrln "")
(** dump an indentation *)
let d_indent indent =
- let s = ref "" in
- for _ = 1 to indent do s := " " ^ !s done ;
- if indent <> 0 then add_print_action (PTstr, Obj.repr !s)
+ if indent <> 0 then
+ let s = String.make (2 * indent) ' ' in
+ add_print_action (PTstr s)
(** dump command to increase the indentation level *)
-let d_increase_indent (indent: int) = add_print_action (PTincrease_indent, Obj.repr indent)
+let d_increase_indent (indent: int) = add_print_action (PTincrease_indent indent)
(** dump command to decrease the indentation level *)
-let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent, Obj.repr indent)
+let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent indent)
diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli
index 39ce1d69d..17c85a39e 100644
--- a/infer/src/base/Logging.mli
+++ b/infer/src/base/Logging.mli
@@ -87,60 +87,18 @@ val reset_formatters : unit -> unit
(** Delayed printing (HTML debug, ...) *)
-(** type of printable elements *)
-type print_type =
- | PTatom
- | PTattribute
- | PTdecrease_indent
- | PTexp
- | PTexp_list
- | PThpred
- | PTincrease_indent
- | PTinstr
- | PTinstr_list
- | PTjprop_list
- | PTjprop_short
- | PTloc
- | PTnode_instrs
- | PToff
- | PToff_list
- | PTpath
- | PTprop
- | PTproplist
- | PTprop_list_with_typ
- | PTprop_with_typ
- | PTpvar
- | PTspec
- | PTstr
- | PTstr_color
- | PTstrln
- | PTstrln_color
- | PTpathset
- | PTpi
- | PTsexp
- | PTsexp_list
- | PTsigma
- | PTtexp_full
- | PTsub
- | PTtyp_full
- | PTtyp_list
- | PTwarning
- | PTerror
- | PTinfo
-
-(** delayable print action *)
-type print_action = print_type * Obj.t (** data to be printed *)
-
-val printer_hook : (F.formatter -> print_action -> unit) ref
-(** hook for the current printer of delayed print actions *)
-
-val add_print_action : print_action -> unit
-(** extend he current print log *)
-
-val get_delayed_prints : unit -> print_action list
+type delayed_prints
+
+val add_print : (F.formatter -> 'a -> unit) -> 'a -> unit
+
+val add_print_with_pe : ?color:Pp.color -> (Pp.env -> F.formatter -> 'a -> unit) -> 'a -> unit
+
+val force_delayed_prints : F.formatter -> delayed_prints -> unit
+
+val get_delayed_prints : unit -> delayed_prints
(** return the delayed print actions *)
-val set_delayed_prints : print_action list -> unit
+val set_delayed_prints : delayed_prints -> unit
(** set the delayed print actions *)
val reset_delayed_prints : unit -> unit
diff --git a/infer/src/biabduction/BiabductionSummary.ml b/infer/src/biabduction/BiabductionSummary.ml
index 25b8afb3b..34ffd6f4f 100644
--- a/infer/src/biabduction/BiabductionSummary.ml
+++ b/infer/src/biabduction/BiabductionSummary.ml
@@ -60,7 +60,7 @@ module Jprop = struct
let pp_short pe f jp = Prop.pp_prop pe f (to_prop jp)
(** Dump the toplevel prop *)
- let d_shallow (jp: Prop.normal t) = L.add_print_action (L.PTjprop_short, Obj.repr jp)
+ let d_shallow (jp: Prop.normal t) = L.add_print_with_pe pp_short jp
(** Get identifies of the jprop *)
let get_id = function Prop (n, _) -> n | Joined (n, _, _, _) -> n
@@ -85,7 +85,7 @@ module Jprop = struct
(** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
let d_list ~(shallow: bool) (jplist: Prop.normal t list) =
- L.add_print_action (L.PTjprop_list, Obj.repr (shallow, jplist))
+ L.add_print_with_pe (pp_list ~shallow) jplist
let rec gen_free_vars =
@@ -264,7 +264,9 @@ let pp_spec pe num_opt fmt spec =
(** Dump a spec *)
-let d_spec (spec: 'a spec) = L.add_print_action (L.PTspec, Obj.repr spec)
+let d_spec (spec: 'a spec) =
+ L.add_print (pp_spec (if Config.write_html then Pp.html Blue else Pp.text) None) spec
+
let pp_specs pe fmt specs =
let total = List.length specs in
diff --git a/infer/src/biabduction/BiabductionSummary.mli b/infer/src/biabduction/BiabductionSummary.mli
index a58244912..47d5b252b 100644
--- a/infer/src/biabduction/BiabductionSummary.mli
+++ b/infer/src/biabduction/BiabductionSummary.mli
@@ -37,12 +37,6 @@ module Jprop : sig
val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t
(** map the function to each prop in the jprop, pointwise *)
- val pp_list : Pp.env -> shallow:bool -> Format.formatter -> Prop.normal t list -> unit
- (** Print a list of joined props, the boolean indicates whether to print subcomponents of joined props *)
-
- val pp_short : Pp.env -> Format.formatter -> Prop.normal t -> unit
- (** Print the toplevel prop *)
-
val to_prop : 'a t -> 'a Prop.t
(** Extract the toplevel jprop of a prop *)
end
@@ -70,15 +64,12 @@ end
val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
(** Cast a list of normalized specs to a list of specs *)
-val d_spec : 'a spec -> unit
+val d_spec : _ spec -> unit
(** Dump a spec *)
val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
(** Convert spec into normal form w.r.t. variable renaming *)
-val pp_spec : Pp.env -> (int * int) option -> Format.formatter -> Prop.normal spec -> unit
-(** Print the spec *)
-
type phase = FOOTPRINT | RE_EXECUTION
val equal_phase : phase -> phase -> bool
diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml
index db4d681b2..f21845870 100644
--- a/infer/src/biabduction/Paths.ml
+++ b/infer/src/biabduction/Paths.ml
@@ -453,7 +453,7 @@ end = struct
add_delayed path ; doit 0 fmt path ; print_delayed ()
- let d p = L.add_print_action (L.PTpath, Obj.repr p)
+ let d p = L.add_print pp p
let create_loc_trace path pos_opt : Errlog.loc_trace =
let trace = ref [] in
@@ -593,9 +593,6 @@ module PathSet : sig
val partition : (Prop.normal Prop.t -> bool) -> t -> t * t
(** partition a pathset on the prop component *)
- val pp : Pp.env -> Format.formatter -> t -> unit
- (** pretty print the pathset *)
-
val size : t -> int
(** number of elements in the pathset *)
@@ -705,7 +702,10 @@ end = struct
iter f ps
- let d (ps: t) = L.add_print_action (L.PTpathset, Obj.repr ps)
+ let d (ps: t) =
+ let pp pe fmt ps = F.fprintf fmt "%a@\n" (pp pe) ps in
+ L.add_print_with_pe pp ps
+
(** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the list *)
let from_renamed_list (pl: ('a Prop.t * Path.t) list) : t =
diff --git a/infer/src/biabduction/Paths.mli b/infer/src/biabduction/Paths.mli
index 58d0e3ae5..82887ba04 100644
--- a/infer/src/biabduction/Paths.mli
+++ b/infer/src/biabduction/Paths.mli
@@ -56,9 +56,6 @@ module Path : sig
val join : t -> t -> t
(** join two paths *)
- val pp : Format.formatter -> t -> unit
- (** pretty print a path *)
-
val pp_stats : Format.formatter -> t -> unit
[@@warning "-32"]
(** pretty print statistics of the path *)
@@ -110,9 +107,6 @@ module PathSet : sig
val partition : (Prop.normal Prop.t -> bool) -> t -> t * t
(** partition a pathset on the prop component *)
- val pp : Pp.env -> Format.formatter -> t -> unit
- (** pretty print the pathset *)
-
val size : t -> int
(** number of elements in the pathset *)
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index 145283fca..adfd98ed2 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -153,7 +153,7 @@ let pp_sub pe f = function
(** Dump a substitution. *)
-let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr sub)
+let d_sub (sub: Sil.subst) = L.add_print_with_pe pp_sub sub
let pp_sub_entry pe0 f entry =
let pe, changed = Sil.color_pre_wrapper pe0 f entry in
@@ -175,7 +175,7 @@ let pp_pi pe =
(** Dump a pi. *)
-let d_pi (pi: pi) = L.add_print_action (PTpi, Obj.repr pi)
+let d_pi (pi: pi) = L.add_print_with_pe pp_pi pi
(** Pretty print a sigma. *)
let pp_sigma pe = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe)
@@ -208,7 +208,7 @@ let pp_sigma_simple pe env fmt sigma =
(** Dump a sigma. *)
-let d_sigma (sigma: sigma) = L.add_print_action (PTsigma, Obj.repr sigma)
+let d_sigma (sigma: sigma) = L.add_print_with_pe pp_sigma sigma
(** Dump a pi and a sigma *)
let d_pi_sigma pi sigma =
@@ -345,7 +345,7 @@ let pp_prop pe0 f prop =
let pp_prop_with_typ pe f p = pp_prop {pe with opt= SIM_WITH_TYP} f p
(** Dump a proposition. *)
-let d_prop (prop: 'a t) = L.add_print_action (PTprop, Obj.repr prop)
+let d_prop (prop: 'a t) = L.add_print_with_pe pp_prop prop
(** Print a list of propositions, prepending each one with the given string *)
let pp_proplist_with_typ pe f plist =
@@ -361,7 +361,7 @@ let pp_proplist_with_typ pe f plist =
(** dump a proplist *)
-let d_proplist_with_typ (pl: 'a t list) = L.add_print_action (PTprop_list_with_typ, Obj.repr pl)
+let d_proplist_with_typ (pl: 'a t list) = L.add_print_with_pe pp_proplist_with_typ pl
(** {1 Functions for computing free non-program variables} *)
diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli
index 514b8c4c1..712b2415b 100644
--- a/infer/src/biabduction/Prop.mli
+++ b/infer/src/biabduction/Prop.mli
@@ -49,9 +49,6 @@ val compare_prop : 'a t -> 'a t -> int
val equal_sigma : sigma -> sigma -> bool
(** Check the equality of two sigma's *)
-val pp_sub : Pp.env -> Format.formatter -> subst -> unit
-(** Pretty print a substitution. *)
-
val d_sub : subst -> unit
(** Dump a substitution. *)
@@ -61,9 +58,6 @@ val pp_pi : Pp.env -> Format.formatter -> pi -> unit
val d_pi : pi -> unit
(** Dump a pi. *)
-val pp_sigma : Pp.env -> Format.formatter -> sigma -> unit
-(** Pretty print a sigma. *)
-
val d_sigma : sigma -> unit
(** Dump a sigma. *)
@@ -80,18 +74,12 @@ val prop_update_obj_sub : Pp.env -> 'a t -> Pp.env
val pp_prop : Pp.env -> Format.formatter -> 'a t -> unit
(** Pretty print a proposition. *)
-val pp_prop_with_typ : Pp.env -> Format.formatter -> normal t -> unit
-(** Pretty print a proposition with type information *)
-
val prop_pred_env : 'a t -> Sil.Predicates.env
(** Create a predicate environment for a prop *)
val d_prop : 'a t -> unit
(** Dump a proposition. *)
-val pp_proplist_with_typ : Pp.env -> Format.formatter -> normal t list -> unit
-(** Pretty print a list propositions with type information *)
-
val d_proplist_with_typ : 'a t list -> unit
val pi_free_vars : pi -> Ident.t Sequence.t
diff --git a/infer/src/biabduction/Propgraph.ml b/infer/src/biabduction/Propgraph.ml
index 718e2b29c..0927e782e 100644
--- a/infer/src/biabduction/Propgraph.ml
+++ b/infer/src/biabduction/Propgraph.ml
@@ -262,4 +262,5 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
(** dump a propset *)
let d_proplist (p: 'a Prop.t) (pl: 'b Prop.t list) =
- L.add_print_action (L.PTproplist, Obj.repr (p, pl))
+ let pp pe = pp_proplist pe "PROP" (p, false) in
+ L.add_print_with_pe pp pl