Clean up code to produce html pages of analysis results in debug mode.

Reviewed By: akotulski

Differential Revision: D3041115

fb-gh-sync-id: 6f86cf5
shipit-source-id: 6f86cf5

infer/src/backend/cfg.ml

@@ -24,18 +24,41 @@ module Node = struct
     | Skip_node of string
 
   and t = { (** a node *)
-    nd_id : int; (** unique id of the node *)
-    mutable nd_dist_exit : int option; (** distance to the exit node *)
-    mutable nd_temps : Ident.t list; (** temporary variables *)
-    mutable nd_dead_pvars_after : Sil.pvar list; (** dead program variables after executing the instructions *)
-    mutable nd_dead_pvars_before : Sil.pvar list; (** dead program variables before executing the instructions *)
-    mutable nd_exn : t list; (** exception nodes in the cfg *)
-    mutable nd_instrs : Sil.instr list; (** instructions for symbolic execution *)
-    mutable nd_kind : nodekind; (** kind of node *)
-    mutable nd_loc : Location.t; (** location in the source code *)
-    mutable nd_preds : t list; (** predecessor nodes in the cfg *)
-    mutable nd_proc : proc_desc option; (** proc desc from cil *)
-    mutable nd_succs : t list; (** successor nodes in the cfg *)
+    (** unique id of the node *)
+    nd_id : int;
+
+    (** distance to the exit node *)
+    mutable nd_dist_exit : int option;
+
+    (** temporary variables *)
+    mutable nd_temps : Ident.t list;
+
+    (** dead program variables after executing the instructions *)
+    mutable nd_dead_pvars_after : Sil.pvar list;
+
+    (** dead program variables before executing the instructions *)
+    mutable nd_dead_pvars_before : Sil.pvar list;
+
+    (** exception nodes in the cfg *)
+    mutable nd_exn : t list;
+
+    (** instructions for symbolic execution *)
+    mutable nd_instrs : Sil.instr list;
+
+    (** kind of node *)
+    mutable nd_kind : nodekind;
+
+    (** location in the source code *)
+    mutable nd_loc : Location.t;
+
+    (** predecessor nodes in the cfg *)
+    mutable nd_preds : t list;
+
+    (** proc desc from cil *)
+    mutable nd_proc : proc_desc option;
+
+    (** successor nodes in the cfg *)
+    mutable nd_succs : t list;
   }
   and proc_desc = { (** procedure description *)
     pd_attributes : ProcAttributes.t; (** attributes of the procedure *)
@@ -482,14 +505,17 @@ module Node = struct
     proc_desc.pd_attributes.ProcAttributes.locals <-
       proc_desc.pd_attributes.ProcAttributes.locals @ new_locals
 
-  (** Print extended instructions for the node, highlighting the given subinstruction if present *)
-  let pp_instr pe0 ~sub_instrs instro fmt node =
+  (** Print extended instructions for the node,
+      highlighting the given subinstruction if present *)
+  let pp_instrs pe0 ~sub_instrs instro fmt node =
     let pe = match instro with
       | None -> pe0
       | Some instr -> pe_extend_colormap pe0 (Obj.repr instr) Red in
     let instrs = get_instrs node in
-    let pp_loc fmt () = F.fprintf fmt " %a " Location.pp (get_loc node) in
-    let print_sub_instrs () = F.fprintf fmt "%a" (Sil.pp_instr_list pe) instrs in
+    let pp_loc fmt () =
+      F.fprintf fmt " %a " Location.pp (get_loc node) in
+    let print_sub_instrs () =
+      F.fprintf fmt "%a" (Sil.pp_instr_list pe) instrs in
     match get_kind node with
     | Stmt_node s ->
         if sub_instrs then print_sub_instrs ()
@@ -530,7 +556,10 @@ module Node = struct
           "Start"
       | Join_node ->
           "Join" in
-    let pp fmt () = F.fprintf fmt "%s\n%a@?" str (pp_instr pe None ~sub_instrs: true) node in
+    let pp fmt () =
+      F.fprintf fmt "%s\n%a@?"
+        str
+        (pp_instrs pe None ~sub_instrs: true) node in
     pp_to_string pp ()
 
   let proc_desc_iter_nodes f proc_desc =

infer/src/backend/cfg.mli

@@ -234,13 +234,16 @@ module Node : sig
   (** Pretty print the node *)
   val pp : Format.formatter -> t -> unit
 
-  (** Print extended instructions for the node, highlighting the given subinstruction if present *)
-  val pp_instr : printenv -> sub_instrs: bool -> Sil.instr option -> Format.formatter -> t -> unit
+  (** Print extended instructions for the node,
+      highlighting the given subinstruction if present *)
+  val pp_instrs :
+    printenv -> sub_instrs: bool -> Sil.instr option -> Format.formatter -> t -> unit
 
   (** Replace the instructions to be executed. *)
   val replace_instrs : t -> Sil.instr list -> unit
 
-  (** Set the (after/before) dead program variables. After/before indicated with the true/false flag. *)
+  (** Set the (after/before) dead program variables.
+      After/before indicated with the true/false flag. *)
   val set_dead_pvars : t -> bool -> Sil.pvar list -> unit
 
   (** Set the node kind *)

infer/src/backend/inferanalyze.ml

@@ -230,15 +230,17 @@ let analyze_exe_env exe_env =
   Specs.clear_spec_tbl ();
   Random.self_init ();
   let line_reader = Printer.LineReader.create () in
-  if !checkers then (* run the checkers only *)
+  if !checkers then
     begin
+      (** run the checkers only *)
       let call_graph = Exe_env.get_cg exe_env in
       Callbacks.iterate_callbacks Checkers.ST.store_summary call_graph exe_env
     end
   else
-    begin (* run the full analysis *)
+    begin
+      (** run the full analysis *)
       Interproc.do_analysis exe_env;
-      Printer.c_files_write_html line_reader exe_env;
+      Printer.write_all_html_files line_reader exe_env;
       Interproc.print_stats exe_env;
       let elapsed = Unix.gettimeofday () -. init_time in
       L.out "Interprocedural footprint analysis terminated in %f sec@." elapsed

infer/src/backend/interproc.ml

@@ -24,13 +24,22 @@ type visitednode =
 module NodeVisitSet =
   Set.Make(struct
     type t = visitednode
-    let compare_ids n1 n2 = Cfg.Node.compare n2 n1 (* higher id is better *)
-    let compare_distance_to_exit { node = n1 } { node = n2 } = (* smaller means higher priority *)
-      let n = match Cfg.Node.get_distance_to_exit n1, Cfg.Node.get_distance_to_exit n2 with
-        | None, None -> 0
-        | None, Some _ -> 1
-        | Some _, None -> - 1
-        | Some d1, Some d2 -> int_compare d1 d2 (* shorter distance to exit is better *) in
+    let compare_ids n1 n2 =
+      (* higher id is better *)
+      Cfg.Node.compare n2 n1
+    let compare_distance_to_exit { node = n1 } { node = n2 } =
+      (* smaller means higher priority *)
+      let n =
+        match Cfg.Node.get_distance_to_exit n1, Cfg.Node.get_distance_to_exit n2 with
+        | None, None ->
+            0
+        | None, Some _ ->
+            1
+        | Some _, None ->
+            - 1
+        | Some d1, Some d2 ->
+            (* shorter distance to exit is better *)
+            int_compare d1 d2 in
       if n <> 0 then n else compare_ids n1 n2
     let compare_number_of_visits x1 x2 =
       let n = int_compare x1.visits x2.visits in (* visited fewer times is better *)
@@ -193,7 +202,8 @@ let do_meet_pre pset =
   else
     Propset.to_proplist pset
 
-(** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *)
+(** Find the preconditions in the current spec table,
+    apply meet then join, and return the joined preconditions *)
 let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
   let collect_do_abstract_one tenv prop =
     if !Config.footprint
@@ -241,9 +251,11 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
 (* =============== START of symbolic execution =============== *)
 
 (** propagate a set of results to the given node *)
-let propagate (wl : Worklist.t) pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
+let propagate
+    (wl : Worklist.t) pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
   let edgeset_todo =
-    let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *)
+    (** prop must be a renamed prop by the invariant preserved by PropSet *)
+    let f prop path edgeset_curr =
       let exn_opt =
         if is_exception
         then Some (Tabulation.prop_get_exn_name pname prop)
@@ -334,9 +346,10 @@ let do_before_node session node =
   State.set_node node;
   State.set_session session;
   L.reset_delayed_prints ();
-  Printer.start_session node loc proc_name session
+  Printer.node_start_session node loc proc_name session
 
-let do_after_node node = Printer.finish_session node
+let do_after_node node =
+  Printer.node_finish_session node
 
 (** Return the list of normal ids occurring in the instructions *)
 let instrs_get_normal_vars instrs =
@@ -393,8 +406,12 @@ let check_assignement_guard node =
       let leti = IList.filter is_letderef_instr ins in
       match pi, leti with
       | [Sil.Prune (Sil.Var(e1), _, _, _)], [Sil.Letderef(e2, e', _, _)]
-      | [Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var(e1), _), _, _, _)], [Sil.Letderef(e2, e', _, _)] when (Ident.equal e1 e2) ->
-          if verbose then L.d_strln ("Found "^(Sil.exp_to_string e')^" as prune var");
+      | [Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var(e1), _), _, _, _)],
+        [Sil.Letderef(e2, e', _, _)]
+        when (Ident.equal e1 e2) ->
+          if verbose
+          then
+            L.d_strln ("Found " ^ (Sil.exp_to_string e') ^ " as prune var");
           [e']
       | _ -> [] in
     let prune_vars = IList.flatten(IList.map (fun n -> prune_var n) succs) in
@@ -415,7 +432,8 @@ let check_assignement_guard node =
                     " nLOC: " ^ (string_of_int l.Location.nLOC));
            L.d_strln " ");
         Location.equal l l_node) succs_loc in
-  let succs_have_simple_guards () = (* check that the guards of the succs are a var or its negation *)
+  (* check that the guards of the succs are a var or its negation *)
+  let succs_have_simple_guards () =
     let check_instr = function
       | Sil.Prune (Sil.Var _, _, _, _) -> true
       | Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var _, _), _, _, _) -> true
@@ -430,13 +448,17 @@ let check_assignement_guard node =
      succs_have_simple_guards () then
     (let instr = Cfg.Node.get_instrs node in
      match succs_loc with
-     | loc_succ:: _ -> (* at this point all successors are at the same location, so we can take the first*)
+     (* at this point all successors are at the same location, so we can take the first*)
+     | loc_succ:: _ ->
          let set_instr_at_succs_loc =
            IList.filter
-             (fun i -> (Location.equal (Sil.instr_get_loc i) loc_succ) && is_set_instr i)
+             (fun i ->
+                Location.equal (Sil.instr_get_loc i) loc_succ &&
+                is_set_instr i)
              instr in
          (match set_instr_at_succs_loc with
-          | [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*)
+          | [Sil.Set(e, _, _, _)] ->
+              (* we now check if e is the same expression used to prune*)
               if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) then (
                 let desc = Errdesc.explain_condition_is_assignment l_node in
                 let exn = Exceptions.Condition_is_assignment (desc, __POS__) in
@@ -444,8 +466,10 @@ let check_assignement_guard node =
                 Reporting.log_warning pname ~loc: (Some l_node) ~pre: pre_opt exn
               )
               else ()
-          | _ -> ())
-     | _ -> if verbose then L.d_strln "NOT FOUND loc_succ"
+          | _ ->
+              ())
+     | _ ->
+         if verbose then L.d_strln "NOT FOUND loc_succ"
     ) else ()
 
 (** Perform symbolic execution for a node starting from an initial prop *)
@@ -453,10 +477,12 @@ let do_symbolic_execution handle_exn tenv
     (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) =
   let pdesc = Cfg.Node.get_proc_desc node in
   State.mark_execution_start node;
-  State.set_const_map (ConstantPropagation.build_const_map pdesc); (* build the const map lazily *)
+  (* build the const map lazily *)
+  State.set_const_map (ConstantPropagation.build_const_map pdesc);
   check_assignement_guard node;
   let instrs = Cfg.Node.get_instrs node in
-  Ident.update_name_generator (instrs_get_normal_vars instrs); (* fresh normal vars must be fresh w.r.t. instructions *)
+  (* fresh normal vars must be fresh w.r.t. instructions *)
+  Ident.update_name_generator (instrs_get_normal_vars instrs);
   let pset =
     SymExec.lifted_sym_exec handle_exn tenv pdesc
       (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in
@@ -518,7 +544,8 @@ let forward_tabulate tenv wl =
         f prop path !cnt ps_size in
       Paths.PathSet.iter exe pathset in
     let log_string proc_name =
-      let phase_string = (if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE") in
+      let phase_string =
+        if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE" in
       let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
       let timestamp = Specs.get_timestamp summary in
       F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in
@@ -616,15 +643,20 @@ let report_context_leaks pname sigma tenv =
       sigma in
   IList.iter
     (function
-      | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) when Sil.pvar_is_global pv ->
+      | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _)
+        when Sil.pvar_is_global pv ->
           IList.iter
             (fun (f_name, f_strexp) ->
-               if not (Harness.is_generated_field f_name) then
-                 check_reachable_context_from_fld (f_name, f_strexp) context_exps) static_flds
+               if not (Harness.is_generated_field f_name)
+               then
+                 check_reachable_context_from_fld
+                   (f_name, f_strexp) context_exps)
+            static_flds
       | _ -> ())
     sigma
 
