[debug] Get rid of proof_cover/isproof

Reviewed By: jberdine

Differential Revision: D10376563

fbshipit-source-id: 783c4a78e

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 =
+      let style_class = if not isvisited then "dangling" else "visited" in
-        if not isvisited then "dangling" else if isproof then "visitedproof" else "visited"
-      in
       F.asprintf
         "<span class='%s'>%s_%d<span class='expansion'>node%d preds:%a succs:%a exn:%a \
          %s%s</span></span>"

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

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<div class=\"msg\" style=\"margin-left:9ex\">%s</div>" 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 "<center><h1>File %a </h1></center>@\n<table class=\"code\">@\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 "<tr><td class=\"num\" id=\"LINE%d\">%d</td><td class=\"line\">%s " line_number
       line_number line_html ;
-    Pp.seq
+    Pp.seq (pp_node_link [fname_encoding] ~description:true) fmt nodes_at_linenum ;
-      (pp_node_link [fname_encoding] ~proof_cover:!proof_cover ~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 table_nodes_at_linenum global_err_log) procs ;
-  List.iter ~f:(write_html_proc filename proof_cover 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 "</table>@\n" ;