diff --git a/infer/src/IR/Io_infer.ml b/infer/src/IR/Io_infer.ml index 342dff345..c25915019 100644 --- a/infer/src/IR/Io_infer.ml +++ b/infer/src/IR/Io_infer.ml @@ -52,8 +52,6 @@ h1 { font-size:14pt } .expansion { display: none; } .visited:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 } .visited { color: darkmagenta; background-color:LemonChiffon; position: relative } -.visitedproof:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 } -.visitedproof { color: darkmagenta; background-color:lightgreen; position: relative } .dangling:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 } .dangling { color: gray; background-color:white; position: relative } .num { width:2.5em; padding-right:2ex; background-color:#eeeeee } @@ -142,13 +140,11 @@ td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2e let node_filename pname id = F.sprintf "%s_node%d" (Typ.Procname.to_filename pname) id (** Print an html link to the given node. *) - let pp_node_link path_to_root pname ~description ~preds ~succs ~exn ~isvisited ~isproof fmt id = + let pp_node_link path_to_root pname ~description ~preds ~succs ~exn ~isvisited fmt id = let node_fname = node_filename pname id in let node_text = let descr = if String.equal description "" then "N" else String.prefix description 1 in - let style_class = - if not isvisited then "dangling" else if isproof then "visitedproof" else "visited" - in + let style_class = if not isvisited then "dangling" else "visited" in F.asprintf "%s_%dnode%d preds:%a succs:%a exn:%a \ %s%s" diff --git a/infer/src/IR/Io_infer.mli b/infer/src/IR/Io_infer.mli index 30b5c7680..558864bce 100644 --- a/infer/src/IR/Io_infer.mli +++ b/infer/src/IR/Io_infer.mli @@ -51,7 +51,6 @@ module Html : sig -> succs:int list -> exn:int list -> isvisited:bool - -> isproof:bool -> Format.formatter -> int -> unit diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 971b5d595..87f2eb5b5 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -78,24 +78,17 @@ let is_visited node = Summary.Stats.is_visited stats node_id -let pp_node_link path_to_root ?proof_cover ~description fmt node = +let pp_node_link path_to_root ~description fmt node = let description = if description then Procdesc.Node.get_description (Pp.html Black) node else "" in - let isproof = - match proof_cover with - | Some proof_cover -> - BiabductionSummary.Visitedset.mem (Procdesc.Node.get_id node, []) proof_cover - | None -> - false - in Io_infer.Html.pp_node_link path_to_root (Procdesc.Node.get_proc_name node) ~description ~preds:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) ~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) ~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) - ~isvisited:(is_visited node) ~isproof fmt + ~isvisited:(is_visited node) fmt (Procdesc.Node.get_id node :> int) @@ -256,7 +249,7 @@ let pp_err_message fmt err_string = F.fprintf fmt "\n
%s
" err_string -let write_html_proc source proof_cover table_nodes_at_linenum global_err_log proc_desc = +let write_html_proc source table_nodes_at_linenum global_err_log proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let process_node n = let lnum = (Procdesc.Node.get_loc n).Location.line in @@ -280,11 +273,6 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro | None -> () | Some summary -> - List.iter - ~f:(fun sp -> - proof_cover := - BiabductionSummary.Visitedset.union sp.BiabductionSummary.visited !proof_cover ) - (Tabulation.get_specs_from_payload summary) ; Errlog.update global_err_log (Summary.get_err_log summary) ) @@ -298,7 +286,7 @@ let write_html_file linereader filename procs = F.fprintf fmt "

File %a

@\n@\n" SourceFile.pp filename in - let print_one_line proof_cover table_nodes_at_linenum table_err_per_line line_number = + let print_one_line table_nodes_at_linenum table_err_per_line line_number = let line_html = match LineReader.from_file_linenum linereader filename line_number with | Some line_raw -> @@ -317,9 +305,7 @@ let write_html_file linereader filename procs = in F.fprintf fmt "
%d%s " line_number line_number line_html ; - Pp.seq - (pp_node_link [fname_encoding] ~proof_cover:!proof_cover ~description:true) - fmt nodes_at_linenum ; + Pp.seq (pp_node_link [fname_encoding] ~description:true) fmt nodes_at_linenum ; List.iter ~f:(fun n -> match Procdesc.Node.get_kind n with @@ -348,14 +334,13 @@ let write_html_file linereader filename procs = pp_prelude () ; let global_err_log = Errlog.empty () in let table_nodes_at_linenum = Hashtbl.create 11 in - let proof_cover = ref BiabductionSummary.Visitedset.empty in - List.iter ~f:(write_html_proc filename proof_cover table_nodes_at_linenum global_err_log) procs ; + List.iter ~f:(write_html_proc filename table_nodes_at_linenum global_err_log) procs ; let table_err_per_line = create_table_err_per_line global_err_log in let linenum = ref 0 in try while true do incr linenum ; - print_one_line proof_cover table_nodes_at_linenum table_err_per_line !linenum + print_one_line table_nodes_at_linenum table_err_per_line !linenum done with End_of_file -> F.fprintf fmt "
@\n" ;