-(** remove locals and formals, and check if the address of a stack variable is left in the result *)
+(** Remove locals and formals,
+    and check if the address of a stack variable is left in the result *)
 let remove_locals_formals_and_check pdesc p =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let pvars, p' = Cfg.remove_locals_formals pdesc p in
@@ -637,17 +669,23 @@ let remove_locals_formals_and_check pdesc p =
   IList.iter check_pvar pvars;
   p'
 
-(* Collect the analysis results for the exit node *)
+(** Collect the analysis results for the exit node. *)
 let collect_analysis_result wl pdesc : Paths.PathSet.t =
   let exit_node = Cfg.Procdesc.get_exit_node pdesc in
   let exit_node_id = Cfg.Node.get_id exit_node in
   let pathset = htable_retrieve wl.Worklist.path_set_visited exit_node_id in
   Paths.PathSet.map (remove_locals_formals_and_check pdesc) pathset
 
-module Pmap = Map.Make (struct type t = Prop.normal Prop.t let compare = Prop.prop_compare end)
+module Pmap = Map.Make
+    (struct
+      type t = Prop.normal Prop.t
+      let compare = Prop.prop_compare
+    end)
 
 let vset_ref_add_path vset_ref path =
-  Paths.Path.iter_all_nodes_nocalls (fun n -> vset_ref := Cfg.NodeSet.add n !vset_ref) path
+  Paths.Path.iter_all_nodes_nocalls
+    (fun n -> vset_ref := Cfg.NodeSet.add n !vset_ref)
+    path
 
 let vset_ref_add_pathset vset_ref pathset =
   Paths.PathSet.iter (fun _ path -> vset_ref_add_path vset_ref path) pathset
@@ -659,7 +697,9 @@ let compute_visited vset =
     let instrs_loc = IList.map Sil.instr_get_loc (Cfg.Node.get_instrs n) in
     let lines = IList.map (fun loc -> loc.Location.line) (node_loc :: instrs_loc) in
     IList.remove_duplicates int_compare (IList.sort int_compare lines) in
-  let do_node n = res := Specs.Visitedset.add (Cfg.Node.get_id n, node_get_all_lines n) !res in
+  let do_node n =
+    res :=
+      Specs.Visitedset.add (Cfg.Node.get_id n, node_get_all_lines n) !res in
   Cfg.NodeSet.iter do_node vset;
   !res
 
@@ -668,8 +708,13 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let sub =
     let fav = Sil.fav_new () in
-    Paths.PathSet.iter (fun prop _ -> Prop.prop_fav_add fav prop) pathset;
-    let sub_list = IList.map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.knormal)))) (Sil.fav_to_list fav) in
+    Paths.PathSet.iter
+      (fun prop _ -> Prop.prop_fav_add fav prop)
+      pathset;
+    let sub_list =
+      IList.map
+        (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.knormal))))
+        (Sil.fav_to_list fav) in
     Sil.sub_of_list sub_list in
   let pre_post_visited_list =
     let pplist = Paths.PathSet.elements pathset in
@@ -678,7 +723,8 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
       let prop'' = Abs.abstract pname tenv prop' in
       let pre, post = Prop.extract_spec prop'' in
       let pre' = Prop.normalize (Prop.prop_sub sub pre) in
-      if !Config.curr_language = Config.Java && Cfg.Procdesc.get_access pdesc <> Sil.Private then
+      if !Config.curr_language =
+         Config.Java && Cfg.Procdesc.get_access pdesc <> Sil.Private then
         report_context_leaks pname (Prop.get_sigma post) tenv;
       let post' =
         if Prover.check_inconsistency_base prop then None
@@ -691,7 +737,10 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
     IList.map f pplist in
   let pre_post_map =
     let add map (pre, post, visited) =
-      let current_posts, current_visited = try Pmap.find pre map with Not_found -> (Paths.PathSet.empty, Specs.Visitedset.empty) in
+      let current_posts, current_visited =
+        try Pmap.find pre map
+        with Not_found ->
+          (Paths.PathSet.empty, Specs.Visitedset.empty) in
       let new_posts = match post with
         | None -> current_posts
         | Some (post, path) -> Paths.PathSet.add_renamed_prop post path current_posts in
@@ -715,7 +764,8 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
 let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let pathset = collect_analysis_result wl pdesc in
-  L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####");
+  L.d_strln
+    ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####");
   Propset.d Prop.prop_emp (Paths.PathSet.to_propset pathset);
   L.d_ln ();
   let res =
