diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index 5a11ace11..16e203941 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -26,9 +26,10 @@ let module Node = {
| Stmt_node string
| Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
- | Skip_node string
+ | Skip_node string;
+
/** a node */
- and t = {
+ type t = {
/** unique id of the node */
nd_id: id,
/** distance to the exit node */
@@ -43,13 +44,14 @@ let module Node = {
nd_loc: Location.t,
/** predecessor nodes in the cfg */
mutable nd_preds: list t,
- /** proc desc from cil */
- nd_proc: option proc_desc,
+ /** name of the procedure the node belongs to */
+ nd_pname: option Procname.t,
/** successor nodes in the cfg */
mutable nd_succs: list t
- }
+ };
+
/** procedure description */
- and proc_desc = {
+ type proc_desc = {
pd_attributes: ProcAttributes.t, /** attributes of the procedure */
pd_id: int, /** unique proc_desc identifier */
mutable pd_nodes: list t, /** list of nodes of this procedure */
@@ -145,7 +147,7 @@ let module Node = {
nd_instrs: [],
nd_kind: Skip_node "dummy",
nd_loc: Location.dummy,
- nd_proc: None,
+ nd_pname: None,
nd_succs: [],
nd_preds: [],
nd_exn: []
@@ -165,7 +167,7 @@ let module Node = {
nd_kind: kind,
nd_loc: loc,
nd_preds: [],
- nd_proc: Some pdesc,
+ nd_pname: Some pdesc.pd_attributes.proc_name,
nd_succs: [],
nd_exn: []
};
@@ -226,13 +228,13 @@ let module Node = {
};
let get_exn node => node.nd_exn;
- /** Get the proc desc of the node */
- let get_proc_desc node =>
- switch node.nd_proc {
+ /** Get the name of the procedure the node belongs to */
+ let get_proc_name node =>
+ switch node.nd_pname {
| None =>
L.out "node_get_proc_desc: at node %d@\n" node.nd_id;
assert false
- | Some proc_desc => proc_desc
+ | Some proc_name => proc_name
};
/** Set the successor nodes and exception nodes, and build predecessor links */
@@ -245,11 +247,10 @@ let module Node = {
/** Set the successor and exception nodes.
If this is a join node right before the exit node, add an extra node in the middle,
otherwise nullify and abstract instructions cannot be added after a conditional. */
- let set_succs_exn node succs exn =>
+ let set_succs_exn pdesc node succs exn =>
switch (node.nd_kind, succs) {
| (Join_node, [{nd_kind: Exit_node _} as exit_node]) =>
let kind = Stmt_node "between_join_and_exit";
- let pdesc = get_proc_desc node;
let node' = create node.nd_loc kind node.nd_instrs pdesc;
set_succs_exn_base node [node'] exn;
set_succs_exn_base node' [exit_node] exn
@@ -355,9 +356,8 @@ let module Node = {
Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name;
/** Add declarations for local variables and return variable to the node */
- let add_locals_ret_declaration node locals => {
+ let add_locals_ret_declaration pdesc node locals => {
let loc = get_loc node;
- let pdesc = get_proc_desc node;
let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name;
let ret_var = {
let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type;
@@ -712,7 +712,7 @@ let module Node = {
if (equal node callee_exit_node) {
proc_desc_set_exit_node resolved_proc_desc new_node
};
- set_succs_exn new_node (loop successors) (loop exn_nodes);
+ set_succs_exn callee_proc_desc new_node (loop successors) (loop exn_nodes);
new_node
};
[converted_node, ...loop other_node]
diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei
index 79106a75b..1f1a049a8 100644
--- a/infer/src/IR/Cfg.rei
+++ b/infer/src/IR/Cfg.rei
@@ -161,7 +161,7 @@ let module Node: {
let prepend_instrs: t => list Sil.instr => unit;
/** Add declarations for local variables and return variable to the node */
- let add_locals_ret_declaration: t => list (Mangled.t, Typ.t) => unit;
+ let add_locals_ret_declaration: Procdesc.t => t => list (Mangled.t, Typ.t) => unit;
/** Compare two nodes */
let compare: t => t => int;
@@ -213,8 +213,8 @@ let module Node: {
from a node with subsequent applications of a generator function */
let get_generated_slope: t => (t => list t) => list t;
- /** Get the proc desc associated to the node */
- let get_proc_desc: t => Procdesc.t;
+ /** Get the name of the procedure the node belongs to */
+ let get_proc_name: t => Procname.t;
/** Get the instructions to be executed */
let get_instrs: t => list Sil.instr;
@@ -249,7 +249,7 @@ let module Node: {
let replace_instrs: t => list Sil.instr => unit;
/** Set the successor nodes and exception nodes, and build predecessor links */
- let set_succs_exn: t => list t => list t => unit;
+ let set_succs_exn: Procdesc.t => t => list t => list t => unit;
};
diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index 61d1d621a..c670e595f 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -55,7 +55,10 @@ let check_access access_opt de_opt =
let find_bucket line_number null_case_flag =
let find_formal_ids node = (* find ids obtained by a letref on a formal parameter *)
let node_instrs = Cfg.Node.get_instrs node in
- let formals = Cfg.Procdesc.get_formals (Cfg.Node.get_proc_desc node) in
+ let formals = match State.get_prop_tenv_pdesc () with
+ | None -> []
+ | Some (_, _, pdesc) ->
+ Cfg.Procdesc.get_formals pdesc in
let formal_names = IList.map fst formals in
let is_formal pvar =
let name = Pvar.get_name pvar in
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 117df45bd..6aeabcd93 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -297,13 +297,11 @@ let propagate_nodes_divergence
(** Symbolic execution for a Join node *)
let do_symexec_join pname tenv wl curr_node (edgeset_todo : Paths.PathSet.t) =
- let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
- let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
let curr_node_id = Cfg.Node.get_id curr_node in
let succ_nodes = Cfg.Node.get_succs curr_node in
let new_dset = edgeset_todo in
let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in
- let old_dset', new_dset' = Dom.pathset_join curr_pname tenv old_dset new_dset in
+ let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in
Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset');
IList.iter (fun node ->
Paths.PathSet.iter (fun prop path ->
@@ -334,14 +332,12 @@ let reset_prop_metrics () =
exception RE_EXE_ERROR
-let do_before_node source session node =
+let do_before_node pname source session node =
let loc = Cfg.Node.get_loc node in
- let proc_desc = Cfg.Node.get_proc_desc node in
- let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
State.set_node node;
State.set_session session;
L.reset_delayed_prints ();
- Printer.node_start_session node loc proc_name (session :> int) source
+ Printer.node_start_session node loc pname (session :> int) source
let do_after_node source node =
Printer.node_finish_session node source
@@ -363,8 +359,7 @@ let instrs_get_normal_vars instrs =
(* which they prune is the variable (or the negation) which was set in the set instruction *)
(* we exclude function calls: if (g(x,y)) ....*)
(* we check that prune nodes have simple guards: a var or its negation*)
-let check_assignement_guard node =
- let pdesc = Cfg.Node.get_proc_desc node in
+let check_assignement_guard pdesc node =
let pname = Cfg.Procdesc.get_proc_name pdesc in
let verbose = false in
let node_contains_call n =
@@ -467,17 +462,17 @@ let check_assignement_guard node =
) else ()
(** Perform symbolic execution for a node starting from an initial prop *)
-let do_symbolic_execution handle_exn tenv
+let do_symbolic_execution pdesc 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;
(* build the const map lazily *)
State.set_const_map (ConstantPropagation.build_const_map tenv pdesc);
- check_assignement_guard node;
+ check_assignement_guard pdesc node;
let instrs = Cfg.Node.get_instrs node in
(* fresh normal vars must be fresh w.r.t. instructions *)
Ident.update_name_generator (instrs_get_normal_vars instrs);
- let pset = SymExec.node handle_exn tenv node (Paths.PathSet.from_renamed_list [(prop, path)]) in
+ let pset =
+ SymExec.node handle_exn tenv pdesc node (Paths.PathSet.from_renamed_list [(prop, path)]) in
L.d_strln ".... After Symbolic Execution ....";
Propset.d prop (Paths.PathSet.to_propset tenv pset);
L.d_ln (); L.d_ln();
@@ -508,20 +503,19 @@ let add_taint_attrs tenv proc_name proc_desc prop =
Taint.add_tainting_attribute tenv attr param prop_acc)
prop
-let forward_tabulate tenv wl source =
+let forward_tabulate tenv pdesc wl source =
+ let pname = Cfg.Procdesc.get_proc_name pdesc in
let handle_exn_node curr_node exn =
- let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
- let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
Exceptions.print_exception_html "Failure of symbolic execution: " exn;
let pre_opt = (* precondition leading to error, if any *)
- State.get_normalized_pre (Abs.abstract_no_symop curr_pname) in
+ State.get_normalized_pre (Abs.abstract_no_symop pname) in
(match pre_opt with
| Some pre ->
L.d_strln "Precondition:"; Prop.d_prop pre; L.d_ln ()
| None -> ());
L.d_strln "SIL INSTR:";
Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln ();
- Reporting.log_error curr_pname exn;
+ Reporting.log_error pname exn;
State.mark_instr_fail exn in
let exe_iter f pathset =
@@ -533,16 +527,16 @@ let forward_tabulate tenv wl source =
f prop path !cnt ps_size in
Paths.PathSet.iter exe pathset in
- let print_node_preamble curr_node proc_name session pathset_todo =
+ let print_node_preamble curr_node session pathset_todo =
let log_string proc_name =
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
- L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^
+ L.d_strln ("**** " ^ (log_string pname) ^ " " ^
"Node: " ^ string_of_int (Cfg.Node.get_id curr_node :> int) ^ ", " ^
- "Procedure: " ^ Procname.to_string proc_name ^ ", " ^
+ "Procedure: " ^ Procname.to_string pname ^ ", " ^
"Session: " ^ string_of_int session ^ ", " ^
"Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****");
L.d_increase_indent 1;
@@ -551,10 +545,10 @@ let forward_tabulate tenv wl source =
Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node;
L.d_ln (); L.d_ln () in
- let do_prop curr_node proc_desc proc_name handle_exn prop_ path cnt num_paths =
+ let do_prop curr_node handle_exn prop_ path cnt num_paths =
let prop =
if Config.taint_analysis
- then add_taint_attrs tenv proc_name proc_desc prop_
+ then add_taint_attrs tenv pname pdesc prop_
else prop_ in
L.d_strln
("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);
@@ -562,31 +556,31 @@ let forward_tabulate tenv wl source =
try
State.reset_diverging_states_node ();
let pset =
- do_symbolic_execution handle_exn tenv curr_node prop path in
+ do_symbolic_execution pdesc handle_exn tenv curr_node prop path in
let succ_nodes = Cfg.Node.get_succs curr_node in
let exn_nodes = Cfg.Node.get_exn curr_node in
- propagate_nodes_divergence tenv proc_desc pset succ_nodes exn_nodes wl;
+ propagate_nodes_divergence tenv pdesc pset succ_nodes exn_nodes wl;
L.d_decrease_indent 1; L.d_ln();
with
| exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn;
L.d_decrease_indent 1; L.d_ln () in
- let do_node curr_node proc_desc proc_name pathset_todo session handle_exn =
+ let do_node curr_node pathset_todo session handle_exn =
check_prop_size pathset_todo;
- print_node_preamble curr_node proc_name session pathset_todo;
+ print_node_preamble curr_node session pathset_todo;
match Cfg.Node.get_kind curr_node with
| Cfg.Node.Join_node ->
- do_symexec_join proc_name tenv wl curr_node pathset_todo
+ do_symexec_join pname tenv wl curr_node pathset_todo
| Cfg.Node.Stmt_node _
| Cfg.Node.Prune_node _
| Cfg.Node.Exit_node _
| Cfg.Node.Skip_node _
| Cfg.Node.Start_node _ ->
- exe_iter (do_prop curr_node proc_desc proc_name handle_exn) pathset_todo in
+ exe_iter (do_prop curr_node handle_exn) pathset_todo in
- let do_node_and_handle curr_node proc_desc proc_name session =
+ let do_node_and_handle curr_node session =
let pathset_todo = path_set_checkout_todo wl curr_node in
try
begin
@@ -594,7 +588,7 @@ let forward_tabulate tenv wl source =
let handle_exn exn =
handle_exn_called := true;
handle_exn_node curr_node exn in
- do_node curr_node proc_desc proc_name pathset_todo session handle_exn;
+ do_node curr_node pathset_todo session handle_exn;
if !handle_exn_called then Printer.force_delayed_prints ();
do_after_node source curr_node
end
@@ -607,15 +601,13 @@ let forward_tabulate tenv wl source =
while not (Worklist.is_empty wl) do
let curr_node = Worklist.remove wl in
- let proc_desc = Cfg.Node.get_proc_desc curr_node in
- let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
- let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
+ let summary = Specs.get_summary_unsafe "forward_tabulate" pname in
mark_visited summary curr_node; (* mark nodes visited in fp and re phases *)
let session =
incr summary.Specs.sessions;
!(summary.Specs.sessions) in
- do_before_node source session curr_node;
- do_node_and_handle curr_node proc_desc proc_name session
+ do_before_node pname source session curr_node;
+ do_node_and_handle curr_node session
done;
L.d_strln ".... Work list empty. Stop ...."; L.d_ln ()
@@ -915,9 +907,9 @@ let initial_prop_from_pre tenv curr_f pre =
(** Re-execute one precondition and return some spec if there was no re-execution error. *)
let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) source
: Prop.normal Specs.spec option =
- let proc_name = Cfg.Procdesc.get_proc_name pdesc in
- do_before_node source 0 init_node;
- L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
+ let pname = Cfg.Procdesc.get_proc_name pdesc in
+ do_before_node pname source 0 init_node;
+ L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string pname ^ " ####");
L.d_indent 1;
L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
L.d_ln (); L.d_ln ();
@@ -932,10 +924,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
try
Worklist.add wl init_node;
ignore (path_set_put_todo wl init_node init_edgeset);
- forward_tabulate tenv wl source;
- do_before_node source 0 init_node;
+ forward_tabulate tenv pdesc wl source;
+ do_before_node pname source 0 init_node;
L.d_strln_color Green
- ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
+ ("#### Finished: RE-execution for " ^ Procname.to_string pname ^ " ####");
L.d_increase_indent 1;
L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition);
L.d_ln ();
@@ -956,9 +948,9 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
do_after_node source init_node;
Some spec
with RE_EXE_ERROR ->
- do_before_node source 0 init_node;
+ do_before_node pname source 0 init_node;
Printer.force_delayed_prints ();
- L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string proc_name ^ "] ...ERROR");
+ L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string pname ^ "] ...ERROR");
L.d_increase_indent 1;
L.d_strln "when starting from pre:";
Prop.d_prop (Specs.Jprop.to_prop precondition);
@@ -986,13 +978,15 @@ let pp_intra_stats wl proc_desc fmt _ =
nodes;
F.fprintf fmt "(%d nodes containing %d states)" (IList.length nodes) !nstates
+type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase)
+
(** Return functions to perform one phase of the analysis for a procedure.
Given [proc_name], return [do, get_results] where [go ()] performs the analysis phase
and [get_results ()] returns the results computed.
This function is architected so that [get_results ()] can be called even after
[go ()] was interrupted by and exception. *)
let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) source
- : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
+ : exe_phase =
let start_node = Cfg.Procdesc.get_start_node pdesc in
let check_recursion_level () =
@@ -1004,7 +998,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level))
end in
- let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
+ let compute_footprint () : exe_phase =
let go (wl : Worklist.t) () =
let init_prop = initial_prop_from_emp tenv pdesc in
(* use existing pre's (in recursion some might exist) as starting points *)
@@ -1031,7 +1025,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
(Cfg.Procdesc.get_flags pdesc)
Mleak_buckets.objc_arc_flag;
ignore (path_set_put_todo wl start_node init_edgeset);
- forward_tabulate tenv wl source in
+ forward_tabulate tenv pdesc wl source in
let get_results (wl : Worklist.t) () =
State.process_execution_failures Reporting.log_warning pname;
let results = collect_analysis_result tenv wl pdesc in
@@ -1053,15 +1047,14 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
let wl = path_set_create_worklist pdesc in
go wl, get_results wl in
- let re_execution proc_name
- : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
+ let re_execution () : exe_phase =
let candidate_preconditions =
IList.map
(fun spec -> spec.Specs.pre)
- (Specs.get_specs proc_name) in
+ (Specs.get_specs pname) in
let valid_specs = ref [] in
let go () =
- L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name;
+ L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp pname;
check_recursion_level ();
let filter p =
let wl = path_set_create_worklist pdesc in
@@ -1074,7 +1067,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
let outcome = if is_valid then "pass" else "fail" in
L.out "Finished re-execution for precondition %d %a (%s)@."
(Specs.Jprop.to_number p)
- (pp_intra_stats wl pdesc) proc_name
+ (pp_intra_stats wl pdesc) pname
outcome;
speco in
if Config.undo_join then
@@ -1083,22 +1076,22 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
ignore (IList.map filter candidate_preconditions) in
let get_results () =
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;
+ L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
+ L.out "#### Finished: Re-Execution for %a ####@." Procname.pp pname;
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 source)
- [(Procname.to_filename proc_name)] in
+ [(Procname.to_filename pname)] in
if Config.write_dotty then
Dotty.pp_speclist_dotty_file filename specs;
L.out "@.@.================================================";
- L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp proc_name;
+ L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp pname;
L.out "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text false) candidate_preconditions;
L.out "@.@.================================================";
- L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp proc_name;
+ L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp pname;
L.out "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions;
specs, Specs.RE_EXECUTION in
@@ -1106,9 +1099,9 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
match Specs.get_phase pname with
| Specs.FOOTPRINT ->
- compute_footprint
+ compute_footprint ()
| Specs.RE_EXECUTION ->
- re_execution pname
+ re_execution ()
let set_current_language proc_desc =
let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
@@ -1385,7 +1378,7 @@ let perform_transition exe_env tenv proc_name source =
f start_node
| None -> ()
with exn when SymOp.exn_not_failure exn -> () in
- apply_start_node (do_before_node source 0);
+ apply_start_node (do_before_node proc_name source 0);
try
Config.allow_leak := true;
let res = collect_preconditions tenv proc_name in
@@ -1511,23 +1504,26 @@ let do_analysis exe_env =
Ondemand.unset_callbacks ()
-let visited_and_total_nodes cfg =
- let all_nodes =
- let set = ref Cfg.NodeSet.empty in
- let add _ n = set := Cfg.NodeSet.add n !set in
- Cfg.iter_all_nodes add cfg;
- !set in
- let filter_node n =
- Cfg.Procdesc.is_defined (Cfg.Node.get_proc_desc n) &&
+let visited_and_total_nodes ~filter cfg =
+ let filter_node pdesc n =
+ Cfg.Procdesc.is_defined pdesc &&
+ filter pdesc &&
match Cfg.Node.get_kind n with
| Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _
| 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.node_is_visited node))
- counted_nodes in
+ let counted_nodes, visited_nodes_re =
+ let set = ref Cfg.NodeSet.empty in
+ let set_visited_re = ref Cfg.NodeSet.empty in
+ let add pdesc n =
+ if filter_node pdesc n then
+ begin
+ set := Cfg.NodeSet.add n !set;
+ if snd (Printer.node_is_visited (Cfg.Procdesc.get_proc_name pdesc) n)
+ then set_visited_re := Cfg.NodeSet.add n !set_visited_re
+ end in
+ Cfg.iter_all_nodes add cfg;
+ !set, !set_visited_re in
Cfg.NodeSet.elements visited_nodes_re, Cfg.NodeSet.elements counted_nodes
(** Print the stats for the given cfg.
@@ -1535,12 +1531,10 @@ let visited_and_total_nodes cfg =
was defined in another module, and was the one which was analyzed *)
let print_stats_cfg proc_shadowed source cfg =
let err_table = Errlog.create_err_table () in
- let nvisited, ntotal = visited_and_total_nodes cfg in
- let node_filter n =
- let node_procname = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc n) in
- Specs.summary_exists node_procname && Specs.get_specs node_procname != [] in
- let nodes_visited = IList.filter node_filter nvisited in
- let nodes_total = IList.filter node_filter ntotal in
+ let filter pdesc =
+ let pname = Cfg.Procdesc.get_proc_name pdesc in
+ Specs.summary_exists pname && Specs.get_specs pname != [] in
+ let nodes_visited, nodes_total = visited_and_total_nodes ~filter cfg in
let num_proc = ref 0 in
let num_nospec_noerror_proc = ref 0 in
let num_spec_noerror_proc = ref 0 in
diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml
index ce5697e01..48711d5fe 100644
--- a/infer/src/backend/paths.ml
+++ b/infer/src/backend/paths.ml
@@ -271,7 +271,7 @@ end = struct
Invariant.reset_stats path
let get_path_pos node =
- let pn = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc node) in
+ let pn = Cfg.Node.get_proc_name node in
let n_id = Cfg.Node.get_id node in
(pn, (n_id :> int))
diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml
index 09256f28d..593a0d2ae 100644
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@@ -77,9 +77,7 @@ end
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
+let node_is_visited proc_name node =
match Specs.get_summary proc_name with
| None ->
false, false
@@ -92,8 +90,8 @@ let node_is_visited node =
is_visited_fp, is_visited_re
(** Return true if the node was visited during analysis *)
-let is_visited node =
- let visited_fp, visited_re = node_is_visited node in
+let is_visited proc_name node =
+ let visited_fp, visited_re = node_is_visited proc_name node in
visited_fp || visited_re
(* =============== START of module NodesHtml =============== *)
@@ -137,21 +135,21 @@ end = struct
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
- (is_visited node) false fmt (Cfg.Node.get_id node :> int)) preds;
+ (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) preds;
F.fprintf fmt "
SUCCS: @\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
- (is_visited node) false fmt (Cfg.Node.get_id node :> int)) succs;
+ (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) succs;
F.fprintf fmt "
EXN: @\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
- (is_visited node) false fmt (Cfg.Node.get_id node :> int)) exns;
+ (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) exns;
F.fprintf fmt "
@\n";
F.pp_print_flush fmt ();
true
@@ -422,7 +420,7 @@ let write_proc_html source whole_seconds pdesc =
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list)
- (is_visited n) false fmt (Cfg.Node.get_id n :> int))
+ (is_visited pname n) false fmt (Cfg.Node.get_id n :> int))
nodes;
(match Specs.get_summary pname with
| None ->
@@ -454,12 +452,12 @@ let create_err_message err_string =
let write_html_proc source 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 process_node n =
let lnum = (Cfg.Node.get_loc n).Location.line in
let curr_nodes =
- try Hashtbl.find nodes_tbl lnum
+ try Hashtbl.find table_nodes_at_linenum lnum
with Not_found -> [] in
- Hashtbl.replace nodes_tbl lnum (n:: curr_nodes) in
+ Hashtbl.replace table_nodes_at_linenum lnum ((n, proc_desc) :: curr_nodes) in
let proc_loc = Cfg.Procdesc.get_loc proc_desc in
let process_proc =
Cfg.Procdesc.is_defined proc_desc &&
@@ -470,7 +468,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
DB.source_file_equal source_captured (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);
+ IList.iter process_node (Cfg.Procdesc.get_nodes proc_desc);
match Specs.get_summary proc_name with
| None ->
()
@@ -522,7 +520,7 @@ let write_html_file linereader filename procs =
line_html in
F.fprintf fmt "%s" str;
IList.iter
- (fun n ->
+ (fun (n, pdesc) ->
let isproof =
Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in
Io_infer.Html.pp_node_link
@@ -531,13 +529,13 @@ let write_html_file linereader filename procs =
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list)
- (is_visited n)
+ (is_visited (Cfg.Procdesc.get_proc_name pdesc) n)
isproof
fmt
(Cfg.Node.get_id n :> int))
nodes_at_linenum;
IList.iter
- (fun n ->
+ (fun (n, _) ->
match Cfg.Node.get_kind n with
| Cfg.Node.Start_node proc_name ->
let num_specs = IList.length (Specs.get_specs proc_name) in
diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli
index aa6a36981..d1090588f 100644
--- a/infer/src/backend/printer.mli
+++ b/infer/src/backend/printer.mli
@@ -40,7 +40,7 @@ val force_delayed_prints : unit -> unit
val node_finish_session : Cfg.node -> DB.source_file -> unit
(** Return true if the node was visited during footprint and during re-execution *)
-val node_is_visited : Cfg.Node.t -> bool * bool
+val node_is_visited : Procname.t -> 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 -> DB.source_file -> unit
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 47c6c34d3..42d33d784 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -857,27 +857,28 @@ let check_inconsistency_base tenv prop =
let inconsistent_ptsto _ =
check_allocatedness tenv prop Exp.zero in
let inconsistent_this_self_var () =
- let procdesc =
- Cfg.Node.get_proc_desc (State.get_node ()) in
- let procedure_attr =
- Cfg.Procdesc.get_attributes procdesc in
- let is_java_this pvar =
- procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in
- let is_objc_instance_self pvar =
- procedure_attr.ProcAttributes.language = Config.Clang &&
- Pvar.get_name pvar = Mangled.from_string "self" &&
- procedure_attr.ProcAttributes.is_objc_instance_method in
- let is_cpp_this pvar =
- procedure_attr.ProcAttributes.language = Config.Clang &&
- Pvar.is_this pvar &&
- procedure_attr.ProcAttributes.is_cpp_instance_method in
- let do_hpred = function
- | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
- Exp.equal e Exp.zero &&
- Pvar.is_seed pv &&
- (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
- | _ -> false in
- IList.exists do_hpred sigma in
+ match State.get_prop_tenv_pdesc () with
+ | None -> false
+ | Some (_, _, pdesc) ->
+ let procedure_attr =
+ Cfg.Procdesc.get_attributes pdesc in
+ let is_java_this pvar =
+ procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in
+ let is_objc_instance_self pvar =
+ procedure_attr.ProcAttributes.language = Config.Clang &&
+ Pvar.get_name pvar = Mangled.from_string "self" &&
+ procedure_attr.ProcAttributes.is_objc_instance_method in
+ let is_cpp_this pvar =
+ procedure_attr.ProcAttributes.language = Config.Clang &&
+ Pvar.is_this pvar &&
+ procedure_attr.ProcAttributes.is_cpp_instance_method in
+ let do_hpred = function
+ | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
+ Exp.equal e Exp.zero &&
+ Pvar.is_seed pv &&
+ (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
+ | _ -> false in
+ IList.exists do_hpred sigma in
let inconsistent_atom = function
| Sil.Aeq (e1, e2) ->
(match e1, e2 with
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 27d530929..9697ee2db 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1657,8 +1657,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
(** {2 Lifted Abstract Transfer Functions} *)
-let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t =
- let pdesc = Cfg.Node.get_proc_desc node in
+let node handle_exn tenv pdesc node (pset : Paths.PathSet.t) : Paths.PathSet.t =
let pname = Cfg.Procdesc.get_proc_name pdesc in
let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
let pset2 =
diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli
index e8e6757ad..e3f91db99 100644
--- a/infer/src/backend/symExec.mli
+++ b/infer/src/backend/symExec.mli
@@ -13,7 +13,8 @@ open! Utils
(** Symbolic Execution *)
(** Symbolic execution of the instructions of a node, lifted to sets of propositions. *)
-val node : (exn -> unit) -> Tenv.t -> Cfg.Node.t -> Paths.PathSet.t -> Paths.PathSet.t
+val node :
+ (exn -> unit) -> Tenv.t -> Cfg.Procdesc.t -> Cfg.Node.t -> Paths.PathSet.t -> Paths.PathSet.t
(** Symbolic execution of a sequence of instructions.
If errors occur and [mask_errors] is true, just treat as skip. *)
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index a75f5c081..b095aef88 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -159,8 +159,7 @@ module ST = struct
end
end
-let report_calls_and_accesses tenv callback node instr =
- let proc_desc = Cfg.Node.get_proc_desc node in
+let report_calls_and_accesses tenv callback proc_desc instr =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let callee = Procname.to_string proc_name in
match PatternMatch.get_java_field_access_signature instr with
@@ -184,7 +183,9 @@ let report_calls_and_accesses tenv callback node instr =
(** Report all field accesses and method calls of a procedure. *)
let callback_check_access { Callbacks.tenv; proc_desc } =
- Cfg.Procdesc.iter_instrs (report_calls_and_accesses tenv "PROC") proc_desc
+ Cfg.Procdesc.iter_instrs
+ (fun _ instr -> report_calls_and_accesses tenv "PROC" proc_desc instr)
+ proc_desc
(** Report all field accesses and method calls of a class. *)
let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
@@ -192,7 +193,9 @@ let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
match get_proc_desc proc_name with
| Some proc_desc ->
let tenv = Exe_env.get_tenv exe_env proc_name in
- Cfg.Procdesc.iter_instrs (report_calls_and_accesses tenv "CLUSTER") proc_desc
+ Cfg.Procdesc.iter_instrs
+ (fun _ instr -> report_calls_and_accesses tenv "CLUSTER" proc_desc instr)
+ proc_desc
| _ ->
()
) all_procs
diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml
index 8fc0e6b0b..f6c9d4037 100644
--- a/infer/src/checkers/dataflow.ml
+++ b/infer/src/checkers/dataflow.ml
@@ -47,10 +47,9 @@ module type DF = sig
end
(** Determine if the node can throw an exception. *)
-let node_throws node (proc_throws : Procname.t -> throws) : throws =
+let node_throws pdesc node (proc_throws : Procname.t -> throws) : throws =
let instr_throws instr =
let is_return pvar =
- let pdesc = Cfg.Node.get_proc_desc node in
let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in
Pvar.equal pvar ret_pvar in
match instr with
@@ -157,7 +156,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
try
let state = H.find t.pre_states node in
let states_succ, states_exn = St.do_node tenv node state in
- propagate t node states_succ states_exn (node_throws node St.proc_throws)
+ propagate t node states_succ states_exn (node_throws proc_desc node St.proc_throws)
with Not_found -> ()
done in
diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml
index b6975d9d6..b9e371faa 100644
--- a/infer/src/clang/cFrontend_decl.ml
+++ b/infer/src/clang/cFrontend_decl.ml
@@ -38,8 +38,9 @@ struct
"\n\n>>---------- Start translating body of function: '%s' ---------<<\n@."
(Procname.to_string procname);
let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in
- Cfg.Node.add_locals_ret_declaration start_node (Cfg.Procdesc.get_locals procdesc);
- Cfg.Node.set_succs_exn start_node meth_body_nodes [];
+ Cfg.Node.add_locals_ret_declaration
+ procdesc start_node (Cfg.Procdesc.get_locals procdesc);
+ Cfg.Node.set_succs_exn procdesc start_node meth_body_nodes [];
Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc))
| None -> ())
with
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 4ac0b7390..b09109b78 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -591,15 +591,16 @@ struct
this_expr_trans trans_state sil_loc expr_info.Clang_ast_t.ei_type_ptr
let rec labelStmt_trans trans_state stmt_info stmt_list label_name =
+ let context = trans_state.context in
(* go ahead with the translation *)
let res_trans = match stmt_list with
| [stmt] ->
instruction trans_state stmt
| _ -> assert false (* expected a stmt or at most a compoundstmt *) in
(* create the label root node into the hashtbl *)
- let sil_loc = CLocation.get_sil_location stmt_info trans_state.context in
+ let sil_loc = CLocation.get_sil_location stmt_info context in
let root_node' = GotoLabel.find_goto_label trans_state.context label_name sil_loc in
- Cfg.Node.set_succs_exn root_node' res_trans.root_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc root_node' res_trans.root_nodes [];
{ empty_res_trans with root_nodes = [root_node']; leaf_nodes = trans_state.succ_nodes }
and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) =
@@ -723,7 +724,8 @@ struct
{ empty_res_trans with exps = [(const_exp, typ)] }
and arraySubscriptExpr_trans trans_state expr_info stmt_list =
- let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
+ let context = trans_state.context in
+ let typ = CTypes_decl.get_type_from_expr_info expr_info context.tenv in
let array_stmt, idx_stmt = (match stmt_list with
| [a; i] -> a, i (* Assumption: the statement list contains 2 elements,
the first is the array expr and the second the index *)
@@ -748,7 +750,7 @@ struct
if res_trans_idx.root_nodes <> []
then
IList.iter
- (fun n -> Cfg.Node.set_succs_exn n res_trans_idx.root_nodes [])
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_idx.root_nodes [])
res_trans_a.leaf_nodes;
(* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *)
@@ -1129,7 +1131,9 @@ struct
"ConditinalStmt Branch" stmt_info all_res_trans in
let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in
let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in
- IList.iter (fun n -> Cfg.Node.set_succs_exn n res_trans.root_nodes []) prune_nodes' in
+ IList.iter
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans.root_nodes [])
+ prune_nodes' in
(match stmt_list with
| [cond; exp1; exp2] ->
let typ =
@@ -1137,7 +1141,7 @@ struct
context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in
let var_typ = add_reference_if_glvalue typ expr_info in
let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in
- Cfg.Node.set_succs_exn join_node succ_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes [];
let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in
Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)];
let continuation' = mk_cond_continuation trans_state.continuation in
@@ -1210,7 +1214,7 @@ struct
let prune_t = mk_prune_node true e' instrs' in
let prune_f = mk_prune_node false e' instrs' in
IList.iter
- (fun n' -> Cfg.Node.set_succs_exn n' [prune_t; prune_f] [])
+ (fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [prune_t; prune_f] [])
res_trans_cond.leaf_nodes;
let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then
[prune_t; prune_f]
@@ -1243,7 +1247,7 @@ struct
| Binop.LOr -> prune_nodes_f, prune_nodes_t
| _ -> assert false) in
IList.iter
- (fun n -> Cfg.Node.set_succs_exn n res_trans_s2.root_nodes [])
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_s2.root_nodes [])
prune_to_s2;
let root_nodes_to_parent =
if (IList.length res_trans_s1.root_nodes) = 0
@@ -1284,7 +1288,7 @@ struct
let succ_nodes = trans_state.succ_nodes in
let sil_loc = CLocation.get_sil_location stmt_info context in
let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in
- Cfg.Node.set_succs_exn join_node succ_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes [];
let trans_state' = { trans_state with succ_nodes = [join_node] } in
let do_branch branch stmt_branch prune_nodes =
(* leaf nodes are ignored here as they will be already attached to join_node *)
@@ -1297,7 +1301,9 @@ struct
res_trans_b.root_nodes) in
let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in
let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in
- IList.iter (fun n -> Cfg.Node.set_succs_exn n nodes_branch []) prune_nodes' in
+ IList.iter
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n nodes_branch [])
+ prune_nodes' in
(match stmt_list with
| [_; decl_stmt; cond; stmt1; stmt2] ->
(* set the flat to inform that we are translating a condition of a if *)
@@ -1333,7 +1339,7 @@ struct
let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in
create_node node_kind res_trans_cond_tmp.instrs sil_loc context in
IList.iter
- (fun n' -> Cfg.Node.set_succs_exn n' [switch_special_cond_node] [])
+ (fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [switch_special_cond_node] [])
res_trans_cond_tmp.leaf_nodes;
let root_nodes =
if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.root_nodes
@@ -1431,8 +1437,8 @@ struct
let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in
(* connects between cases, then continuation has priority about breaks *)
let prune_node_t, prune_node_f = create_prune_nodes_for_case case in
- Cfg.Node.set_succs_exn prune_node_t case_entry_point [];
- Cfg.Node.set_succs_exn prune_node_f last_prune_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc prune_node_t case_entry_point [];
+ Cfg.Node.set_succs_exn context.procdesc prune_node_f last_prune_nodes [];
case_entry_point, [prune_node_t; prune_node_f]
| DefaultStmt(stmt_info, default_content) :: rest ->
let sil_loc = CLocation.get_sil_location stmt_info context in
@@ -1442,13 +1448,14 @@ struct
translate_and_connect_cases rest next_nodes [placeholder_entry_point] in
let default_entry_point =
connected_instruction (IList.rev default_content) last_nodes in
- Cfg.Node.set_succs_exn placeholder_entry_point default_entry_point [];
+ Cfg.Node.set_succs_exn
+ context.procdesc placeholder_entry_point default_entry_point [];
default_entry_point, last_prune_nodes
| _ -> assert false in
let top_entry_point, top_prune_nodes =
translate_and_connect_cases list_of_cases succ_nodes succ_nodes in
let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point in
- Cfg.Node.set_succs_exn switch_special_cond_node top_prune_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc switch_special_cond_node top_prune_nodes [];
let top_nodes = res_trans_decl.root_nodes in
IList.iter
(fun n' -> Cfg.Node.append_instrs n' []) succ_nodes;
@@ -1529,9 +1536,13 @@ struct
match loop_kind with
| Loops.For _ | Loops.While _ -> res_trans_body.root_nodes
| Loops.DoWhile _ -> [join_node] in
- Cfg.Node.set_succs_exn join_node join_succ_nodes [];
- IList.iter (fun n -> Cfg.Node.set_succs_exn n prune_t_succ_nodes []) prune_nodes_t;
- IList.iter (fun n -> Cfg.Node.set_succs_exn n succ_nodes []) prune_nodes_f;
+ Cfg.Node.set_succs_exn context.procdesc join_node join_succ_nodes [];
+ IList.iter
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n prune_t_succ_nodes [])
+ prune_nodes_t;
+ IList.iter
+ (fun n -> Cfg.Node.set_succs_exn context.procdesc n succ_nodes [])
+ prune_nodes_f;
let root_nodes =
match loop_kind with
| Loops.For _ ->
@@ -1880,6 +1891,7 @@ struct
let mk_ret_node instrs =
let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in
Cfg.Node.set_succs_exn
+ context.procdesc
ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] [];
ret_node in
let trans_result = (match stmt_list with
@@ -1912,7 +1924,7 @@ struct
let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in
let ret_node = mk_ret_node instrs in
IList.iter
- (fun n -> Cfg.Node.set_succs_exn n [ret_node] [])
+ (fun n -> Cfg.Node.set_succs_exn procdesc n [ret_node] [])
res_trans_stmt.leaf_nodes;
let root_nodes_to_parent =
if IList.length res_trans_stmt.root_nodes >0
@@ -1999,7 +2011,7 @@ struct
autorelease_pool_vars, sil_loc, CallFlags.default) in
let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in
let call_node = create_node node_kind [stmt_call] sil_loc context in
- Cfg.Node.set_succs_exn call_node trans_state.succ_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc call_node trans_state.succ_nodes [];
let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in
instructions trans_state' stmts
@@ -2098,7 +2110,7 @@ struct
and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info =
let context = trans_state.context in
- let typ = CTypes_decl.get_type_from_expr_info expr_info context.CContext.tenv in
+ let typ = CTypes_decl.get_type_from_expr_info expr_info context.tenv in
let sil_loc = CLocation.get_sil_location stmt_info context in
let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
let is_dyn_array = cxx_new_expr_info.Clang_ast_t.xnei_is_array in
@@ -2135,7 +2147,7 @@ struct
let (var_exp, typ) = var_exp_typ in
let res_trans_init_list = initListExpr_initializers_trans trans_state_init var_exp 0 stmts
typ is_dyn_array stmt_info in
- CTrans_utils.collect_res_trans res_trans_init_list
+ CTrans_utils.collect_res_trans context.procdesc res_trans_init_list
else init_expr_trans trans_state_init var_exp_typ init_stmt_info stmt_opt in
let all_res_trans = [res_trans_size; res_trans_new; res_trans_init] in
let nname = "CXXNewExpr" in
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index 3af8ef6d2..e42c2b42c 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -158,7 +158,7 @@ let empty_res_trans = {
let undefined_expression () = Exp.Var (Ident.create_fresh Ident.knormal)
(** Collect the results of translating a list of instructions, and link up the nodes created. *)
-let collect_res_trans l =
+let collect_res_trans pdesc l =
let rec collect l rt =
match l with
| [] -> rt
@@ -170,7 +170,7 @@ let collect_res_trans l =
if rt'.leaf_nodes <> [] then rt'.leaf_nodes
else rt.leaf_nodes in
if rt'.root_nodes <> [] then
- IList.iter (fun n -> Cfg.Node.set_succs_exn n rt'.root_nodes []) rt.leaf_nodes;
+ IList.iter (fun n -> Cfg.Node.set_succs_exn pdesc n rt'.root_nodes []) rt.leaf_nodes;
collect l'
{ root_nodes = root_nodes;
leaf_nodes = leaf_nodes;
@@ -238,14 +238,16 @@ struct
(* deals with creating or not a cfg node depending of owning the *)
(* priority_node. It returns nodes, ids, instrs that should be passed to parent *)
let compute_results_to_parent trans_state loc nd_name stmt_info res_states_children =
- let res_state = collect_res_trans res_states_children in
+ let res_state = collect_res_trans trans_state.context.procdesc res_states_children in
let create_node = own_priority_node trans_state.priority stmt_info && res_state.instrs <> [] in
if create_node then
(* We need to create a node *)
let node_kind = Cfg.Node.Stmt_node (nd_name) in
let node = Nodes.create_node node_kind res_state.instrs loc trans_state.context in
- Cfg.Node.set_succs_exn node trans_state.succ_nodes [];
- IList.iter (fun leaf -> Cfg.Node.set_succs_exn leaf [node] []) res_state.leaf_nodes;
+ Cfg.Node.set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes [];
+ IList.iter
+ (fun leaf -> Cfg.Node.set_succs_exn trans_state.context.procdesc leaf [node] [])
+ res_state.leaf_nodes;
(* Invariant: if root_nodes is empty then the params have not created a node.*)
let root_nodes = (if res_state.root_nodes <> [] then res_state.root_nodes
else [node]) in
@@ -438,20 +440,20 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
(Clang_ast_j.string_of_cast_kind cast_kind);
([], (exp, cast_typ))
-let trans_assertion_failure sil_loc context =
+let trans_assertion_failure sil_loc (context : CContext.t) =
let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in
let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in
let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in
let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
and failure_node =
Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in
- Cfg.Node.set_succs_exn failure_node [exit_node] [];
+ Cfg.Node.set_succs_exn context.procdesc failure_node [exit_node] [];
{ empty_res_trans with root_nodes = [failure_node]; }
-let trans_assume_false sil_loc context succ_nodes =
+let trans_assume_false sil_loc (context : CContext.t) succ_nodes =
let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in
let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in
- Cfg.Node.set_succs_exn prune_node succ_nodes [];
+ Cfg.Node.set_succs_exn context.procdesc prune_node succ_nodes [];
{ empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] }
let trans_assertion trans_state sil_loc =
diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli
index 8fd56a710..e2f18c495 100644
--- a/infer/src/clang/cTrans_utils.mli
+++ b/infer/src/clang/cTrans_utils.mli
@@ -44,7 +44,7 @@ val empty_res_trans: trans_result
val undefined_expression: unit -> Exp.t
-val collect_res_trans : trans_result list -> trans_result
+val collect_res_trans : Cfg.Procdesc.t -> trans_result list -> trans_result
val extract_var_exp_or_fail : trans_state -> Exp.t * Typ.t
diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml
index 8ff3de3ea..c82687588 100644
--- a/infer/src/eradicate/eradicate.ml
+++ b/infer/src/eradicate/eradicate.ml
@@ -97,7 +97,7 @@ struct
checks.TypeCheck.check_ret_type;
if checks.TypeCheck.eradicate then
EradicateChecks.check_return_annotation tenv
- find_canonical_duplicate curr_pname exit_node ret_range
+ find_canonical_duplicate curr_pdesc ret_range
ret_ia ret_implicitly_nullable loc in
let do_before_dataflow initial_typestate =
@@ -326,7 +326,7 @@ struct
tenv curr_pname curr_pdesc
annotated_signature;
- TypeErr.report_forall_checks_and_reset tenv (Checkers.ST.report_error tenv) curr_pname;
+ TypeErr.report_forall_checks_and_reset tenv (Checkers.ST.report_error tenv) curr_pdesc;
update_summary curr_pname curr_pdesc final_typestate_opt
(** Entry point for the eradicate-based checker infrastructure. *)
diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml
index 6835c0bed..e1c09ab1f 100644
--- a/infer/src/eradicate/eradicateChecks.ml
+++ b/infer/src/eradicate/eradicateChecks.ml
@@ -67,7 +67,6 @@ let check_field_access tenv
let origin_descr = TypeAnnotation.descr_origin tenv ta in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false))
(Some instr_ref)
loc curr_pname
@@ -87,7 +86,6 @@ let check_array_access tenv
let origin_descr = TypeAnnotation.descr_origin tenv ta in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed))
(Some instr_ref)
loc
@@ -103,7 +101,7 @@ type from_call =
| From_containsKey (** x.containsKey *)
(** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *)
-let check_condition tenv case_zero find_canonical_duplicate curr_pname
+let check_condition tenv case_zero find_canonical_duplicate curr_pdesc
node e typ ta true_branch from_call idenv linereader loc instr_ref : unit =
let is_fun_nonnull ta = match TypeAnnotation.get_origin ta with
| TypeOrigin.Proc proc_origin ->
@@ -111,7 +109,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
Annotations.ia_is_nonnull ia
| _ -> false in
- let contains_instanceof_throwable node =
+ let contains_instanceof_throwable pdesc node =
(* Check if the current procedure has a catch Throwable. *)
(* That always happens in the bytecode generated by try-with-resources. *)
let loc = Cfg.Node.get_loc node in
@@ -128,7 +126,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
let do_node n =
if Location.equal loc (Cfg.Node.get_loc n)
then IList.iter do_instr (Cfg.Node.get_instrs n) in
- Cfg.Procdesc.iter_nodes do_node (Cfg.Node.get_proc_desc node);
+ Cfg.Procdesc.iter_nodes do_node pdesc;
!throwable_found in
let from_try_with_resources () : bool =
@@ -137,7 +135,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
| Some line ->
not (string_contains "==" line || string_contains "!=" line)
&& (string_contains "}" line)
- && contains_instanceof_throwable node
+ && contains_instanceof_throwable curr_pdesc node
| None -> false in
let is_temp = Idenv.exp_is_temp idenv e in
@@ -156,10 +154,9 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
if should_report then
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Condition_redundant (is_always_true, explain_expr tenv node e, nonnull))
(Some instr_ref)
- loc curr_pname
+ loc curr_pdesc
(** Check an "is zero" condition. *)
let check_zero tenv find_canonical_duplicate = check_condition tenv true find_canonical_duplicate
@@ -169,13 +166,14 @@ let check_nonzero tenv find_canonical_duplicate = check_condition tenv false fin
(** Check an assignment to a field. *)
let check_field_assignment tenv
- find_canonical_duplicate curr_pname node instr_ref typestate exp_lhs
+ find_canonical_duplicate curr_pdesc node instr_ref typestate exp_lhs
exp_rhs typ loc fname t_ia_opt typecheck_expr : unit =
+ let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
let (t_lhs, ta_lhs, _) =
- typecheck_expr node instr_ref curr_pname typestate exp_lhs
+ typecheck_expr node instr_ref curr_pdesc typestate exp_lhs
(typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in
let (_, ta_rhs, _) =
- typecheck_expr node instr_ref curr_pname typestate exp_rhs
+ typecheck_expr node instr_ref curr_pdesc typestate exp_rhs
(typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in
let should_report_nullable =
let field_is_field_injector_readwrite () = match t_ia_opt with
@@ -208,20 +206,18 @@ let check_field_assignment tenv
let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Field_annotation_inconsistent (ann, fname, origin_descr))
(Some instr_ref)
- loc curr_pname
+ loc curr_pdesc
end;
if should_report_mutable then
begin
let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Field_not_mutable (fname, origin_descr))
(Some instr_ref)
- loc curr_pname
+ loc curr_pdesc
end
@@ -291,11 +287,10 @@ let check_constructor_initialization tenv
not may_be_assigned_in_final_typestate then
report_error tenv
find_canonical_duplicate
- start_node
(TypeErr.Field_not_initialized (fn, curr_pname))
None
loc
- curr_pname;
+ curr_pdesc;
(* Check if field is over-annotated. *)
if Config.eradicate_field_over_annotated &&
@@ -303,11 +298,10 @@ let check_constructor_initialization tenv
not (may_be_nullable_in_final_typestate ()) then
report_error tenv
find_canonical_duplicate
- start_node
(TypeErr.Field_over_annotated (fn, curr_pname))
None
loc
- curr_pname;
+ curr_pdesc;
) in
IList.iter do_field fields
@@ -336,8 +330,9 @@ let spec_make_return_nullable curr_pname =
(** Check the annotations when returning from a method. *)
let check_return_annotation tenv
- find_canonical_duplicate curr_pname exit_node ret_range
+ find_canonical_duplicate curr_pdesc ret_range
ret_ia ret_implicitly_nullable loc : unit =
+ let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
let ret_annotated_nullable = Annotations.ia_is_nullable ret_ia in
let ret_annotated_present = Annotations.ia_is_present ret_ia in
let ret_annotated_nonnull = Annotations.ia_is_nonnull ret_ia in
@@ -376,20 +371,18 @@ let check_return_annotation tenv
report_error tenv
find_canonical_duplicate
- exit_node
(TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr))
None
- loc curr_pname
+ loc curr_pdesc
end;
if return_over_annotated then
begin
report_error tenv
find_canonical_duplicate
- exit_node
(TypeErr.Return_over_annotated curr_pname)
None
- loc curr_pname
+ loc curr_pdesc
end
| None ->
()
@@ -397,7 +390,7 @@ let check_return_annotation tenv
(** Check the receiver of a virtual call. *)
let check_call_receiver tenv
find_canonical_duplicate
- curr_pname
+ curr_pdesc
node
typestate
call_params
@@ -409,7 +402,7 @@ let check_call_receiver tenv
match call_params with
| ((original_this_e, this_e), typ) :: _ ->
let (_, this_ta, _) =
- typecheck_expr tenv node instr_ref curr_pname typestate this_e
+ typecheck_expr tenv node instr_ref curr_pdesc typestate this_e
(typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in
let null_method_call = TypeAnnotation.get_value Annotations.Nullable this_ta in
let optional_get_on_absent =
@@ -423,17 +416,16 @@ let check_call_receiver tenv
let origin_descr = TypeAnnotation.descr_origin tenv this_ta in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Call_receiver_annotation_inconsistent
(ann, descr, callee_pname, origin_descr))
(Some instr_ref)
- loc curr_pname
+ loc curr_pdesc
end
| [] -> ()
(** Check the parameters of a call. *)
let check_call_parameters tenv
- find_canonical_duplicate curr_pname node typestate callee_attributes
+ find_canonical_duplicate curr_pdesc node typestate callee_attributes
sig_params call_params loc instr_ref typecheck_expr : unit =
let callee_pname = callee_attributes.ProcAttributes.proc_name in
let has_this = is_virtual sig_params in
@@ -444,7 +436,7 @@ let check_call_parameters tenv
let formal_is_nullable = Annotations.ia_is_nullable ia1 in
let formal_is_present = Annotations.ia_is_present ia1 in
let (_, ta2, _) =
- typecheck_expr node instr_ref curr_pname typestate e2
+ typecheck_expr node instr_ref curr_pdesc typestate e2
(t2, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in
let parameter_not_nullable =
not param_is_this &&
@@ -473,7 +465,6 @@ let check_call_parameters tenv
let callee_loc = callee_attributes.ProcAttributes.loc in
report_error tenv
find_canonical_duplicate
- node
(TypeErr.Parameter_annotation_inconsistent (
ann,
description,
@@ -482,7 +473,7 @@ let check_call_parameters tenv
callee_loc,
origin_descr))
(Some instr_ref)
- loc curr_pname;
+ loc curr_pdesc;
if Models.Inference.enabled then
Models.Inference.proc_add_parameter_nullable callee_pname param_num tot_param_num
end;
@@ -515,10 +506,9 @@ let check_overridden_annotations
if ret_is_nullable && not ret_overridden_nullable then
report_error tenv
find_canonical_duplicate
- start_node
(TypeErr.Inconsistent_subclass_return_annotation (proc_name, overriden_proc_name))
None
- loc proc_name
+ loc proc_desc
and check_params overriden_proc_name overriden_signature =
let compare pos current_param overriden_param : int =
@@ -529,11 +519,10 @@ let check_overridden_annotations
&& Annotations.ia_is_nullable overriden_ia then
report_error tenv
find_canonical_duplicate
- start_node
(TypeErr.Inconsistent_subclass_parameter_annotation
(Mangled.to_string current_name, pos, proc_name, overriden_proc_name))
None
- loc proc_name in
+ loc proc_desc in
(pos + 1) in
(* TODO (#5280249): investigate why argument lists can be of different length *)
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index e2c45d78d..012c66ad0 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -157,7 +157,7 @@ type checks =
(** Typecheck an expression. *)
let rec typecheck_expr
- find_canonical_duplicate visited checks tenv node instr_ref curr_pname
+ find_canonical_duplicate visited checks tenv node instr_ref (curr_pdesc : Cfg.Procdesc.t)
typestate e tr_default loc : TypeState.range = match e with
| Exp.Lvar pvar ->
(match TypeState.lookup_pvar pvar typestate with
@@ -177,7 +177,7 @@ let rec typecheck_expr
| Exp.Exn e1 ->
typecheck_expr
find_canonical_duplicate visited checks tenv
- node instr_ref curr_pname
+ node instr_ref curr_pdesc
typestate e1 tr_default loc
| Exp.Const _ ->
let (typ, _, locs) = tr_default in
@@ -186,7 +186,7 @@ let rec typecheck_expr
let _, _, locs = tr_default in
let (_, ta, locs') =
typecheck_expr
- find_canonical_duplicate visited checks tenv node instr_ref curr_pname typestate exp
+ find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate exp
(typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, locs) loc in
let tr_new = match EradicateChecks.get_field_annotation tenv fn typ with
| Some (t, ia) ->
@@ -198,7 +198,7 @@ let rec typecheck_expr
| None -> tr_default in
if checks.eradicate then
EradicateChecks.check_field_access tenv
- find_canonical_duplicate curr_pname node instr_ref exp fn ta loc;
+ find_canonical_duplicate curr_pdesc node instr_ref exp fn ta loc;
tr_new
| Exp.Lindex (array_exp, index_exp) ->
let (_, ta, _) =
@@ -208,7 +208,7 @@ let rec typecheck_expr
checks tenv
node
instr_ref
- curr_pname
+ curr_pdesc
typestate
array_exp
tr_default
@@ -223,7 +223,7 @@ let rec typecheck_expr
if checks.eradicate then
EradicateChecks.check_array_access tenv
find_canonical_duplicate
- curr_pname
+ curr_pdesc
node
instr_ref
array_exp
@@ -429,8 +429,7 @@ let typecheck_instr
annotated_signature.Annotations.params in
let is_return pvar =
- let pdesc = Cfg.Node.get_proc_desc node in
- let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in
+ let ret_pvar = Cfg.Procdesc.get_ret_var curr_pdesc in
Pvar.equal pvar ret_pvar in
(* Apply a function to a pvar and its associated content if front-end generated. *)
@@ -458,7 +457,7 @@ let typecheck_instr
let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 =
typecheck_expr
find_canonical_duplicate calls_this checks tenv node instr_ref
- curr_pname typestate1 exp1
+ curr_pdesc typestate1 exp1
(typ1, TypeAnnotation.const Annotations.Nullable false origin1, [loc1])
loc1 in
@@ -490,7 +489,7 @@ let typecheck_instr
let t_ia_opt = EradicateChecks.get_field_annotation tenv fn f_typ in
if checks.eradicate then
EradicateChecks.check_field_assignment tenv
- find_canonical_duplicate curr_pname node
+ find_canonical_duplicate curr_pdesc node
instr_ref typestate1 e1' e2 typ loc fn t_ia_opt
(typecheck_expr find_canonical_duplicate calls_this checks tenv)
| _ -> () in
@@ -531,7 +530,7 @@ let typecheck_instr
checks tenv
node
instr_ref
- curr_pname
+ curr_pdesc
typestate
array_exp
(t, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc])
@@ -539,7 +538,7 @@ let typecheck_instr
if checks.eradicate then
EradicateChecks.check_array_access tenv
find_canonical_duplicate
- curr_pname
+ curr_pdesc
node
instr_ref
array_exp
@@ -642,11 +641,10 @@ let typecheck_instr
let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in
EradicateChecks.report_error tenv
find_canonical_duplicate
- node
(TypeErr.Condition_redundant
(true, EradicateChecks.explain_expr tenv node cond, false))
(Some instr_ref)
- loc curr_pname
+ loc curr_pdesc
end;
TypeState.add
pvar
@@ -793,7 +791,7 @@ let typecheck_instr
if cflags.CallFlags.cf_virtual && checks.eradicate then
EradicateChecks.check_call_receiver tenv
find_canonical_duplicate
- curr_pname
+ curr_pdesc
node
typestate1
call_params
@@ -804,7 +802,7 @@ let typecheck_instr
if checks.eradicate then
EradicateChecks.check_call_parameters tenv
find_canonical_duplicate
- curr_pname
+ curr_pdesc
node
typestate1
callee_attributes
@@ -946,7 +944,7 @@ let typecheck_instr
if checks.eradicate then
EradicateChecks.check_zero tenv
- find_canonical_duplicate curr_pname
+ find_canonical_duplicate curr_pdesc
node' e' typ
ta true_branch EradicateChecks.From_condition
idenv linereader loc instr_ref;
@@ -992,7 +990,7 @@ let typecheck_instr
typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in
if checks.eradicate then
- EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pname
+ EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc
node e' typ ta true_branch from_call idenv linereader loc instr_ref;
begin
match from_call with
diff --git a/infer/src/eradicate/typeErr.ml b/infer/src/eradicate/typeErr.ml
index 2e7663e55..167c05473 100644
--- a/infer/src/eradicate/typeErr.ml
+++ b/infer/src/eradicate/typeErr.ml
@@ -306,7 +306,8 @@ type st_report_error =
(** Report an error right now. *)
let report_error_now tenv
- (st_report_error : st_report_error) node err_instance loc pname : unit =
+ (st_report_error : st_report_error) err_instance loc pdesc : unit =
+ let pname = Cfg.Procdesc.get_proc_name pdesc in
let demo_mode = true in
let do_print_base ew_string kind_s s =
let mname = match pname with
@@ -529,7 +530,7 @@ let report_error_now tenv
let always_report = Strict.err_instance_get_strict tenv err_instance <> None in
st_report_error
pname
- (Cfg.Node.get_proc_desc node)
+ pdesc
kind_s
loc
~advice
@@ -542,22 +543,22 @@ let report_error_now tenv
(** Report an error unless is has been reported already, or unless it's a forall error
since it requires waiting until the end of the analysis and be printed by flush. *)
-let report_error tenv (st_report_error : st_report_error) find_canonical_duplicate node
- err_instance instr_ref_opt loc pname_java =
+let report_error tenv (st_report_error : st_report_error) find_canonical_duplicate
+ err_instance instr_ref_opt loc pdesc =
let should_report_now =
add_err find_canonical_duplicate err_instance instr_ref_opt loc in
if should_report_now then
- report_error_now tenv st_report_error node err_instance loc pname_java
+ report_error_now tenv st_report_error err_instance loc pdesc
(** Report the forall checks at the end of the analysis and reset the error table *)
-let report_forall_checks_and_reset tenv st_report_error proc_name =
+let report_forall_checks_and_reset tenv st_report_error proc_desc =
let iter (err_instance, instr_ref_opt) err_state =
match instr_ref_opt, get_forall err_instance with
| Some instr_ref, is_forall ->
let node = InstrRef.get_node instr_ref in
State.set_node node;
if is_forall && err_state.always
- then report_error_now tenv st_report_error node err_instance err_state.loc proc_name
+ then report_error_now tenv st_report_error err_instance err_state.loc proc_desc
| None, _ -> () in
H.iter iter err_tbl;
reset ()
diff --git a/infer/src/eradicate/typeErr.mli b/infer/src/eradicate/typeErr.mli
index 11ce8a8c6..7a03dcf19 100644
--- a/infer/src/eradicate/typeErr.mli
+++ b/infer/src/eradicate/typeErr.mli
@@ -81,10 +81,10 @@ type st_report_error =
val report_error :
Tenv.t -> st_report_error ->
- (Cfg.Node.t -> Cfg.Node.t) -> Cfg.Node.t ->
+ (Cfg.Node.t -> Cfg.Node.t) ->
err_instance -> InstrRef.t option -> Location.t ->
- Procname.t -> unit
+ Cfg.Procdesc.t -> unit
-val report_forall_checks_and_reset : Tenv.t -> st_report_error -> Procname.t -> unit
+val report_forall_checks_and_reset : Tenv.t -> st_report_error -> Cfg.Procdesc.t -> unit
val reset : unit -> unit
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index 11d33b024..aefcf0d01 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -257,9 +257,9 @@ let setup_harness_cfg harness_name env cg cfg =
(create_node start_kind, create_node exit_kind) in
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node;
- Cfg.Node.add_locals_ret_declaration start_node [];
- Cfg.Node.set_succs_exn start_node [harness_node] [exit_node];
- Cfg.Node.set_succs_exn harness_node [exit_node] [exit_node];
+ Cfg.Node.add_locals_ret_declaration procdesc start_node [];
+ Cfg.Node.set_succs_exn procdesc start_node [harness_node] [exit_node];
+ Cfg.Node.set_succs_exn procdesc harness_node [exit_node] [exit_node];
add_harness_to_cg harness_name harness_node cg
(** create a procedure named harness_name that calls each of the methods in trace in the specified
diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml
index 848397909..f35cd7acb 100644
--- a/infer/src/java/jFrontend.ml
+++ b/infer/src/java/jFrontend.ml
@@ -48,7 +48,7 @@ let add_edges
if super_call then (fun _ -> exit_nodes)
else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in
let connect node pc =
- Cfg.Node.set_succs_exn node (get_succ_nodes node pc) (get_exn_nodes pc) in
+ Cfg.Node.set_succs_exn context.procdesc node (get_succ_nodes node pc) (get_exn_nodes pc) in
let connect_nodes pc translated_instruction =
match translated_instruction with
| JTrans.Skip -> ()
@@ -57,7 +57,7 @@ let add_edges
connect node_true pc;
connect node_false pc
| JTrans.Loop (join_node, node_true, node_false) ->
- Cfg.Node.set_succs_exn join_node [node_true; node_false] [];
+ Cfg.Node.set_succs_exn context.procdesc join_node [node_true; node_false] [];
connect node_true pc;
connect node_false pc in
let first_nodes =
@@ -65,11 +65,11 @@ let add_edges
direct_successors (-1) in
(* the exceptions edges here are going directly to the exit node *)
- Cfg.Node.set_succs_exn start_node first_nodes exit_nodes;
+ Cfg.Node.set_succs_exn context.procdesc start_node first_nodes exit_nodes;
if not super_call then
(* the exceptions node is just before the exit node *)
- Cfg.Node.set_succs_exn exn_node exit_nodes exit_nodes;
+ Cfg.Node.set_succs_exn context.procdesc exn_node exit_nodes exit_nodes;
Array.iteri connect_nodes method_body_nodes
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 78cf3a79b..d40215250 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -272,7 +272,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
let start_node = Cfg.Node.create Location.dummy start_kind [] procdesc in
let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create Location.dummy exit_kind [] procdesc in
- Cfg.Node.set_succs_exn start_node [exit_node] [exit_node];
+ Cfg.Node.set_succs_exn procdesc start_node [exit_node] [exit_node];
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node;
procdesc
@@ -329,7 +329,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
JContext.add_exn_node proc_name exn_node;
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node;
- Cfg.Node.add_locals_ret_declaration start_node locals;
+ Cfg.Node.add_locals_ret_declaration procdesc start_node locals;
procdesc in
Some procdesc
with JBir.Subroutine | JBasics.Class_structure_error _ ->
diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml
index fecf5d859..dbf48dd2c 100644
--- a/infer/src/java/jTransExn.ml
+++ b/infer/src/java/jTransExn.ml
@@ -91,8 +91,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let node_false =
let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in
create_node loc node_kind_false instrs_false in
- Cfg.Node.set_succs_exn node_true catch_nodes exit_nodes;
- Cfg.Node.set_succs_exn node_false succ_nodes exit_nodes;
+ Cfg.Node.set_succs_exn procdesc node_true catch_nodes exit_nodes;
+ Cfg.Node.set_succs_exn procdesc node_false succ_nodes exit_nodes;
let is_finally = handler.JBir.e_catch_type = None in
if is_finally
then [node_true] (* TODO (#4759480): clean up the translation so prune nodes are not created at all *)
@@ -109,7 +109,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
| n:: _ -> Cfg.Node.get_loc n
| [] -> Location.dummy in
let entry_node = create_entry_node loc in
- Cfg.Node.set_succs_exn entry_node nodes_first_handler exit_nodes;
+ Cfg.Node.set_succs_exn procdesc entry_node nodes_first_handler exit_nodes;
Hashtbl.add catch_block_table handler_list [entry_node] in
Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table;
catch_block_table
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index b9a565395..198710151 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -176,7 +176,7 @@ module Make
let create_node kind cmds =
Cfg.Node.create dummy_loc kind cmds pdesc in
let set_succs cur_node succs ~exn_handlers=
- Cfg.Node.set_succs_exn cur_node succs exn_handlers in
+ Cfg.Node.set_succs_exn pdesc cur_node succs exn_handlers in
let mk_prune_nodes_for_cond cond_exp if_kind =
let mk_prune_node cond_exp if_kind true_branch =
let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in
diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml
index b842e610e..342f4f77e 100644
--- a/infer/src/unit/procCfgTests.ml
+++ b/infer/src/unit/procCfgTests.ml
@@ -37,9 +37,9 @@ let tests =
Cfg.Procdesc.set_start_node test_pdesc n1;
(* let -> represent normal transitions and -*-> represent exceptional transitions *)
(* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *)
- Cfg.Node.set_succs_exn n1 [n2] [n3];
- Cfg.Node.set_succs_exn n2 [n4] [n3];
- Cfg.Node.set_succs_exn n3 [n4] [n4];
+ Cfg.Node.set_succs_exn test_pdesc n1 [n2] [n3];
+ Cfg.Node.set_succs_exn test_pdesc n2 [n4] [n3];
+ Cfg.Node.set_succs_exn test_pdesc n3 [n4] [n4];
let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in
let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in