diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 690eba396..3f68ac130 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -296,47 +296,27 @@ module Node = struct F.pp_print_string fmt "UnaryOperator" - (** Print extended instructions for the node, - highlighting the given subinstruction if present *) - 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 - in - let instrs = get_instrs node in - Instrs.pp pe fmt instrs - else - let () = - match get_kind node with - | Stmt_node s -> - F.fprintf fmt "statements (%a)" pp_stmt s - | Prune_node (_, _, descr) -> - F.fprintf fmt "assume %s" descr - | Exit_node -> - F.pp_print_string fmt "exit" - | Skip_node s -> - F.fprintf fmt "skip (%s)" s - | Start_node -> - F.pp_print_string fmt "start" - | Join_node -> - F.pp_print_string fmt "join" - in - F.fprintf fmt " %a " Location.pp (get_loc node) - + let pp_instrs ~highlight pe0 f node = + let pe = + match highlight with + | None -> + pe0 + | Some instr -> + Pp.extend_colormap pe0 (Obj.repr instr) Red + in + Instrs.pp pe f (get_instrs node) - (** Dump extended instructions for the node *) - let d_instrs ~(sub_instrs : bool) (curr_instr : Sil.instr option) (node : t) = - L.d_pp_with_pe ~color:Pp.Green (pp_instrs ~sub_instrs ~instro:curr_instr) node + let d_instrs ~highlight (node : t) = L.d_pp_with_pe ~color:Green (pp_instrs ~highlight) node (** Return a description of the cfg node *) let get_description pe node = - let str = + let str_kind = match get_kind node with | Stmt_node _ -> "Instructions" | Prune_node (_, _, descr) -> - "Conditional" ^ " " ^ descr + "Conditional " ^ descr | Exit_node -> "Exit" | Skip_node _ -> @@ -346,8 +326,7 @@ module Node = struct | Join_node -> "Join" in - let pp fmt = F.fprintf fmt "%s@.%a" str (pp_instrs pe ~instro:None ~sub_instrs:true) node in - F.asprintf "%t" pp + F.asprintf "%s@\n%a" str_kind (Instrs.pp pe) (get_instrs node) (** simple key for a node: just look at the instructions *) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index e41060b04..1ef6d787f 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -93,8 +93,8 @@ module Node : sig val append_instrs : t -> Sil.instr list -> unit (** Append the instructions to the list of instructions to execute *) - val d_instrs : sub_instrs:bool -> Sil.instr option -> t -> unit - (** Dump extended instructions for the node *) + val d_instrs : highlight:Sil.instr option -> t -> unit + (** Dump instructions for the node, highlighting the given subinstruction if present *) val dummy : Typ.Procname.t -> t (** Create a dummy node *) @@ -154,11 +154,6 @@ module Node : sig val pp_stmt : Format.formatter -> stmt_nodekind -> 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 *) - val compute_key : t -> NodeKey.t end diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 0530bd4ce..905c6bb52 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -181,8 +181,8 @@ 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) ~instro:None ~sub_instrs:true) - node Io_infer.Html.pp_end_color () ; + (Instrs.pp (Pp.html Green)) + (Procdesc.Node.get_instrs 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) ((node_id :> int), session, loc.Location.line) diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 9467eb7f2..7a3459a07 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -421,7 +421,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = | None -> () ) ; L.d_strln "SIL INSTR:" ; - Procdesc.Node.d_instrs ~sub_instrs:true (State.get_instr ()) curr_node ; + Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ; L.d_ln () ; Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; State.mark_instr_fail exn @@ -447,7 +447,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = L.d_increase_indent () ; Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ; L.d_strln ".... Instructions: ...." ; - Procdesc.Node.d_instrs ~sub_instrs:true (State.get_instr ()) curr_node ; + Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ; L.d_ln () ; L.d_ln () in