@@ -725,13 +775,17 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
       let visited =
         let vset_ref = ref Cfg.NodeSet.empty in
         vset_ref_add_pathset vset_ref pathset;
-        vset_ref_add_pathset vset_ref pathset_diverging; (* nodes from diverging states were also visited *)
+        (* nodes from diverging states were also visited *)
+        vset_ref_add_pathset vset_ref pathset_diverging;
         compute_visited !vset_ref in
       do_join_post pname tenv pathset, visited with
     | exn when (match exn with Exceptions.Leak _ -> true | _ -> false) ->
         raise (Failure "Leak in post collecion") in
-  L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Postconditions after join ####");
-  L.d_increase_indent 1; Propset.d Prop.prop_emp (Paths.PathSet.to_propset (fst res)); L.d_decrease_indent 1;
+  L.d_strln
+    ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Postconditions after join ####");
+  L.d_increase_indent 1;
+  Propset.d Prop.prop_emp (Paths.PathSet.to_propset (fst res));
+  L.d_decrease_indent 1;
   L.d_ln ();
   res
 
@@ -755,31 +809,35 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
       Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in
     IList.map do_formal new_formals in
   let sigma_seed =
-    create_seed_vars (Prop.get_sigma prop @ sigma_new_formals) (* formals already there plus new ones *) in
+    create_seed_vars
+      (* formals already there plus new ones *)
+      (Prop.get_sigma prop @ sigma_new_formals) in
   let sigma = sigma_seed @ sigma_new_formals in
   let new_pi =
-    let pi = Prop.get_pi prop in
-    pi
-    (* inactive until it becomes necessary, as it pollutes props
-       let fav_ids = Sil.fav_to_list (Prop.sigma_fav sigma_locals) in
-       let mk_undef_atom id = Prop.mk_neq (Sil.Var id) (Sil.Const (Sil.Cattribute (Sil.Aundef "UNINITIALIZED"))) in
-       let pi_undef = IList.map mk_undef_atom fav_ids in
-       pi_undef @ pi *) in
+    Prop.get_pi prop in
   let prop' =
     Prop.replace_pi new_pi (Prop.prop_sigma_star prop sigma) in
-  Prop.replace_sigma_footprint (Prop.get_sigma_footprint prop' @ sigma_new_formals) prop'
+  Prop.replace_sigma_footprint
+    (Prop.get_sigma_footprint prop' @ sigma_new_formals)
+    prop'
 
 (** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true
     as well as seed variables *)
-let initial_prop tenv (curr_f: Cfg.Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t =
+let initial_prop
+    tenv (curr_f: Cfg.Procdesc.t) (prop : 'a Prop.t) add_formals
+  : Prop.normal Prop.t =
   let construct_decl (x, typ) =
     (Sil.mk_pvar x (Cfg.Procdesc.get_proc_name curr_f), typ) in
   let new_formals =
     if add_formals
     then IList.map construct_decl (Cfg.Procdesc.get_formals curr_f)
     else [] in (** no new formals added *)
-  let prop1 = Prop.prop_reset_inst (fun inst_old -> Sil.update_inst inst_old Sil.inst_formal) prop in
-  let prop2 = prop_init_formals_seed tenv new_formals prop1 in
+  let prop1 =
+    Prop.prop_reset_inst
+      (fun inst_old -> Sil.update_inst inst_old Sil.inst_formal)
+      prop in
+  let prop2 =
+    prop_init_formals_seed tenv new_formals prop1 in
   Prop.prop_rename_primed_footprint_vars (Prop.normalize prop2)
 
 (** Construct an initial prop from the empty prop *)
@@ -790,10 +848,16 @@ let initial_prop_from_emp tenv curr_f =
 let initial_prop_from_pre tenv curr_f pre =
   if !Config.footprint then
     let vars = Sil.fav_to_list (Prop.prop_fav pre) in
-    let sub_list = IList.map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.kfootprint)))) vars in
+    let sub_list =
+      IList.map
+        (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.kfootprint))))
+        vars in
     let sub = Sil.sub_of_list sub_list in
     let pre2 = Prop.prop_sub sub pre in
-    let pre3 = Prop.replace_sigma_footprint (Prop.get_sigma pre2) (Prop.replace_pi_footprint (Prop.get_pure pre2) pre2) in
+    let pre3 =
+      Prop.replace_sigma_footprint
+        (Prop.get_sigma pre2)
+        (Prop.replace_pi_footprint (Prop.get_pure pre2) pre2) in
     initial_prop tenv curr_f pre3 false
   else
     initial_prop tenv curr_f pre false
@@ -807,8 +871,13 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
   L.d_indent 1;
   L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
   L.d_ln (); L.d_ln ();
-  let init_prop = initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in
-  let init_edgeset = Paths.PathSet.add_renamed_prop init_prop (Paths.Path.start init_node) Paths.PathSet.empty in
+  let init_prop =
+    initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in
+  let init_edgeset =
+    Paths.PathSet.add_renamed_prop
+      init_prop
+      (Paths.Path.start init_node)
+      Paths.PathSet.empty in
   do_after_node init_node;
   try
     Worklist.add wl init_node;
@@ -821,7 +890,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
     L.d_ln ();
     let posts, visited =
       let pset, visited = collect_postconditions wl tenv pdesc in
-      let plist = IList.map (fun (p, path) -> (Cfg.remove_seed_vars p, path)) (Paths.PathSet.elements pset) in
+      let plist =
+        IList.map
+          (fun (p, path) -> (Cfg.remove_seed_vars p, path))
+          (Paths.PathSet.elements pset) in
       plist, visited in
     let pre =
       let p = Cfg.remove_locals_ret pdesc (Specs.Jprop.to_prop precondition) in
@@ -846,14 +918,21 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
 
 (** get all the nodes in the current call graph with their defined children *)
 let get_procs_and_defined_children call_graph =
-  IList.map (fun (n, ns) -> (n, Procname.Set.elements ns)) (Cg.get_nodes_and_defined_children call_graph)
+  IList.map
+    (fun (n, ns) ->
+       (n, Procname.Set.elements ns))
+    (Cg.get_nodes_and_defined_children call_graph)
 
 let pp_intra_stats wl proc_desc fmt _ =
   let nstates = ref 0 in
   let nodes = Cfg.Procdesc.get_nodes proc_desc in
