diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index 8b3f1e2be..0b0515298 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -35,7 +35,6 @@ let analyze_exe_env exe_env => { L.log_progress_file (); Specs.clear_spec_tbl (); Random.self_init (); - let line_reader = Printer.LineReader.create (); if Config.checkers { /* run the checkers only */ let call_graph = Exe_env.get_cg exe_env; @@ -43,7 +42,7 @@ let analyze_exe_env exe_env => { } else { /* run the full analysis */ Interproc.do_analysis exe_env; - Printer.write_all_html_files line_reader exe_env; + Printer.write_all_html_files exe_env; Interproc.print_stats exe_env; let elapsed = Unix.gettimeofday () -. init_time; L.out "Interprocedural footprint analysis terminated in %f sec@." elapsed diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index a5bc9f22f..d60c9559f 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -445,41 +445,41 @@ let create_table_err_per_line err_log = let create_err_message err_string = "\n
" ^ err_string ^ "
" -(** Create filename.ext.html. *) -let write_html_file linereader filename cfg = +let write_html_proc proof_cover table_nodes_at_linenum global_err_log proc_desc = + let proc_name = Cfg.Procdesc.get_proc_name proc_desc in let process_node nodes_tbl n = let lnum = (Cfg.Node.get_loc n).Location.line in let curr_nodes = try Hashtbl.find nodes_tbl lnum with Not_found -> [] in Hashtbl.replace nodes_tbl lnum (n:: curr_nodes) in - let fname_encoding = - DB.source_file_encoding filename in - let (fd, fmt) = - Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in - let do_proc proof_cover table_nodes_at_linenum global_err_log proc_name proc_desc = - let proc_loc = (Cfg.Procdesc.get_loc proc_desc) in - let process_proc = - Cfg.Procdesc.is_defined proc_desc && - DB.source_file_equal proc_loc.Location.file !DB.current_source && - match AttributesTable.file_defining_procedure proc_name with - | None -> true - | Some source_file -> - DB.source_file_equal source_file (Cfg.Procdesc.get_loc proc_desc).file in - if process_proc then - begin - IList.iter (process_node table_nodes_at_linenum) (Cfg.Procdesc.get_nodes proc_desc); - match Specs.get_summary proc_name with - | None -> - () - | Some summary -> - IList.iter - (fun sp -> - proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover) - (Specs.get_specs_from_payload summary); - Errlog.update global_err_log summary.Specs.attributes.ProcAttributes.err_log - end in + let proc_loc = Cfg.Procdesc.get_loc proc_desc in + let process_proc = + Cfg.Procdesc.is_defined proc_desc && + DB.source_file_equal proc_loc.Location.file !DB.current_source && + match AttributesTable.file_defining_procedure proc_name with + | None -> true + | Some source_file -> + DB.source_file_equal source_file (Cfg.Procdesc.get_loc proc_desc).file in + if process_proc then + begin + IList.iter (process_node table_nodes_at_linenum) (Cfg.Procdesc.get_nodes proc_desc); + match Specs.get_summary proc_name with + | None -> + () + | Some summary -> + IList.iter + (fun sp -> + proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover) + (Specs.get_specs_from_payload summary); + Errlog.update global_err_log summary.Specs.attributes.ProcAttributes.err_log + end +(** Create filename.ext.html. *) +let write_html_file linereader filename procs = + DB.current_source := filename; + let fname_encoding = DB.source_file_encoding filename in + let (fd, fmt) = Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in let pp_prelude () = let s = "

File " ^ @@ -487,7 +487,6 @@ let write_html_file linereader filename cfg = "

\n" ^ "\n" in F.fprintf fmt "%s" s in - let print_one_line proof_cover table_nodes_at_linenum table_err_per_line line_number = let line_html = match LineReader.from_file_linenum linereader !DB.current_source line_number with @@ -553,7 +552,7 @@ let write_html_file linereader filename cfg = let global_err_log = Errlog.empty () in let table_nodes_at_linenum = Hashtbl.create 11 in let proof_cover = ref Specs.Visitedset.empty in - Cfg.iter_proc_desc cfg (do_proc proof_cover table_nodes_at_linenum global_err_log); + IList.iter (write_html_proc 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 @@ -568,8 +567,9 @@ let write_html_file linereader filename cfg = Io_infer.Html.close (fd, fmt)) (** Create filename.ext.html for each file in the exe_env. *) -let write_all_html_files linereader exe_env = +let write_all_html_files exe_env = if Config.write_html then + let linereader = LineReader.create () in Exe_env.iter_files (fun _ cfg -> let source_files_in_cfg = @@ -583,7 +583,6 @@ let write_all_html_files linereader exe_env = !files in DB.SourceFileSet.iter (fun file -> - DB.current_source := file; - write_html_file linereader file cfg) + write_html_file linereader file (Cfg.get_all_procs cfg)) source_files_in_cfg) exe_env diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index c37a7772d..ed444ed6b 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -49,5 +49,7 @@ val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit The boolean indicates whether to print whole seconds only. *) val write_proc_html : bool -> Cfg.Procdesc.t -> unit +val write_html_file : LineReader.t -> DB.source_file -> Cfg.Procdesc.t list -> unit + (** Create filename.ext.html for each file in the exe_env. *) -val write_all_html_files : LineReader.t -> Exe_env.t -> unit +val write_all_html_files : Exe_env.t -> unit