-  IList.iter (fun node ->
-      nstates := !nstates + Paths.PathSet.size
-                   (htable_retrieve wl.Worklist.path_set_visited (Cfg.Node.get_id node))) nodes;
+  IList.iter
+    (fun node ->
+       nstates :=
+         !nstates +
+         Paths.PathSet.size
+           (htable_retrieve wl.Worklist.path_set_visited (Cfg.Node.get_id node)))
+    nodes;
   F.fprintf fmt "(%d nodes containing %d states)" (IList.length nodes) !nstates
 
 (** Return functions to perform one phase of the analysis for a procedure.
@@ -877,9 +956,11 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
   let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
     let go (wl : Worklist.t) () =
       let init_prop = initial_prop_from_emp tenv pdesc in
-      let init_props_from_pres = (* use existing pre's (in recursion some might exist) as starting points *)
+      (* use existing pre's (in recursion some might exist) as starting points *)
+      let init_props_from_pres =
         let specs = Specs.get_specs pname in
-        let mk_init precondition = (* rename spec vars to footrpint vars, and copy current to footprint *)
+        (* rename spec vars to footrpint vars, and copy current to footprint *)
+        let mk_init precondition =
           initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in
         IList.map (fun spec -> mk_init spec.Specs.pre) specs in
       let init_props = Propset.from_proplist (init_prop :: init_props_from_pres) in
@@ -894,7 +975,10 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
       L.d_decrease_indent 1;
       check_recursion_level ();
       Worklist.add wl start_node;
-      Config.arc_mode := Hashtbl.mem (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag;
+      Config.arc_mode :=
+        Hashtbl.mem
+          (Cfg.Procdesc.get_flags pdesc)
+          Mleak_buckets.objc_arc_flag;
       ignore (path_set_put_todo wl start_node init_edgeset);
       forward_tabulate tenv wl in
     let get_results (wl : Worklist.t) () =
@@ -921,7 +1005,10 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
 
   let re_execution proc_name
     : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
-    let candidate_preconditions = IList.map (fun spec -> spec.Specs.pre) (Specs.get_specs proc_name) in
+    let candidate_preconditions =
+      IList.map
+        (fun spec -> spec.Specs.pre)
+        (Specs.get_specs proc_name) in
     let valid_specs = ref [] in
     let go () =
       L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name;
@@ -948,8 +1035,12 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
       let specs = !valid_specs in
       L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp proc_name;
       L.out "#### Finished: Re-Execution for %a ####@." Procname.pp proc_name;
-      let valid_preconditions = IList.map (fun spec -> spec.Specs.pre) specs in
-      let filename = DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(Procname.to_filename proc_name)] in
+      let valid_preconditions =
+        IList.map (fun spec -> spec.Specs.pre) specs in
+      let filename =
+        DB.Results_dir.path_to_filename
+          DB.Results_dir.Abs_source_dir
+          [(Procname.to_filename proc_name)] in
       if !Config.write_dotty then
         Dotty.pp_speclist_dotty_file filename specs;
       L.out "@.@.================================================";
@@ -1103,7 +1194,8 @@ let update_specs proc_name phase (new_specs : Specs.NormSpec.t list)
               new_specs)
     then begin
       changed:= true;
-      L.out "Specs changed: removing pre of spec@\n%a@." (Specs.pp_spec pe_text None) old_spec;
+      L.out "Specs changed: removing pre of spec@\n%a@."
+        (Specs.pp_spec pe_text None) old_spec;
       current_specs := SpecMap.remove old_spec.Specs.pre !current_specs end
     else () in
   let add_spec spec = (* add a new spec by doing union of the posts *)
@@ -1125,7 +1217,8 @@ let update_specs proc_name phase (new_specs : Specs.NormSpec.t list)
 
     with Not_found ->
       changed := true;
-      L.out "Specs changed: added new pre@\n%a@." (Specs.Jprop.pp_short pe_text) spec.Specs.pre;
+      L.out "Specs changed: added new pre@\n%a@."
+        (Specs.Jprop.pp_short pe_text) spec.Specs.pre;
       current_specs :=
         SpecMap.add
           spec.Specs.pre
@@ -1225,9 +1318,11 @@ let transition_footprint_re_exe proc_name joined_pres =
     the procedures enabled after the analysis of [proc_name] *)
 let perform_transition exe_env tenv proc_name =
   let transition () =
-    let joined_pres = (* disable exceptions for leaks and protect against any other errors *)
+    (* disable exceptions for leaks and protect against any other errors *)
+    let joined_pres =
       let allowleak = !Config.allowleak in
-      let apply_start_node f = (* apply the start node to f, and do nothing in case of exception *)
+      (* apply the start node to f, and do nothing in case of exception *)
+      let apply_start_node f =
         try
           match Exe_env.get_proc_desc exe_env proc_name with
           | Some pdesc ->
@@ -1355,10 +1450,14 @@ let visited_and_total_nodes cfg =
     | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> true
     | Cfg.Node.Skip_node _ | Cfg.Node.Join_node -> false in
   let counted_nodes = Cfg.NodeSet.filter filter_node all_nodes in
-  let visited_nodes_re = Cfg.NodeSet.filter (fun node -> snd (Printer.is_visited_phase node)) counted_nodes in
+  let visited_nodes_re =
+    Cfg.NodeSet.filter
+      (fun node -> snd (Printer.node_is_visited node))
+      counted_nodes in
   Cfg.NodeSet.elements visited_nodes_re, Cfg.NodeSet.elements counted_nodes
 
-(** Print the stats for the given cfg; consider every defined proc unless a proc with the same name
+(** Print the stats for the given cfg.
+    Consider every defined proc unless a proc with the same name
     was defined in another module, and was the one which was analyzed *)
 let print_stats_cfg proc_shadowed cfg =
   let err_table = Errlog.create_err_table () in
@@ -1380,7 +1479,8 @@ let print_stats_cfg proc_shadowed cfg =
     let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
     if proc_shadowed proc_desc ||
        Specs.get_summary proc_name = None then
-      L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name
+      L.out "print_stats: ignoring function %a which is also defined in another file@."
+        Procname.pp proc_name
     else
       let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in
       let stats = summary.Specs.stats in

infer/src/backend/io_infer.ml

@@ -13,113 +13,145 @@
 module F = Format
 
 (* =============== START of module Html =============== *)
-module Html : sig
-  val close : Unix.file_descr * Format.formatter -> unit (** Close an Html file *)
-  val create : DB.Results_dir.path_kind -> DB.Results_dir.path -> Unix.file_descr * Format.formatter (** Create a new html file *)
-  val modified_during_analysis : DB.Results_dir.path -> bool (** Return true if the html file was modified since the beginning of the analysis *)
-  val open_out : DB.Results_dir.path -> Unix.file_descr * Format.formatter (** Open an Html file to append data *)
-  val pp_line_link : ?with_name: bool -> ?text: (string option) -> DB.Results_dir.path -> Format.formatter -> int -> unit (** Print an html link to the given line number of the current source file *)
-  val pp_hline : Format.formatter -> unit -> unit (** Print a horizontal line *)
-  val pp_end_color : Format.formatter -> unit -> unit (** Print end color *)
-
-  (** [pp_node_link path_to_root description isvisited isproof fmt id] prints an html link to the given node.
-      [path_to_root] is the path to the dir for the procedure in the spec db.
-      [description] is a string description.
-      [is_visited] indicates whether the node should be active or greyed out.
-      [is_proof] indicates whether the node is part of a proof and should be green.
-      [id] is the node identifier. *)
-  val pp_node_link : DB.Results_dir.path -> string -> int list -> int list -> int list -> bool -> bool -> Format.formatter -> int -> unit
-  val pp_proc_link : DB.Results_dir.path -> Procname.t -> Format.formatter -> string -> unit (** Print an html link to the given proc *)
-  val pp_session_link : ?with_name: bool -> string list -> Format.formatter -> int * int * int -> unit (** Print an html link given node id and session *)
-  val pp_start_color : Format.formatter -> color -> unit (** Print start color *)
-end = struct
+module Html =
+struct
+  (** Create a new html file *)
   let create pk path =
     let fname, dir_path = match IList.rev path with
-      | fname:: dir_path -> fname, dir_path
-      | [] -> raise (Failure "Html.create") in
-    let fd = DB.Results_dir.create_file pk (IList.rev ((fname ^ ".html") :: dir_path)) in
+      | fname :: path_rev ->
+          fname, IList.rev ((fname ^ ".html") :: path_rev)
+      | [] ->
+          raise (Failure "Html.create") in
+    let fd = DB.Results_dir.create_file pk dir_path in
     let outc = Unix.out_channel_of_descr fd in
     let fmt = F.formatter_of_out_channel outc in
-    let (++) x y = x ^ "\n" ^ y in
     let s =
-      "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\">" ++
-      "<html>\n<head>\n<title>" ^ fname ^ "</title>" ++
-                                          "<style type=\"text/css\">" ++
-                                          "body { color:#000000; background-color:#ffffff }" ++
-                                          "body { font-family:Helvetica, sans-serif; font-size:10pt }" ++
-                                          "h1 { font-size:14pt }" ++
-                                          ".code { border-collapse:collapse; width:100%; }" ++
-                                          ".code { font-family: \"Andale Mono\", monospace; font-size:10pt }" ++
-                                          ".code { line-height: 1.2em }" ++
-                                          ".comment { color: green; font-style: oblique }" ++
-                                          ".keyword { color: blue }" ++
-                                          ".string_literal { color: red }" ++
-                                          ".color_black { color: black }" ++
-                                          ".color_blue { color: blue }" ++
-                                          ".color_green { color: green }" ++
-                                          ".color_red { color: red }" ++
-                                          ".color_orange { color: orange }" ++
-                                          ".directive { color: darkmagenta }" ++
-                                          ".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 }" ++
-                                          ".num { text-align:right; font-size: smaller }" ++
-                                          ".num { color:#444444 }" ++
-                                          ".line { padding-left: 1ex; border-left: 3px solid #ccc }" ++
-                                          ".line { white-space: pre }" ++
-                                          ".msg { background-color:#fff8b4; color:#000000 }" ++
-                                          ".msg { -webkit-box-shadow:1px 1px 7px #000 }" ++
-                                          ".msg { -webkit-border-radius:5px }" ++
-                                          ".msg { font-family:Helvetica, sans-serif; font-size: smaller }" ++
-                                          ".msg { font-weight: bold }" ++
-                                          ".msg { float:left }" ++
-                                          ".msg { padding:0.5em 1ex 0.5em 1ex }" ++
-                                          ".msg { margin-top:10px; margin-bottom:10px }" ++
-                                          ".msg { max-width:60em; word-wrap: break-word; white-space: pre-wrap;}" ++
-                                          ".mrange { background-color:#dfddf3 }" ++
-                                          ".mrange { border-bottom:1px solid #6F9DBE }" ++
-                                          ".PathIndex { font-weight: bold }" ++
-                                          "table.simpletable {" ++
-                                          "padding: 5px;" ++
-                                          "font-size:12pt;" ++
-                                          "margin:20px;" ++
-                                          "border-collapse: collapse; border-spacing: 0px;" ++
-                                          "}" ++
-                                          "td.rowname {" ++
-                                          "text-align:right; font-weight:bold; color:#444444;" ++
-                                          "padding-right:2ex; }" ++
-                                          "</style>" ++
-                                          "</head>" ++
-                                          "<body" ^ ">" ++
-                                                    "" in
+      "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\">\n\
+       <html>\n\
+       <head>\n\
+       <title>" ^
+      fname ^
+      "</title>\n\
+       <style type=\"text/css\">\n\
+       body { color:#000000; background-color:#ffffff }\n\
+       body { font-family:Helvetica, sans-serif; font-size:10pt }\n\
+       h1 { font-size:14pt }\n\
+       .code { border-collapse:collapse; width:100%; }\n\
+       .code { font-family: \"Andale Mono\", monospace; font-size:10pt }\n\
+       .code { line-height: 1.2em }\n\
+       .comment { color: green; font-style: oblique }\n\
+       .keyword { color: blue }\n\
+       .string_literal { color: red }\n\
+       .color_black { color: black }\n\
+       .color_blue { color: blue }\n\
+       .color_green { color: green }\n\
+       .color_red { color: red }\n\
+       .color_orange { color: orange }\n\
+       .directive { color: darkmagenta }\n\
+       .expansion { display: none; }\n\
+       .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 }\n\
+       .visited {\
+       color: darkmagenta;\
+       background-color:LemonChiffon;\
+       position: relative }\n\
+       .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 }\n\
+       .visitedproof {\
+       color: darkmagenta;\
+       background-color:lightgreen;\
+       position: relative }\n\
+       .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 }\n\
+       .dangling { color: gray; background-color:white; position: relative }\n\
+       .num { width:2.5em; padding-right:2ex; background-color:#eeeeee }\n\
+       .num { text-align:right; font-size: smaller }\n\
+       .num { color:#444444 }\n\
+       .line { padding-left: 1ex; border-left: 3px solid #ccc }\n\
+       .line { white-space: pre }\n\
+       .msg { background-color:#fff8b4; color:#000000 }\n\
+       .msg { -webkit-box-shadow:1px 1px 7px #000 }\n\
+       .msg { -webkit-border-radius:5px }\n\
+       .msg { font-family:Helvetica, sans-serif; font-size: smaller }\n\
+       .msg { font-weight: bold }\n\
+       .msg { float:left }\n\
+       .msg { padding:0.5em 1ex 0.5em 1ex }\n\
+       .msg { margin-top:10px; margin-bottom:10px }\n\
+       .msg { max-width:60em; word-wrap: break-word; white-space: pre-wrap;}\n\
+       .mrange { background-color:#dfddf3 }\n\
+       .mrange { border-bottom:1px solid #6F9DBE }\n\
+       .PathIndex { font-weight: bold }\n\
+       table.simpletable { padding: 5px; font-size:12pt; margin:20px; border-collapse: collapse;\
+       border-spacing: 0px; }\n\
+       td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2ex; }\n\
+       </style>\n\
+       </head>\
+       \n\
+       <body>\
+       \n" in
     F.fprintf fmt "%s" s;
     (fd, fmt)
 
-  (** get the full html filename from a path *)
+  (** Get the full html filename from a path *)
   let get_full_fname path =
-    let fname, dir_path = match IList.rev path with
-      | fname:: dir_path -> fname, dir_path
-      | [] -> raise (Failure "Html.open_out") in
-    DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir (IList.rev ((fname ^ ".html") :: dir_path))
+    let dir_path = match IList.rev path with
+      | fname :: path_rev ->
+          IList.rev ((fname ^ ".html") :: path_rev)
+      | [] ->
+          raise (Failure "Html.open_out") in
+    DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir dir_path
 
+  (** Open an Html file to append data *)
   let open_out path =
     let full_fname = get_full_fname path in
-    let fd = Unix.openfile (DB.filename_to_string full_fname) [Unix.O_WRONLY; Unix.O_APPEND] 0o777 in
+    let fd =
+      Unix.openfile
+        (DB.filename_to_string full_fname)
+        [Unix.O_WRONLY; Unix.O_APPEND]
+        0o777 in
     let outc = Unix.out_channel_of_descr fd in
     let fmt = F.formatter_of_out_channel outc in
     (fd, fmt)
 
+  (** Return true if the html file was modified since the beginning of the analysis *)
   let modified_during_analysis path =
     let fname = get_full_fname path in
     if DB.file_exists fname then
       DB.file_modified_time fname >= initial_analysis_time
     else false
 
+  (** Close an Html file *)
   let close (fd, fmt) =
     F.fprintf fmt "</body>@\n</html>@.";
     Unix.close fd
@@ -136,58 +168,86 @@ end = struct
   let pp_end_color fmt () =
     F.fprintf fmt "%s" "</span>"
 
-  let pp_link ?(name = None) ?(pos = None) path fmt text =
+  let pp_link ?(name = None) ?(pos = None) ~path fmt text =
     let pos_str = match pos with
       | None -> ""
       | Some s -> "#" ^ s in
-    let link_str = (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Rel path)) ^ ".html" ^ pos_str in
+    let link_str =
+      (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Rel path))
+      ^ ".html"
+      ^ pos_str in
     let name_str = match name with
       | None -> ""
       | Some n -> "name=\"" ^ n ^ "\"" in
     let pr_str = "<a " ^ name_str ^ "href=\"" ^ link_str ^ "\">" ^ text ^ "</a>" in
     F.fprintf fmt " %s" pr_str
 
-  (** [pp_node_link path_to_root description isvisited isproof fmt id] prints an html link to the given node. *)
+  (** [pp_node_link path_to_root description isvisited isproof fmt id]
+      prints an html link to the given node. *)
   let pp_node_link path_to_root description preds succs exn isvisited isproof fmt id =
     let display_name =
-      (if description = "" then "N" else String.sub description 0 1) ^ "_" ^ (string_of_int id) in
+      (if description = "" then "N" else String.sub description 0 1)
+      ^ "_"
+      ^ (string_of_int id) in
     let node_name = "node" ^ string_of_int id 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 if isproof then "visitedproof" else "visited" in
     let node_text =
       let pp fmt () =
-        Format.fprintf fmt "<span class='%s'>%s<span class='expansion'>node%d preds:%a succs:%a exn:%a %s%s</span></span>"
+        Format.fprintf fmt
+          "<span class='%s'>%s\
+           <span class='expansion'>\
+           node%d preds:%a succs:%a exn:%a %s%s\
+           </span>\
+           </span>"
           style_class display_name id
-          (pp_seq Format.pp_print_int) preds (pp_seq Format.pp_print_int) succs (pp_seq Format.pp_print_int) exn
-          description (if not isvisited then "\nNOT VISITED" else "") in
+          (pp_seq Format.pp_print_int) preds
+          (pp_seq Format.pp_print_int) succs
+          (pp_seq Format.pp_print_int) exn
+          description
+          (if not isvisited then "\nNOT VISITED" else "") in
       pp_to_string pp () in
-    if not isvisited then F.fprintf fmt " %s" node_text
-    else pp_link (path_to_root @ ["nodes"; node_name]) fmt node_text
+    if not isvisited
+    then F.fprintf fmt " %s" node_text
+    else pp_link ~path: (path_to_root @ ["nodes"; node_name]) fmt node_text
 
   (** Print an html link to the given proc *)
   let pp_proc_link path_to_root proc_name fmt text =
-    pp_link (path_to_root @ [Procname.to_filename proc_name]) fmt text
+    pp_link ~path: (path_to_root @ [Procname.to_filename proc_name]) fmt text
 
   (** Print an html link to the given line number of the current source file *)
   let pp_line_link ?(with_name = false) ?(text = None) path_to_root fmt linenum =
     let fname = DB.source_file_encoding !DB.current_source in
     let linenum_str = string_of_int linenum in
     let name = "LINE" ^ linenum_str in
-    pp_link ~name: (if with_name then Some name else None) (path_to_root @ [".."; fname]) ~pos: (Some name)
-      fmt (match text with Some s -> s | None -> linenum_str)
+    pp_link
+      ~name: (if with_name then Some name else None)
+      ~pos: (Some name)
+      ~path: (path_to_root @ [".."; fname])
+      fmt
+      (match text with Some s -> s | None -> linenum_str)
 
   (** Print an html link given node id and session *)
   let pp_session_link ?(with_name = false) path_to_root fmt (node_id, session, linenum) =
     let node_name = "node" ^ (string_of_int node_id) in
     let path_to_node = path_to_root @ ["nodes"; node_name] in
     let pos = "session" ^ (string_of_int session) in
-    pp_link ~name: (if with_name then Some pos else None) ~pos: (Some pos) path_to_node fmt (node_name ^ "#" ^ pos);
+    pp_link
+      ~name: (if with_name then Some pos else None)
+      ~pos: (Some pos)
+      ~path: path_to_node
+      fmt
+      (node_name ^ "#" ^ pos);
     F.fprintf fmt "(%a)" (pp_line_link path_to_root) linenum
 end
 (* =============== END of module Html =============== *)
 
 (* =============== START of module Xml =============== *)
 (** Create and print xml trees *)
-module Xml = struct
+module Xml =
+struct
   let tag_branch = "branch"
   let tag_call_trace = "call_trace"
   let tag_callee = "callee"
@@ -252,10 +312,20 @@ module Xml = struct
         let indent' = if newline = "" then "" else indent ^ "  " in
         let space = if attributes = [] then "" else " " in
         let pp_inside fmt () = match forest with
-          | [] -> ()
-          | [String s] -> pp fmt "%s" s
-          | _ -> pp fmt "%s%a%s" newline (pp_forest newline indent') forest indent in
-        pp fmt "%s<%s%s%a>%a</%s>%s" indent name space pp_attributes attributes pp_inside () name newline
+          | [] ->
+              ()
+          | [String s] ->
+              pp fmt "%s" s
+          | _ ->
+              pp fmt "%s%a%s" newline (pp_forest newline indent') forest indent in
+        pp fmt "%s<%s%s%a>%a</%s>%s"
+          indent
+          name
+          space
+          pp_attributes attributes
+          pp_inside ()
+          name
+          newline
     | String s ->
         F.fprintf fmt "%s%s%s" indent s newline
   and pp_forest newline indent fmt forest =

infer/src/backend/ondemand.ml

@@ -101,7 +101,7 @@ let save_global_state () =
     current_source = !DB.current_source;
     delayed_prints = L.get_delayed_prints ();
     footprint_mode = !Config.footprint;
-    html_formatter = !Printer.html_formatter;
+    html_formatter = !Printer.curr_html_formatter;
     name_generator = Ident.NameGenerator.get_current ();
     symexec_state = State.save_state ();
   }
@@ -112,7 +112,7 @@ let restore_global_state st =
   DB.current_source := st.current_source;
   L.set_delayed_prints st.delayed_prints;
   Config.footprint := st.footprint_mode;
-  Printer.html_formatter := st.html_formatter;
+  Printer.curr_html_formatter := st.html_formatter;
   Ident.NameGenerator.set_current st.name_generator;
   State.restore_state st.symexec_state;
   Timeout.resume_previous_timeout ()
@@ -157,7 +157,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
         timestamp = summary.Specs.timestamp + 1 } in
     Specs.add_summary callee_pname summary';
     Checkers.ST.store_summary callee_pname;
-    Printer.proc_write_log false callee_pdesc in
+    Printer.write_proc_html false callee_pdesc in
 
   let log_error_and_continue exn kind =
     Reporting.log_error callee_pname exn;

infer/src/backend/printer.ml

@@ -13,30 +13,92 @@
 module L = Logging
 module F = Format
 
-(** return true if the node was visited during footprint and during re-execution*)
-let is_visited_phase node =
+(** Module to read specific lines from files.
+    The data from any file will stay in memory until the handle is collected by the gc. *)
+module LineReader =
+struct
+  (** Map a file name to an array of string, one for each line in the file. *)
+  type t = (DB.source_file, string array) Hashtbl.t
+
+  let create () =
+    Hashtbl.create 1
+
+  let read_file fname =
+    let cin = open_in fname in
+    let lines = ref [] in
+    try
+      while true do
+        let line_raw = input_line cin in
+        let line =
+          let len = String.length line_raw in
+          if len > 0 && String.get line_raw (len -1) = '\013' then
+            String.sub line_raw 0 (len -1)
+          else line_raw in
+        lines := line :: !lines
+      done;
+      assert false (* execution never reaches here *)
+    with End_of_file ->
+      (close_in cin;
+       Array.of_list (IList.rev !lines))
+
+  let file_data (hash: t) fname =
+    try
+      Some (Hashtbl.find hash fname)
+    with Not_found ->
+    try
+      let lines_arr = read_file (DB.source_file_to_string fname) in
+      Hashtbl.add hash fname lines_arr;
+      Some lines_arr
+    with exn when exn_not_failure exn -> None
+
+  let from_file_linenum_original hash fname linenum =
+    match file_data hash fname with
+    | None -> None
+    | Some lines_arr ->
+        if linenum > 0 && linenum <= Array.length lines_arr
+        then Some lines_arr.(linenum -1)
+        else None
+
+  let from_file_linenum hash fname linenum =
+    let fname_in_resdir =
+      DB.source_file_in_resdir fname in
+    let sourcefile_in_resdir =
+      DB.abs_source_file_from_path (DB.filename_to_string fname_in_resdir) in
+    from_file_linenum_original hash sourcefile_in_resdir linenum
+
+  let from_loc hash loc =
+    from_file_linenum hash loc.Location.file loc.Location.line
+end
+
+
+(** Current formatter for the html output *)
+let curr_html_formatter = ref F.std_formatter
+
+(** Return true if the node was visited during footprint and during re-execution*)
+let node_is_visited node =
   let proc_desc = Cfg.Node.get_proc_desc node in
   let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
   match Specs.get_summary proc_name with
-  | None -> false, false
+  | None ->
+      false, false
   | Some summary ->
       let stats = summary.Specs.stats in
-      let is_visited_fp = IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in
-      let is_visited_re = IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in
+      let is_visited_fp =
+        IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in
+      let is_visited_re =
+        IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in
       is_visited_fp, is_visited_re
 
-(** return true if the node was visited during analysis *)
+(** Return true if the node was visited during analysis *)
 let is_visited node =
-  let visited_fp, visited_re = is_visited_phase node in
+  let visited_fp, visited_re = node_is_visited node in
   visited_fp || visited_re
 
-(** current formatter for the html output *)
-let html_formatter = ref F.std_formatter
-
-(* =============== START of module Log_nodes =============== *)
+(* =============== START of module NodesHtml =============== *)
 
-(** Print information when starting and finishing the processing of a node *)
-module Log_nodes : sig
+(** Print information into html files for nodes
+    when starting and finishing the processing of a node *)
+module NodesHtml : sig
   val start_node :
     int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> bool
   val finish_node : int -> unit
@@ -53,7 +115,7 @@ end = struct
         (false, Io_infer.Html.open_out ["nodes"; node_fname])
       else
         (true, Io_infer.Html.create DB.Results_dir.Abs_source_dir ["nodes"; node_fname]) in
-    html_formatter := fmt;
+    curr_html_formatter := fmt;
     Hashtbl.replace log_files (node_fname, !DB.current_source) fd;
     if needs_initialization then
       (F.fprintf fmt "<center><h1>Cfg Node %a</h1></center>"
@@ -71,13 +133,15 @@ end = struct
              (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
              (is_visited node) false fmt (Cfg.Node.get_id node)) preds;
        F.fprintf fmt "<br>SUCCS: @\n";
-       IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] ""
+       IList.iter (fun node ->
+           Io_infer.Html.pp_node_link [".."] ""
              (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node))
              (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node))
              (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
              (is_visited node) false fmt (Cfg.Node.get_id node)) succs;
        F.fprintf fmt "<br>EXN: @\n";
-       IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] ""
+       IList.iter (fun node ->
+           Io_infer.Html.pp_node_link [".."] ""
              (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node))
              (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node))
              (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
@@ -92,13 +156,16 @@ end = struct
     let fname = id_to_fname nodeid in
     let fd = Hashtbl.find log_files (fname, !DB.current_source) in
     Unix.close fd;
-    html_formatter := F.std_formatter
+    curr_html_formatter := F.std_formatter
 end
-(* =============== END of module Log_nodes =============== *)
+(* =============== END of module NodesHtml =============== *)
 
-(** printing functions *)
+(* =============== Printing functions =============== *)
+
+(** Execute the delayed print actions *)
 let force_delayed_print fmt =
-  let pe_default = if !Config.write_html then pe_html Black else pe_text in
+  let pe_default =
+    if !Config.write_html then pe_html Black else pe_text in
   function
   | (L.PTatom, a) ->
       let (a: Sil.atom) = Obj.obj a in
@@ -122,12 +189,24 @@ let force_delayed_print fmt =
       F.fprintf fmt "%s@[" !s
   | (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 Green (Sil.pp_instr (pe_html Green)) i Io_infer.Html.pp_end_color ()
-      else Sil.pp_instr pe_text fmt i
+      if !Config.write_html
+      then
+        F.fprintf fmt "%a%a%a"
+          Io_infer.Html.pp_start_color Green
+          (Sil.pp_instr (pe_html Green)) i
+          Io_infer.Html.pp_end_color ()
+      else
+        Sil.pp_instr pe_text fmt i
   | (L.PTinstr_list, il) ->
       let (il: Sil.instr list) = Obj.obj il in
-      if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Sil.pp_instr_list (pe_html Green)) il Io_infer.Html.pp_end_color ()
-      else Sil.pp_instr_list pe_text fmt il
+      if !Config.write_html
+      then
+        F.fprintf fmt "%a%a%a"
+          Io_infer.Html.pp_start_color Green
+          (Sil.pp_instr_list (pe_html Green)) il
+          Io_infer.Html.pp_end_color ()
+      else
+        Sil.pp_instr_list pe_text fmt il
   | (L.PTjprop_list, shallow_jpl) ->
       let ((shallow: bool), (jpl: Prop.normal Specs.Jprop.t list)) = Obj.obj shallow_jpl in
       Specs.Jprop.pp_list pe_default shallow fmt jpl
@@ -139,8 +218,15 @@ let force_delayed_print fmt =
       Location.pp fmt loc
   | (L.PTnode_instrs, b_n) ->
       let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in
-      if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) io ~sub_instrs: b) n Io_infer.Html.pp_end_color ()
-      else F.fprintf fmt "%a" (Cfg.Node.pp_instr pe_text io ~sub_instrs: b) n
+      if !Config.write_html
+      then
+        F.fprintf fmt "%a%a%a"
+          Io_infer.Html.pp_start_color Green
+          (Cfg.Node.pp_instrs (pe_html Green) io ~sub_instrs: b) n
+          Io_infer.Html.pp_end_color ()
+      else
+        F.fprintf fmt "%a"
+          (Cfg.Node.pp_instrs pe_text io ~sub_instrs: b) n
   | (L.PToff, off) ->
       let (off: Sil.offset) = Obj.obj off in
       Sil.pp_offset pe_default fmt off
@@ -182,21 +268,35 @@ let force_delayed_print fmt =
       Prop.pp_sigma pe_default fmt sigma
   | (L.PTspec, spec) ->
       let (spec: Prop.normal Specs.spec) = Obj.obj spec in
-      Specs.pp_spec (if !Config.write_html then pe_html Blue else pe_text) None fmt spec
+      Specs.pp_spec
+        (if !Config.write_html then pe_html Blue else pe_text)
+        None fmt spec
   | (L.PTstr, s) ->
       let (s: string) = Obj.obj s in
       F.fprintf fmt "%s" s
   | (L.PTstr_color, s) ->
       let (s: string), (c: 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.fprintf fmt "%s" s
+      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.fprintf fmt "%s" 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: 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
+      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
@@ -211,54 +311,86 @@ let force_delayed_print fmt =
       (pp_seq (Sil.pp_typ 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 Red s Io_infer.Html.pp_end_color ()
-      else F.fprintf fmt "ERROR: %s" s
+      if !Config.write_html
+      then
+        F.fprintf fmt "%aERROR: %s%a"
+          Io_infer.Html.pp_start_color 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 Orange s Io_infer.Html.pp_end_color ()
-      else F.fprintf fmt "WARNING: %s" s
+      if !Config.write_html
+      then
+        F.fprintf fmt "%aWARNING: %s%a"
+          Io_infer.Html.pp_start_color 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 Blue s Io_infer.Html.pp_end_color ()
-      else F.fprintf fmt "INFO: %s" s
+      if !Config.write_html
+      then
+        F.fprintf fmt "%aINFO: %s%a"
+          Io_infer.Html.pp_start_color 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 *)
+(** 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 !html_formatter "@?"; (* flush html stream *)
-  IList.iter (force_delayed_print !html_formatter) (IList.rev (L.get_delayed_prints ()));
-  F.fprintf !html_formatter "@?";
+  F.fprintf !curr_html_formatter "@?"; (* flush html stream *)
+  IList.iter
+    (force_delayed_print !curr_html_formatter)
+    (IList.rev (L.get_delayed_prints ()));
+  F.fprintf !curr_html_formatter "@?";
   L.reset_delayed_prints ();
   Config.forcing_delayed_prints := false
 
 (** Start a session, and create a new html fine for the node if it does not exist yet *)
-let _start_session node (loc: Location.t) proc_name session =
+let start_session node (loc: Location.t) proc_name session =
   let node_id = Cfg.Node.get_id node in
-  (if Log_nodes.start_node node_id loc proc_name (Cfg.Node.get_preds node) (Cfg.Node.get_succs node) (Cfg.Node.get_exn node)
-   then F.fprintf !html_formatter "%a@[<v>%a@]%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) None ~sub_instrs: true) node Io_infer.Html.pp_end_color ());
-  F.fprintf !html_formatter "%a%a"
+  (if NodesHtml.start_node
+      node_id loc proc_name
+      (Cfg.Node.get_preds node)
+      (Cfg.Node.get_succs node)
+      (Cfg.Node.get_exn node)
+   then
+     F.fprintf !curr_html_formatter "%a<LISTING>%a</LISTING>%a"
+       Io_infer.Html.pp_start_color Green
+       (Cfg.Node.pp_instrs (pe_html Green) None ~sub_instrs: true) node
+       Io_infer.Html.pp_end_color ());
+  F.fprintf !curr_html_formatter "%a%a"
     Io_infer.Html.pp_hline ()
     (Io_infer.Html.pp_session_link ~with_name: true [".."])
     (node_id, session, loc.Location.line);
-  F.fprintf !html_formatter "<LISTING>%a" Io_infer.Html.pp_start_color Black
+  F.fprintf !curr_html_formatter "<LISTING>%a"
+    Io_infer.Html.pp_start_color Black
 
-let start_session node loc proc_name session =
-  if !Config.write_html then _start_session node loc proc_name session
+let node_start_session node loc proc_name session =
+  if !Config.write_html then
+    start_session node loc proc_name session
 
 (** Finish a session, and perform delayed print actions if required *)
-let finish_session node =
+let node_finish_session node =
   if !Config.test == false then force_delayed_prints ()
   else L.reset_delayed_prints ();
   if !Config.write_html then begin
-    F.fprintf !html_formatter "</LISTING>%a" Io_infer.Html.pp_end_color ();
-    Log_nodes.finish_node (Cfg.Node.get_id node)
+    F.fprintf !curr_html_formatter "</LISTING>%a"
+      Io_infer.Html.pp_end_color ();
+    NodesHtml.finish_node (Cfg.Node.get_id node)
   end
 
-(** Write log file for the proc *)
-let proc_write_log whole_seconds pdesc =
+(** Write html file for the procedure.
+    The boolean indicates whether to print whole seconds only *)
+let write_proc_html whole_seconds pdesc =
   if !Config.write_html then
     begin
       let pname = Cfg.Procdesc.get_proc_name pdesc in
@@ -267,10 +399,13 @@ let proc_write_log whole_seconds pdesc =
       let fd, fmt =
         Io_infer.Html.create DB.Results_dir.Abs_source_dir [Procname.to_filename pname] in
       F.fprintf fmt "<center><h1>Procedure %a</h1></center>@\n"
-        (Io_infer.Html.pp_line_link ~text: (Some (Escape.escape_xml (Procname.to_string pname))) [])
+        (Io_infer.Html.pp_line_link
+           ~text: (Some (Escape.escape_xml (Procname.to_string pname)))
+           [])
         linenum;
       IList.iter
-        (fun n -> Io_infer.Html.pp_node_link []
+        (fun n ->
+           Io_infer.Html.pp_node_link []
              (Cfg.Node.get_description (pe_html Black) n)
              (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n))
              (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n))
@@ -278,17 +413,21 @@ let proc_write_log whole_seconds pdesc =
              (is_visited n) false fmt (Cfg.Node.get_id n))
         nodes;
       (match Specs.get_summary pname with
-       | None -> ()
+       | None ->
+           ()
        | Some summary ->
            Specs.pp_summary (pe_html Black) whole_seconds fmt summary;
            Io_infer.Html.close (fd, fmt))
     end
 
 (** Creare a hash table mapping line numbers to the set of errors occurring on that line *)
-let create_errors_per_line err_log =
+let create_table_err_per_line err_log =
   let err_per_line = Hashtbl.create 17 in
   let add_err _ loc _ _ _ err_name desc _ _ _ _ =
-    let err_str = Localise.to_string err_name ^ " " ^ (pp_to_string Localise.pp_error_desc desc) in
+    let err_str =
+      Localise.to_string err_name ^
+      " " ^
+      (pp_to_string Localise.pp_error_desc desc) in
     try
       let set = Hashtbl.find err_per_line loc.Location.line in
       Hashtbl.replace err_per_line loc.Location.line (StringSet.add err_str set)
@@ -297,148 +436,128 @@ let create_errors_per_line err_log =
   Errlog.iter add_err err_log;
   err_per_line
 
-(** create err message for html file *)
+(** Create error message for html file *)
 let create_err_message err_string =
   "\n<div class=\"msg\" style=\"margin-left:9ex\">" ^ err_string ^ "</div>"
 
-(** Module to read specific lines from files.
-    The data from any file will stay in memory until the handle is collected by the gc *)
-module LineReader : sig
-  type t
-
-  (** create a line reader *)
-  val create : unit -> t
-
-  (** get the line from a source file and line number *)
-  val from_file_linenum_original : t -> DB.source_file -> int -> string option
-
-  (** get the line from a source file and line number looking for the copy of the file in the results dir *)
-  val from_file_linenum : t -> DB.source_file -> int -> string option
-
-  (** get the line from a location looking for the copy of the file in the results dir *)
-  val from_loc : t -> Location.t -> string option
-end = struct
-
-  (* map a file name to an array of string, one for each line in the file *)
-  type t = (DB.source_file, string array) Hashtbl.t
-
-  let create () =
-    Hashtbl.create 1
-
-  let read_file fname =
-    let cin = open_in fname in
-    let lines = ref [] in
-    try
-      while true do
-        let line_raw = input_line cin in
-        let line =
-          let len = String.length line_raw in
-          if len > 0 && String.get line_raw (len -1) = '\013' then
-            String.sub line_raw 0 (len -1)
-          else line_raw in
-        lines := line :: !lines
-      done;
-      assert false (* execution never reaches here *)
-    with End_of_file ->
-      (close_in cin;
-       Array.of_list (IList.rev !lines))
-
-  let file_data (hash: t) fname =
-    try
-      Some (Hashtbl.find hash fname)
-    with Not_found ->
-    try
-      let lines_arr = read_file (DB.source_file_to_string fname) in
-      Hashtbl.add hash fname lines_arr;
-      Some lines_arr
-    with exn when exn_not_failure exn -> None
-
-  let from_file_linenum_original hash fname linenum =
-    match file_data hash fname with
-    | None -> None
-    | Some lines_arr ->
-        if linenum > 0 && linenum <= Array.length lines_arr
-        then Some lines_arr.(linenum -1)
-        else None
-
-  let from_file_linenum hash fname linenum =
-    let fname_in_resdir = DB.source_file_in_resdir fname in
-    let sourcefile_in_resdir = DB.abs_source_file_from_path (DB.filename_to_string fname_in_resdir) in
-    from_file_linenum_original hash sourcefile_in_resdir linenum
-
-  let from_loc hash loc =
-    from_file_linenum hash loc.Location.file loc.Location.line
-end
-
-(** Create filename.c.html with line numbers and links to nodes *)
-let c_file_write_html linereader fname cfg =
-  let proof_cover = ref Specs.Visitedset.empty in
-  let tbl = Hashtbl.create 11 in
-  let process_node n =
+(** Create filename.ext.html. *)
+let write_html_file linereader filename cfg =
+  let process_node nodes_tbl n =
     let lnum = (Cfg.Node.get_loc n).Location.line in
     let curr_nodes =
-      try Hashtbl.find tbl lnum
+      try Hashtbl.find nodes_tbl lnum
       with Not_found -> [] in
-    Hashtbl.replace tbl lnum (n:: curr_nodes) in
-  let fname_encoding = DB.source_file_encoding fname in
-  let (fd, fmt) = Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in
-  let global_err_log = Errlog.empty () in
-  let do_proc proc_name proc_desc = (* add the err_log of this proc to [global_err_log] *)
+    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 =
+    (* add the err_log of this proc to [global_err_log] *)
     let proc_loc = (Cfg.Procdesc.get_loc proc_desc) in
     if Cfg.Procdesc.is_defined proc_desc &&
        (DB.source_file_equal proc_loc.Location.file !DB.current_source) then
       begin
-        IList.iter process_node (Cfg.Procdesc.get_nodes proc_desc);
+        IList.iter (process_node table_nodes_at_linenum) (Cfg.Procdesc.get_nodes proc_desc);
         match Specs.get_summary proc_name with
-        | None -> ()
+        | None ->
+            ()
         | Some summary ->
             IList.iter
-              (fun sp -> proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover)
+              (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
-  Cfg.iter_proc_desc cfg do_proc;
-  let err_per_line = create_errors_per_line global_err_log in
-  try
-    (let s = "<center><h1>File " ^ (DB.source_file_to_string !DB.current_source) ^ "</h1></center>\n" ^
+
+  let pp_prelude () =
+    let s =
+      "<center><h1>File " ^
+      (DB.source_file_to_string !DB.current_source) ^
+      "</h1></center>\n" ^
       "<table class=\"code\">\n" in
-     F.fprintf fmt "%s" s);
-    let linenum = ref 0 in
-    while true do
-      incr linenum;
-      let line_html = match LineReader.from_file_linenum linereader !DB.current_source !linenum with
-        | Some line_raw -> Escape.escape_xml line_raw
-        | None -> raise End_of_file 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
+      | Some line_raw ->
+          Escape.escape_xml line_raw
+      | None ->
+          raise End_of_file in
     let nodes_at_linenum =
-        try Hashtbl.find tbl !linenum
+      try Hashtbl.find table_nodes_at_linenum line_number
       with Not_found -> [] in
     let errors_at_linenum =
       try
-          let errset = Hashtbl.find err_per_line !linenum in
+        let errset = Hashtbl.find table_err_per_line line_number in
         StringSet.elements errset
       with Not_found -> [] in
-      let linenum_str = string_of_int !linenum in
+    let linenum_str = string_of_int line_number in
     let line_str = "LINE" ^ linenum_str in
     let str =
-        "<tr><td class=\"num\" id=\"" ^ line_str ^ "\">" ^ linenum_str ^ "</td><td class=\"line\">" ^ line_html in
+      "<tr><td class=\"num\" id=\"" ^
+      line_str ^
+      "\">" ^
+      linenum_str ^
+      "</td><td class=\"line\">" ^
+      line_html in
     F.fprintf fmt "%s" str;
-      IList.iter (fun n ->
-          let isproof = Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in
-          Io_infer.Html.pp_node_link [fname_encoding] (Cfg.Node.get_description (pe_html Black) n) (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) (is_visited n) isproof fmt (Cfg.Node.get_id n)) nodes_at_linenum;
-      IList.iter (fun n -> match Cfg.Node.get_kind n with
+    IList.iter
+      (fun n ->
+         let isproof =
+           Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in
+         Io_infer.Html.pp_node_link
+           [fname_encoding]
+           (Cfg.Node.get_description (pe_html Black) n)
+           (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n))
+           (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n))
+           (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n))
+           (is_visited n)
+           isproof
+           fmt
+           (Cfg.Node.get_id n))
+      nodes_at_linenum;
+    IList.iter
+      (fun n ->
+         match Cfg.Node.get_kind n with
          | Cfg.Node.Start_node proc_desc ->
              let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
              let num_specs = IList.length (Specs.get_specs proc_name) in
-              let label = (Escape.escape_xml (Procname.to_string proc_name)) ^ ": " ^ (string_of_int num_specs) ^ " specs" in
+             let label =
+               (Escape.escape_xml (Procname.to_string proc_name)) ^
+               ": " ^
+               (string_of_int num_specs) ^
+               " specs" in
              Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label
-          | _ -> ()) nodes_at_linenum;
-      IList.iter (fun err_string -> F.fprintf fmt "%s" (create_err_message err_string)) errors_at_linenum;
-      F.fprintf fmt "%s" "</td></tr>\n"
+         | _ ->
+             ())
+      nodes_at_linenum;
+    IList.iter
+      (fun err_string ->
+         F.fprintf fmt "%s" (create_err_message err_string))
+      errors_at_linenum;
+    F.fprintf fmt "%s" "</td></tr>\n" in
+
+  pp_prelude ();
+  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);
+  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
     done
   with End_of_file ->
     (F.fprintf fmt "%s" "</table>\n";
      Errlog.pp_html [fname_encoding] fmt global_err_log;
      Io_infer.Html.close (fd, fmt))
 
-let c_files_write_html linereader exe_env =
-  if !Config.write_html then Exe_env.iter_files (c_file_write_html linereader) exe_env
+(** Create filename.ext.html for each file in the exe_env. *)
+let write_all_html_files linereader exe_env =
+  if !Config.write_html then
+    Exe_env.iter_files (write_html_file linereader) exe_env

infer/src/backend/printer.mli

@@ -10,27 +10,6 @@
 
 (** Printers for the analysis results *)
 
-(** Current html formatter *)
-val html_formatter : Format.formatter ref
-
-(** return true if the node was visited during footprint and during re-execution*)
-val is_visited_phase : Cfg.Node.t -> bool * bool
-
-(** return true if the node was visited during analysis *)
-val is_visited : Cfg.Node.t -> bool
-
-(** Execute the delayed print actions *)
-val force_delayed_prints : unit -> unit
-
-(** Start a session, and create a new html fine for the node if it does not exist yet *)
-val start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit
-
-(** Finish a session, and perform delayed print actions if required *)
-val finish_session : Cfg.node -> unit
-
-(** Write log file for the proc, the boolean indicates whether to print whole seconds only *)
-val proc_write_log : bool -> Cfg.Procdesc.t -> unit
-
 (** Module to read specific lines from files.
     The data from any file will stay in memory until the handle is collected by the gc *)
 module LineReader : sig
@@ -49,5 +28,24 @@ module LineReader : sig
   val from_loc : t -> Location.t -> string option
 end
 
-(** Create filename.c.html with line numbers and links to nodes for each file in the exe_env *)
-val c_files_write_html : LineReader.t -> Exe_env.t -> unit
+(** Current html formatter *)
+val curr_html_formatter : Format.formatter ref
+
+(** Execute the delayed print actions *)
+val force_delayed_prints : unit -> unit
+
+(** Finish a session, and perform delayed print actions if required *)
+val node_finish_session : Cfg.node -> unit
+
+(** Return true if the node was visited during footprint and during re-execution *)
+val node_is_visited : Cfg.Node.t -> bool * bool
+
+(** Start a session, and create a new html fine for the node if it does not exist yet *)
+val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit
+
+(** Write html file for the procedure.
+    The boolean indicates whether to print whole seconds only. *)
+val write_proc_html : bool -> Cfg.Procdesc.t -> unit
+
+(** Create filename.ext.html for each file in the exe_env. *)
+val write_all_html_files : LineReader.t -> Exe_env.t -> unit