From ea7c13ff6c768acded605c9bfba1276315018511 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Wed, 2 Sep 2015 13:15:09 -0100 Subject: [PATCH] [backend][cleanup] Move proc_attributes to a separate module. Summary: Move proc_attributes to a separate module. Field err_log, in common between proc desc and summary, can now be moved to ProcAttributes without creating cycles of dependencies. --- infer/src/backend/callbacks.ml | 8 +-- infer/src/backend/cfg.ml | 52 ++++++++--------- infer/src/backend/cfg.mli | 4 +- infer/src/backend/dotty.ml | 5 +- infer/src/backend/fork.ml | 6 +- infer/src/backend/inferanalyze.ml | 2 +- infer/src/backend/inferprint.ml | 51 +++++++++-------- infer/src/backend/interproc.ml | 15 +++-- infer/src/backend/location.ml | 9 +-- infer/src/backend/location.mli | 4 +- infer/src/backend/objc_preanal.ml | 2 +- infer/src/backend/printer.ml | 2 +- infer/src/backend/procAttributes.ml | 82 +++++++++++++++++++++++++++ infer/src/backend/procAttributes.mli | 41 ++++++++++++++ infer/src/backend/prover.ml | 2 +- infer/src/backend/reporting.ml | 2 +- infer/src/backend/sil.ml | 45 --------------- infer/src/backend/sil.mli | 26 --------- infer/src/backend/specs.ml | 78 ++++++++++---------------- infer/src/backend/specs.mli | 10 ++-- infer/src/backend/symExec.ml | 16 +++--- infer/src/checkers/checkers.ml | 6 +- infer/src/checkers/codeQuery.ml | 2 +- infer/src/checkers/eradicate.ml | 11 ++-- infer/src/checkers/typeCheck.ml | 6 +- infer/src/clang/cEnum_decl.ml | 27 +-------- infer/src/clang/cMethod_trans.ml | 48 ++++------------ infer/src/harness/inhabit.ml | 49 +++------------- infer/src/java/jTrans.ml | 84 ++++++---------------------- infer/src/llvm/lTrans.ml | 21 ++----- 30 files changed, 304 insertions(+), 412 deletions(-) create mode 100644 infer/src/backend/procAttributes.ml create mode 100644 infer/src/backend/procAttributes.mli diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 903e303c7..b64bbcbae 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -64,8 +64,8 @@ let proc_inline_synthetic_methods cfg proc_desc : unit = | Some pd -> let is_access = Procname.java_is_access_method pn in let attributes = Cfg.Procdesc.get_attributes pd in - let is_synthetic = attributes.Sil.is_synthetic_method in - let is_bridge = attributes.Sil.is_bridge_method in + let is_synthetic = attributes.ProcAttributes.is_synthetic_method in + let is_bridge = attributes.ProcAttributes.is_bridge_method in if is_access || is_bridge || is_synthetic then inline_synthetic_method ret_ids etl pd pn loc else None @@ -121,7 +121,7 @@ let get_procedure_definition exe_env proc_name = (fun proc_desc -> proc_inline_synthetic_methods cfg proc_desc; let idenv = Idenv.create cfg proc_desc - and language = (Cfg.Procdesc.get_attributes proc_desc).Sil.language in + and language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in (idenv, tenv, proc_name, proc_desc, language)) (Cfg.Procdesc.find_from_name cfg proc_name) @@ -224,7 +224,7 @@ let iterate_callbacks store_summary call_graph exe_env = let loc = match procdesc_opt with | Some proc_desc -> Cfg.Procdesc.get_loc proc_desc - | None -> Location.loc_none in + | None -> Location.dummy in Specs.reset_summary call_graph proc_name loc in diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index be29e9b0e..9f8fa5f0d 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -40,12 +40,11 @@ module Node = struct mutable nd_succs : t list; (** successor nodes in the cfg *) } and proc_desc = { (** procedure description *) - pd_attributes : Sil.proc_attributes; (** attributes of the procedure *) + pd_attributes : ProcAttributes.t; (** attributes of the procedure *) pd_id : int; (** unique proc_desc identifier *) mutable pd_nodes : t list; (** list of nodes of this procedure *) mutable pd_start_node : t; (** start node of this procedure *) mutable pd_exit_node : t; (** exit node of ths procedure *) - pd_err_log: Errlog.t; (** error log at translation time *) mutable pd_changed : bool; (** true if proc has changed since last analysis *) } @@ -104,9 +103,10 @@ module Node = struct try list_for_all2 node_eq n1s n2s with Invalid_argument _ -> false in - pd1.pd_attributes.Sil.is_defined = pd2.pd_attributes.Sil.is_defined && - Sil.typ_equal pd1.pd_attributes.Sil.ret_type pd2.pd_attributes.Sil.ret_type && - formals_eq pd1.pd_attributes.Sil.formals pd2.pd_attributes.Sil.formals && + let att1 = pd1.pd_attributes and att2 = pd2.pd_attributes in + att1.ProcAttributes.is_defined = att2.ProcAttributes.is_defined && + Sil.typ_equal att1.ProcAttributes.ret_type att2.ProcAttributes.ret_type && + formals_eq att1.ProcAttributes.formals att2.ProcAttributes.formals && nodes_eq pd1.pd_nodes pd2.pd_nodes in let old_procs = cfg_old.name_pdesc_tbl in let new_procs = cfg_new.name_pdesc_tbl in @@ -131,12 +131,12 @@ module Node = struct let node_list' = let filter_node node = match node.nd_proc with | None -> true - | Some pdesc -> is_enabled pdesc.pd_attributes.Sil.proc_name in + | Some pdesc -> is_enabled pdesc.pd_attributes.ProcAttributes.proc_name in list_filter filter_node !(cfg.node_list) in let procs_to_remove = let psetr = ref Procname.Set.empty in let do_proc pname pdesc = - if pdesc.pd_attributes.Sil.is_defined && + if pdesc.pd_attributes.ProcAttributes.is_defined && not (is_enabled pname) && not (in_address_set pname) then psetr := Procname.Set.add pname !psetr in @@ -179,7 +179,7 @@ module Node = struct nd_dead_pvars_before = []; nd_instrs = []; nd_kind = Skip_node "dummy"; - nd_loc = Location.loc_none; + nd_loc = Location.dummy; nd_proc = None; nd_succs = []; nd_preds = []; nd_exn = []; } @@ -384,15 +384,15 @@ module Node = struct node.nd_instrs <- instrs let proc_desc_get_ret_var pdesc = - Sil.get_ret_pvar pdesc.pd_attributes.Sil.proc_name + Sil.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 loc = get_loc node in let pdesc = get_proc_desc node in - let proc_name = pdesc.pd_attributes.Sil.proc_name in + let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name in let ret_var = - let ret_type = pdesc.pd_attributes.Sil.ret_type in + let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type in (proc_desc_get_ret_var pdesc, ret_type) in let construct_decl (x, typ) = (Sil.mk_pvar x proc_name, typ) in @@ -429,7 +429,7 @@ module Node = struct proc_desc.pd_start_node let proc_desc_get_err_log proc_desc = - proc_desc.pd_err_log + proc_desc.pd_attributes.ProcAttributes.err_log let proc_desc_get_attributes proc_desc = proc_desc.pd_attributes @@ -462,33 +462,33 @@ module Node = struct (** Set a flag for the proc desc *) let proc_desc_set_flag pdesc key value = - proc_flags_add pdesc.pd_attributes.Sil.proc_flags key value + proc_flags_add pdesc.pd_attributes.ProcAttributes.proc_flags key value (** Return the return type of the procedure *) let proc_desc_get_ret_type proc_desc = - proc_desc.pd_attributes.Sil.ret_type + proc_desc.pd_attributes.ProcAttributes.ret_type let proc_desc_get_proc_name proc_desc = - proc_desc.pd_attributes.Sil.proc_name + proc_desc.pd_attributes.ProcAttributes.proc_name (** Return [true] iff the procedure is defined, and not just declared *) let proc_desc_is_defined proc_desc = - proc_desc.pd_attributes.Sil.is_defined + proc_desc.pd_attributes.ProcAttributes.is_defined let proc_desc_get_loc proc_desc = - proc_desc.pd_attributes.Sil.loc + proc_desc.pd_attributes.ProcAttributes.loc (** Return name and type of formal parameters *) let proc_desc_get_formals proc_desc = - proc_desc.pd_attributes.Sil.formals + proc_desc.pd_attributes.ProcAttributes.formals (** Return name and type of local variables *) let proc_desc_get_locals proc_desc = - proc_desc.pd_attributes.Sil.locals + proc_desc.pd_attributes.ProcAttributes.locals (** Return name and type of captured variables *) let proc_desc_get_captured proc_desc = - proc_desc.pd_attributes.Sil.captured + proc_desc.pd_attributes.ProcAttributes.captured let proc_desc_get_nodes proc_desc = proc_desc.pd_nodes @@ -503,11 +503,12 @@ module Node = struct (** Get flags for the proc desc *) let proc_desc_get_flags proc_desc = - proc_desc.pd_attributes.Sil.proc_flags + proc_desc.pd_attributes.ProcAttributes.proc_flags (** Append the locals to the list of local variables *) let proc_desc_append_locals proc_desc new_locals = - proc_desc.pd_attributes.Sil.locals <- proc_desc.pd_attributes.Sil.locals @ new_locals + proc_desc.pd_attributes.ProcAttributes.locals <- + proc_desc.pd_attributes.ProcAttributes.locals @ new_locals (** Get the cyclomatic complexity for the procedure *) let proc_desc_get_cyclomatic proc_desc = @@ -681,7 +682,7 @@ module Procdesc = struct type proc_desc_builder = { cfg : cfg; - proc_attributes : Sil.proc_attributes; + proc_attributes : ProcAttributes.t; } let create (b : proc_desc_builder) = @@ -694,10 +695,9 @@ module Procdesc = struct pd_nodes = []; pd_start_node = dummy (); pd_exit_node = dummy (); - pd_err_log = Errlog.empty (); pd_changed = true } in - pdesc_tbl_add b.cfg b.proc_attributes.Sil.proc_name pdesc; + pdesc_tbl_add b.cfg b.proc_attributes.ProcAttributes.proc_name pdesc; pdesc let remove = Node.proc_desc_remove @@ -762,7 +762,7 @@ let get_defined_procs cfg = let get_objc_generated_procs cfg = list_filter ( fun procdesc -> - (Procdesc.get_attributes procdesc).Sil.is_generated) (get_all_procs cfg) + (Procdesc.get_attributes procdesc).ProcAttributes.is_generated) (get_all_procs cfg) (** get the function names which should be analyzed before the other ones *) let get_priority_procnames cfg = diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index 3123b784e..d03919f0d 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -33,7 +33,7 @@ module Procdesc : sig type proc_desc_builder = { cfg : cfg; - proc_attributes : Sil.proc_attributes; + proc_attributes : ProcAttributes.t; } (** Create a procdesc *) @@ -47,7 +47,7 @@ module Procdesc : sig val find_from_name : cfg -> Procname.t -> t option (** Get the attributes of the procedure. *) - val get_attributes : t -> Sil.proc_attributes + val get_attributes : t -> ProcAttributes.t (** Get the cyclomatic complexity for the procedure *) val get_cyclomatic : t -> int diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index aab726857..3ccc2bc34 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -903,7 +903,10 @@ let pp_cfgnodelabel fmt (n : Cfg.Node.t) = let pp_label fmt n = match Cfg.Node.get_kind n with | Cfg.Node.Start_node (pdesc) -> - let gen = if (Cfg.Procdesc.get_attributes pdesc).Sil.is_generated then " (generated)" else "" in + let gen = + if (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_generated + then " (generated)" + else "" in (* let def = if Cfg.Procdesc.is_defined pdesc then "defined" else "declared" in *) (* Format.fprintf fmt "Start %a (%s)" pp_id (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) def *) Format.fprintf fmt "Start %s%s\\nFormals: %a\\nLocals: %a" diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index c17b53594..1e0348d6f 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -437,7 +437,7 @@ let post_process_procs exe_env procs_done = let check_no_specs pn = if Specs.get_specs pn = [] then begin Errdesc.warning_err - (Specs.get_summary_unsafe pn).Specs.attributes.Sil.loc + (Specs.get_summary_unsafe pn).Specs.attributes.ProcAttributes.loc "No specs found for %a@." Procname.pp pn end in let cg = Exe_env.get_cg exe_env in @@ -583,7 +583,7 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res || not (proc_is_up_to_date call_graph pname)) in let process_one_proc pname (calls: Cg.in_out_calls) = DB.current_source := - (Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file; + (Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file; if !trace then begin let whole_seconds = false in @@ -637,7 +637,7 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res let (pname, weight) = Process.get_last_input p_str in (try DB.current_source := - (Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file; + (Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file; process_result exe_env (pname, weight) summ with exn -> assert false); Timing_log.event_finish (Procname.to_string pname); diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 8731d15f8..5ccdf2989 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -207,7 +207,7 @@ let () = (* parse command-line arguments *) module Simulator = struct (** Simulate the analysis only *) let reset_summaries cg = list_iter - (fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.loc_none) + (fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.dummy) (Cg.get_nodes_and_calls cg) (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 1f2b45419..8b1ba5066 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -245,6 +245,8 @@ type summary_val = (** compute values from summary data to export to csv and xml format *) let summary_values top_proc_set summary = let stats = summary.Specs.stats in + let attributes = summary.Specs.attributes in + let err_log = attributes.ProcAttributes.err_log in let proc_name = Specs.get_proc_name summary in let is_top = Procname.Set.mem proc_name top_proc_set in let signature = Specs.get_signature summary in @@ -283,11 +285,11 @@ let summary_values top_proc_set summary = vsymop = stats.Specs.symops; verr = Errlog.size (fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint) - stats.Specs.err_log; - vflags = summary.Specs.attributes.Sil.proc_flags; - vfile = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file; - vline = summary.Specs.attributes.Sil.loc.Location.line; - vloc = summary.Specs.attributes.Sil.loc.Location.nLOC; + err_log; + vflags = attributes.ProcAttributes.proc_flags; + vfile = DB.source_file_to_string attributes.ProcAttributes.loc.Location.file; + vline = attributes.ProcAttributes.loc.Location.line; + vloc = attributes.ProcAttributes.loc.Location.nLOC; vtop = if is_top then "Y" else "N"; vsignature = signature; vweight = nodes_nr; @@ -402,7 +404,7 @@ module BugsCsv = struct (** Write bug report in csv format *) let pp_bugs error_filter fname fmt summary = let pp x = F.fprintf fmt x in - let err_log = summary.Specs.stats.Specs.err_log in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass = if in_footprint && error_filter error_desc error_name then let err_desc_string = error_desc_to_csv_string error_desc in @@ -415,7 +417,8 @@ module BugsCsv = struct let kind = Exceptions.err_kind_string ekind in let type_str = Localise.to_string error_name in let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in - let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in + let filename = + DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in let always_report = match Localise.error_desc_extract_tag_value error_desc "always_report" with | "" -> "false" @@ -450,13 +453,14 @@ module BugsJson = struct (** Write bug report in JSON format *) let pp_bugs error_filter fname fmt summary = let pp x = F.fprintf fmt x in - let err_log = summary.Specs.stats.Specs.err_log in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass = if in_footprint && error_filter error_desc error_name then let kind = Exceptions.err_kind_string ekind in let bug_type = Localise.to_string error_name in let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in - let file = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in + let file = + DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in let bug = { bug_class = Exceptions.err_class_string eclass; kind = kind; @@ -480,7 +484,7 @@ end module BugsTxt = struct (** Write bug report in text format *) let pp_bugs error_filter fname fmt summary = - let err_log = summary.Specs.stats.Specs.err_log in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass = if in_footprint && error_filter error_desc error_name then Exceptions.pp_err (node_id, node_key) loc ekind error_name error_desc None fmt () in @@ -520,7 +524,7 @@ module BugsXml = struct (** print bugs from summary in xml *) let pp_bugs error_filter linereader fmt summary = - let err_log = summary.Specs.stats.Specs.err_log in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in let do_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass = if in_footprint && error_filter error_desc error_name then let err_desc_string = error_desc_to_xml_string error_desc in @@ -541,7 +545,8 @@ module BugsXml = struct let proc_name = Specs.get_proc_name summary in let procedure_name = Procname.to_string proc_name in let procedure_id = Procname.to_filename proc_name in - let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in + let filename = + DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in let bug_hash = get_bug_hash kind type_str procedure_id filename node_key error_desc in let forest = [ @@ -589,7 +594,7 @@ module CallsCsv = struct pp "\"%s\"," (Escape.escape_csv (Procname.to_filename caller_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_string callee_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_filename callee_name)); - pp "%s," (DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file); + pp "%s," (DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file); pp "%d," loc.Location.line; pp "%a@\n" Specs.CallStats.pp_trace trace in Specs.CallStats.iter do_call stats.Specs.call_stats @@ -606,7 +611,7 @@ module UnitTest = struct let do_spec spec = incr cnt; let c_file = Filename.basename - (DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file) in + (DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file) in let code = Autounit.genunit c_file proc_name !cnt (Specs.get_formals summary) spec in F.fprintf fmt "%a@." Autounit.pp_code code in @@ -734,8 +739,8 @@ module Stats = struct let process_summary error_filter summary linereader stats = let specs = Specs.get_specs_from_payload summary in - let found_errors = - process_err_log error_filter linereader summary.Specs.stats.Specs.err_log stats in + let found_errors = process_err_log + error_filter linereader summary.Specs.attributes.ProcAttributes.err_log stats in let is_defective = found_errors in let is_verified = specs <> [] && not is_defective in let is_checked = not (is_defective || is_verified) in @@ -744,7 +749,7 @@ module Stats = struct if is_verified then stats.nverified <- stats.nverified + 1; if is_checked then stats.nchecked <- stats.nchecked + 1; if is_defective then stats.ndefective <- stats.ndefective + 1; - process_loc summary.Specs.attributes.Sil.loc stats + process_loc summary.Specs.attributes.ProcAttributes.loc stats let num_files stats = Hashtbl.length stats.files @@ -817,7 +822,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let error_filter error_desc error_name = let always_report () = Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in - (filters.Inferconfig.path_filter summary.Specs.attributes.Sil.loc.Location.file + (filters.Inferconfig.path_filter summary.Specs.attributes.ProcAttributes.loc.Location.file || always_report ()) && filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name in do_outf procs_csv (fun outf -> F.fprintf outf.fmt "%a" (ProcsCsv.pp_summary fname top_proc_set) summary); @@ -856,7 +861,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna do_outf xml_out (fun outf -> Dotty.print_specs_xml (Specs.get_signature summary) - specs summary.Specs.attributes.Sil.loc outf.fmt; + specs summary.Specs.attributes.ProcAttributes.loc outf.fmt; close_outf outf) end end @@ -907,12 +912,12 @@ module AnalysisResults = struct let summ_cmp (fname1, summ1) (fname2, summ2) = let n = DB.source_file_compare - summ1.Specs.attributes.Sil.loc.Location.file - summ2.Specs.attributes.Sil.loc.Location.file in + summ1.Specs.attributes.ProcAttributes.loc.Location.file + summ2.Specs.attributes.ProcAttributes.loc.Location.file in if n <> 0 then n else int_compare - summ1.Specs.attributes.Sil.loc.Location.line - summ2.Specs.attributes.Sil.loc.Location.line in + summ1.Specs.attributes.ProcAttributes.loc.Location.line + summ2.Specs.attributes.ProcAttributes.loc.Location.line in list_sort summ_cmp !summaries (** Create an iterator which loads spec files one at a time *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 40ddf8d70..1722f4118 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -982,7 +982,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t re_execution pname let set_current_language cfg proc_desc = - let language = (Cfg.Procdesc.get_attributes proc_desc).Sil.language in + let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in Config.curr_language := language (** reset counters before analysing a procedure *) @@ -1041,7 +1041,7 @@ let remove_this_not_null prop = let report_runtime_exceptions tenv cfg pdesc summary = let pname = Specs.get_proc_name summary in let is_public_method = - (Specs.get_attributes summary).Sil.access = Sil.Public in + (Specs.get_attributes summary).ProcAttributes.access = Sil.Public in let is_main = is_public_method && Procname.is_java pname @@ -1232,12 +1232,14 @@ let do_analysis exe_env = let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *) let calls = get_calls pdesc in let cyclomatic = Cfg.Procdesc.get_cyclomatic pdesc in - let attributes = Cfg.Procdesc.get_attributes pdesc in + let attributes = + { (Cfg.Procdesc.get_attributes pdesc) with + ProcAttributes.err_log = static_err_log; } in Callbacks.proc_inline_synthetic_methods cfg pdesc; Specs.init_summary (dep, nodes, proc_flags, - static_err_log, calls, cyclomatic, None, attributes) in + calls, cyclomatic, None, attributes) in let filter = if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children) else if !Config.only_nospecs then filter_nospecs @@ -1288,6 +1290,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg = else let summary = Specs.get_summary_unsafe proc_name in let stats = summary.Specs.stats in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in incr num_proc; let specs = Specs.get_specs_from_payload summary in tot_specs := (list_length specs) + !tot_specs; @@ -1295,14 +1298,14 @@ let print_stats_cfg proc_shadowed proc_is_active cfg = match specs, Errlog.size (fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint) - stats.Specs.err_log with + err_log with | [], 0 -> incr num_nospec_noerror_proc | _, 0 -> incr num_spec_noerror_proc | [], _ -> incr num_nospec_error_proc | _, _ -> incr num_spec_error_proc in tot_symops := !tot_symops + stats.Specs.symops; if stats.Specs.stats_timeout then incr num_timeout; - Errlog.extend_table err_table stats.Specs.err_log in + Errlog.extend_table err_table err_log in let print_file_stats fmt () = let num_errors = Errlog.err_table_size_footprint Exceptions.Kerror err_table in let num_warnings = Errlog.err_table_size_footprint Exceptions.Kwarning err_table in diff --git a/infer/src/backend/location.ml b/infer/src/backend/location.ml index 1cca459fa..62bc99d16 100644 --- a/infer/src/backend/location.ml +++ b/infer/src/backend/location.ml @@ -26,6 +26,7 @@ let compare loc1 loc2 = (** Dump a location *) let d (loc: t) = L.add_print_action (L.PTloc, Obj.repr loc) +(** Dummy location *) let dummy = { line = -1; col = -1; @@ -36,14 +37,6 @@ let dummy = { let equal loc1 loc2 = compare loc1 loc2 = 0 -(** Unknown location *) -let loc_none = { - line = - 1; - col = - 1; - file = DB.source_file_empty; - nLOC = 0; -} - (** Pretty print a location *) let pp f (loc: t) = F.fprintf f "[line %d]" loc.line diff --git a/infer/src/backend/location.mli b/infer/src/backend/location.mli index f6922f246..5711df7f0 100644 --- a/infer/src/backend/location.mli +++ b/infer/src/backend/location.mli @@ -20,13 +20,11 @@ val compare : t -> t -> int (** Dump a location. *) val d : t -> unit +(** Dummy location *) val dummy : t val equal : t -> t -> bool -(** Unknown location *) -val loc_none : t - (** Pretty print a location. *) val pp : Format.formatter -> t -> unit diff --git a/infer/src/backend/objc_preanal.ml b/infer/src/backend/objc_preanal.ml index ed86c08d4..e6f8ce6cc 100644 --- a/infer/src/backend/objc_preanal.ml +++ b/infer/src/backend/objc_preanal.ml @@ -62,7 +62,7 @@ let fill_generated_proc_map generated_proc_map = let update_generate_proc_map generated_proc_map = let update_generated_pname_to_map cfg source_dir procdesc () = let cfg_pname = Cfg.Procdesc.get_proc_name procdesc in - if not (Cfg.Procdesc.get_attributes procdesc).Sil.is_generated then + if not (Cfg.Procdesc.get_attributes procdesc).ProcAttributes.is_generated then try ignore(Procname.Hash.find generated_proc_map cfg_pname); Procname.Hash.replace generated_proc_map cfg_pname true with Not_found -> () in diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 7d60d5bf9..690060266 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -400,7 +400,7 @@ let c_file_write_html proc_is_active linereader fname tenv cfg = list_iter (fun sp -> proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover) (Specs.get_specs_from_payload summary); - Errlog.update global_err_log summary.Specs.stats.Specs.err_log + 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 diff --git a/infer/src/backend/procAttributes.ml b/infer/src/backend/procAttributes.ml new file mode 100644 index 000000000..2a357ca58 --- /dev/null +++ b/infer/src/backend/procAttributes.ml @@ -0,0 +1,82 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Attributes of a procedure. *) + +module L = Logging +module F = Format +open Utils + +type t = + { + access : Sil.access; (** visibility access *) + captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *) + err_log: Errlog.t; (** Error log for the procedure *) + exceptions : string list; (** exceptions thrown by the procedure *) + formals : (string * Sil.typ) list; (** name and type of formal parameters *) + func_attributes : Sil.func_attribute list; + is_abstract : bool; (** the procedure is abstract *) + mutable is_bridge_method : bool; (** the procedure is a bridge method *) + is_defined : bool; (** true if the procedure is defined, and not just declared *) + is_generated : bool; (** the procedure has been generated *) + is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) + mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) + language : Config.language; (** language of the procedure *) + loc : Location.t; (** location of this procedure in the source code *) + mutable locals : (Mangled.t * Sil.typ) list; (** name and type of local variables *) + method_annotation : Sil.method_annotation; (** annotations for java methods *) + proc_flags : proc_flags; (** flags of the procedure *) + proc_name : Procname.t; (** name of the procedure *) + ret_type : Sil.typ; (** return type *) + } + +let copy pa = + { + access = pa.access; + captured = pa.captured; + err_log = pa.err_log; + exceptions = pa.exceptions; + formals = pa.formals; + func_attributes = pa.func_attributes; + is_abstract = pa.is_abstract; + is_bridge_method = pa.is_bridge_method; + is_defined = pa.is_defined; + is_generated = pa.is_generated; + is_objc_instance_method = pa.is_objc_instance_method; + is_synthetic_method = pa.is_synthetic_method; + language = pa.language; + loc = pa.loc; + locals = pa.locals; + method_annotation = pa.method_annotation; + proc_flags = pa.proc_flags; + proc_name = pa.proc_name; + ret_type = pa.ret_type; + } + +let default proc_name language = { + access = Sil.Default; + formals = []; + captured = []; + err_log = Errlog.empty (); + exceptions = []; + func_attributes = []; + is_abstract = false; + is_defined = false; + is_bridge_method = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language; + loc = Location.dummy; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = Sil.Tvoid; +} diff --git a/infer/src/backend/procAttributes.mli b/infer/src/backend/procAttributes.mli new file mode 100644 index 000000000..399106a8f --- /dev/null +++ b/infer/src/backend/procAttributes.mli @@ -0,0 +1,41 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Attributes of a procedure. *) + +open Utils + +type t = + { + access : Sil.access; (** visibility access *) + captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *) + err_log: Errlog.t; (** Error log for the procedure *) + exceptions : string list; (** exceptions thrown by the procedure *) + formals : (string * Sil.typ) list; (** name and type of formal parameters *) + func_attributes : Sil.func_attribute list; + is_abstract : bool; (** the procedure is abstract *) + mutable is_bridge_method : bool; (** the procedure is a bridge method *) + is_defined : bool; (** true if the procedure is defined, and not just declared *) + is_generated : bool; (** the procedure has been generated *) + is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) + mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) + language : Config.language; (** language of the procedure *) + loc : Location.t; (** location of this procedure in the source code *) + mutable locals : (Mangled.t * Sil.typ) list; (** name and type of local variables *) + method_annotation : Sil.method_annotation; (** annotations for java methods *) + proc_flags : proc_flags; (** flags of the procedure *) + proc_name : Procname.t; (** name of the procedure *) + ret_type : Sil.typ; (** return type *) + } + +(** Create a copy of a proc_attributes *) +val copy : t -> t + +(** Create a proc_attributes with default values. *) +val default : Procname.t -> Config.language -> t diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index e31f66208..9af6014d9 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -834,7 +834,7 @@ let check_inconsistency_base prop = Sil.exp_equal e Sil.exp_zero && Sil.pvar_is_seed pv && Sil.pvar_get_name pv = Mangled.from_string "self" && - procedure_attr.Sil.is_objc_instance_method && + procedure_attr.ProcAttributes.is_objc_instance_method && not (Procname.is_constructor procname) | _ -> false in list_exists do_hpred sigma in diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 16c02d2d9..f20f6d00e 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -31,7 +31,7 @@ let log_issue exn = match Specs.get_summary proc_name with | Some summary -> - let err_log = summary.Specs.stats.Specs.err_log in + let err_log = summary.Specs.attributes.ProcAttributes.err_log in let loc = match loc with | None -> State.get_loc () | Some loc -> loc in diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 1749b97f9..c5a1a7e09 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -678,51 +678,6 @@ and exp = | Lindex of exp * exp (** an array index offset: exp1[exp2] *) | Sizeof of typ * Subtype.t (** a sizeof expression *) -(** Attributes of a procedure. *) -type proc_attributes = - { - access : access; (** visibility access *) - captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *) - exceptions : string list; (** exceptions thrown by the procedure *) - formals : (string * typ) list; (** name and type of formal parameters *) - func_attributes : func_attribute list; - is_abstract : bool; (** the procedure is abstract *) - mutable is_bridge_method : bool; (** the procedure is a bridge method *) - is_defined : bool; (** true if the procedure is defined, and not just declared *) - is_generated : bool; (** the procedure has been generated *) - is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) - mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) - language : Config.language; (** language of the procedure *) - loc : Location.t; (** location of this procedure in the source code *) - mutable locals : (Mangled.t * typ) list; (** name and type of local variables *) - method_annotation : method_annotation; (** annotations for java methods *) - proc_flags : proc_flags; (** flags of the procedure *) - proc_name : Procname.t; (** name of the procedure *) - ret_type : typ; (** return type *) - } - -let copy_proc_attributes pa = - { - access = pa.access; - captured = pa.captured; - exceptions = pa.exceptions; - formals = pa.formals; - func_attributes = pa.func_attributes; - is_abstract = pa.is_abstract; - is_bridge_method = pa.is_bridge_method; - is_defined = pa.is_defined; - is_generated = pa.is_generated; - is_objc_instance_method = pa.is_objc_instance_method; - is_synthetic_method = pa.is_synthetic_method; - language = pa.language; - loc = pa.loc; - locals = pa.locals; - method_annotation = pa.method_annotation; - proc_flags = pa.proc_flags; - proc_name = pa.proc_name; - ret_type = pa.ret_type; - } - (** Kind of prune instruction *) type if_kind = | Ik_bexp (* boolean expressions, and exp ? exp : exp *) diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index fd3135815..8230b62ab 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -313,32 +313,6 @@ and exp = | Lindex of exp * exp (** an array index offset: [exp1\[exp2\]] *) | Sizeof of typ * Subtype.t (** a sizeof expression *) -(** Attributes of a procedure. *) -type proc_attributes = - { - access : access; (** visibility access *) - captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *) - exceptions : string list; (** exceptions thrown by the procedure *) - formals : (string * typ) list; (** name and type of formal parameters *) - func_attributes : func_attribute list; - is_abstract : bool; (** the procedure is abstract *) - mutable is_bridge_method : bool; (** the procedure is a bridge method *) - is_defined : bool; (** true if the procedure is defined, and not just declared *) - is_generated : bool; (** the procedure has been generated *) - is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) - mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) - language : Config.language; (** language of the procedure *) - loc : Location.t; (** location of this procedure in the source code *) - mutable locals : (Mangled.t * typ) list; (** name and type of local variables *) - method_annotation : method_annotation; (** annotations for java methods *) - proc_flags : proc_flags; (** flags of the procedure *) - proc_name : Procname.t; (** name of the procedure *) - ret_type : typ; (** return type *) - } - -(** Create a copy of a proc_attributes *) -val copy_proc_attributes : proc_attributes -> proc_attributes - (** Sets of types. *) module TypSet : Set.S with type elt = typ diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 8f226efbb..8d36dd11d 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -291,7 +291,6 @@ type stats = stats_timeout: bool; (** Flag to indicate whether a timeout occurred *) stats_calls: Cg.in_out_calls; (** num of procs calling, and called *) symops: int; (** Number of SymOp's throughout the whole analysis of the function *) - err_log: Errlog.t; (** Error log for the procedure *) mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *) mutable nodes_visited_re : IntSet.t; (** Nodes visited during the re-execution phase *) call_stats : call_stats; @@ -320,7 +319,7 @@ type summary = stats: stats; (** statistics: execution time and list of errors *) status: status; (** ACTIVE when the proc is being analyzed *) timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) - attributes : Sil.proc_attributes; (** Attributes of the procedure *) + attributes : ProcAttributes.t; (** Attributes of the procedure *) } (** origin of a summary: current results dir, a spec library, or models *) @@ -344,9 +343,9 @@ let pp_timeout fmt = function | true -> F.fprintf fmt "Y" | false -> F.fprintf fmt "N" -let pp_stats whole_seconds fmt stats = +let pp_stats err_log whole_seconds fmt stats = F.fprintf fmt "TIME:%a TIMEOUT:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds) stats.stats_time pp_timeout stats.stats_timeout stats.symops stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls; - F.fprintf fmt "ERRORS: @[%a@]" Errlog.pp stats.err_log + F.fprintf fmt "ERRORS: @[%a@]" Errlog.pp err_log (** Print the spec *) let pp_spec pe num_opt fmt spec = @@ -406,11 +405,11 @@ let get_signature summary = let pp_name f () = F.fprintf f "%s" p in let pp f () = Sil.pp_type_decl pe_text pp_name Sil.pp_exp f typ in let decl = pp_to_string pp () in - s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.Sil.formals; + s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.ProcAttributes.formals; let pp_procname f () = F.fprintf f "%a" - Procname.pp summary.attributes.Sil.proc_name in + Procname.pp summary.attributes.ProcAttributes.proc_name in let pp f () = - Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.attributes.Sil.ret_type in + Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.attributes.ProcAttributes.ret_type in let decl = pp_to_string pp () in decl ^ "(" ^ !s ^ ")" @@ -422,24 +421,26 @@ let pp_summary_no_stats_specs fmt summary = F.fprintf fmt "%a@\n" pp_pair (describe_phase summary); F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map -let pp_stats_html fmt stats = - Errlog.pp_html [] fmt stats.err_log +let pp_stats_html err_log fmt stats = + Errlog.pp_html [] fmt err_log let get_specs_from_payload summary = match summary.payload with | PrePosts specs -> NormSpec.tospecs specs | TypeState _ -> [] (** Print the summary *) -let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with +let pp_summary pe whole_seconds fmt summary = + let err_log = summary.attributes.ProcAttributes.err_log in + match pe.pe_kind with | PP_TEXT -> pp_summary_no_stats_specs fmt summary; - F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats; + F.fprintf fmt "%a@\n" (pp_stats err_log whole_seconds) summary.stats; F.fprintf fmt "%a" (pp_specs pe) (get_specs_from_payload summary) | PP_HTML -> Io_infer.Html.pp_start_color fmt Black; F.fprintf fmt "@\n%a" pp_summary_no_stats_specs summary; Io_infer.Html.pp_end_color fmt (); - pp_stats_html fmt summary.stats; + pp_stats_html err_log fmt summary.stats; Io_infer.Html.pp_hline fmt (); F.fprintf fmt "@\n"; pp_specs pe fmt (get_specs_from_payload summary); @@ -447,7 +448,7 @@ let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with | PP_LATEX -> F.fprintf fmt "\\begin{verbatim}@\n"; pp_summary_no_stats_specs fmt summary; - F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats; + F.fprintf fmt "%a@\n" (pp_stats err_log whole_seconds) summary.stats; F.fprintf fmt "\\end{verbatim}@\n"; F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary) @@ -455,7 +456,7 @@ let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with let pp_spec_table pe whole_seconds fmt () = Procname.Hash.iter (fun proc_name (summ, orig) -> F.fprintf fmt "PROC %a@\n%a@\n" Procname.pp proc_name (pp_summary pe whole_seconds) summ) spec_tbl -let empty_stats err_log calls cyclomatic in_out_calls_opt = +let empty_stats calls cyclomatic in_out_calls_opt = { stats_time = 0.0; stats_timeout = false; stats_calls = @@ -463,7 +464,6 @@ let empty_stats err_log calls cyclomatic in_out_calls_opt = | Some in_out_calls -> in_out_calls | None -> { Cg.in_calls = 0; Cg.out_calls = 0 }); symops = 0; - err_log = err_log; nodes_visited_fp = IntSet.empty; nodes_visited_re = IntSet.empty; call_stats = CallStats.init calls; @@ -627,7 +627,7 @@ let proc_is_library proc_name proc_desc = else false (** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *) -let proc_get_attributes proc_name proc_desc : Sil.proc_attributes = +let proc_get_attributes proc_name proc_desc : ProcAttributes.t = let from_proc_desc = Cfg.Procdesc.get_attributes proc_desc in let defined = Cfg.Procdesc.is_defined proc_desc in if not defined then @@ -638,7 +638,7 @@ let proc_get_attributes proc_name proc_desc : Sil.proc_attributes = else from_proc_desc let proc_get_method_annotation proc_name proc_desc = - (proc_get_attributes proc_name proc_desc).Sil.method_annotation + (proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation let get_origin proc_name = match get_summary_origin proc_name with @@ -663,13 +663,13 @@ let get_timestamp summary = summary.timestamp let get_proc_name summary = - summary.attributes.Sil.proc_name + summary.attributes.ProcAttributes.proc_name let get_ret_type summary = - summary.attributes.Sil.ret_type + summary.attributes.ProcAttributes.ret_type let get_formals summary = - summary.attributes.Sil.formals + summary.attributes.ProcAttributes.formals let get_attributes summary = summary.attributes @@ -680,7 +680,7 @@ let get_flag proc_name key = match get_summary proc_name with | None -> None | Some summary -> - let proc_flags = summary.attributes.Sil.proc_flags in + let proc_flags = summary.attributes.ProcAttributes.proc_flags in try Some (Hashtbl.find proc_flags key) with Not_found -> None @@ -692,7 +692,7 @@ let get_iterations proc_name = | None -> raise (Failure ("Specs.get_iterations: " ^ (Procname.to_string proc_name) ^ "Not_found")) | Some summary -> - let proc_flags = summary.attributes.Sil.proc_flags in + let proc_flags = summary.attributes.ProcAttributes.proc_flags in try let time_str = Hashtbl.find proc_flags proc_flag_iterations in Pervasives.int_of_string time_str @@ -747,11 +747,11 @@ let update_dependency_map proc_name = set_summary_origin proc_name { summary with dependency_map = current_dependency_map } origin (** [init_summary (depend_list, nodes, - proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, proc_attributes)] + proc_flags, calls, cyclomatic, in_out_calls_opt, proc_attributes)] initializes the summary for [proc_name] given dependent procs in list [depend_list]. *) let init_summary (depend_list, nodes, - proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, + proc_flags, calls, cyclomatic, in_out_calls_opt, proc_attributes) = let dependency_map = mk_initial_dependency_map depend_list in let summary = @@ -761,42 +761,24 @@ let init_summary phase = FOOTPRINT; sessions = ref 0; payload = PrePosts []; - stats = empty_stats initial_err_log calls cyclomatic in_out_calls_opt; + stats = empty_stats calls cyclomatic in_out_calls_opt; status = INACTIVE; timestamp = 0; attributes = { proc_attributes with - Sil.proc_flags = proc_flags; }; + ProcAttributes.proc_flags = proc_flags; }; } in - Procname.Hash.replace spec_tbl proc_attributes.Sil.proc_name (summary, Res_dir) + Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir) let reset_summary call_graph proc_name loc = let dependents = Cg.get_defined_children call_graph proc_name in - let proc_attributes = { - Sil.access = Sil.Default; - formals = []; - captured = []; - exceptions = []; - func_attributes = []; - is_abstract = false; - is_defined = false; - is_bridge_method = false; - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = !Config.curr_language; - loc; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; - ret_type = Sil.Tvoid; - } in + let proc_attributes = + { (ProcAttributes.default proc_name !Config.curr_language) with + loc; } in init_summary ( Procname.Set.elements dependents, [], proc_flags_empty (), - Errlog.empty (), [], 0, Some (Cg.get_calls call_graph proc_name), diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 332704326..7ca19b75e 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -105,7 +105,6 @@ type stats = stats_timeout: bool; (** Flag to indicate whether a timeout occurred *) stats_calls: Cg.in_out_calls; (** num of procs calling, and called *) symops: int; (** Number of SymOp's throughout the whole analysis of the function *) - err_log: Errlog.t; (** Error log for the procedure *) mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *) mutable nodes_visited_re : IntSet.t; (** Nodes visited during the re-execution phase *) call_stats : CallStats.t; @@ -133,7 +132,7 @@ type summary = stats: stats; (** statistics: execution time and list of errors *) status: status; (** ACTIVE when the proc is being analyzed *) timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) - attributes : Sil.proc_attributes; (** Attributes of the procedure *) + attributes : ProcAttributes.t; (** Attributes of the procedure *) } (** origin of a summary: current results dir, a spec library, or models *) @@ -161,7 +160,7 @@ val d_spec : 'a spec -> unit val get_proc_name : summary -> Procname.t (** Get the attributes of the procedure. *) -val get_attributes : summary -> Sil.proc_attributes +val get_attributes : summary -> ProcAttributes.t (** Get the return type of the procedure *) val get_ret_type : summary -> Sil.typ @@ -217,11 +216,10 @@ val init_summary : (Procname.t list * (** depend list *) int list * (** nodes *) proc_flags * (** procedure flags *) - Errlog.t * (** initial error log *) (Procname.t * Location.t) list * (** calls *) int * (** cyclomatic *) (Cg.in_out_calls option) * (** in and out calls *) - Sil.proc_attributes) (** attributes of the procedure *) + ProcAttributes.t) (** attributes of the procedure *) -> unit val reset_summary : Cg.t -> Procname.t -> Location.t -> unit @@ -248,7 +246,7 @@ val pp_specs : printenv -> Format.formatter -> Prop.normal spec list -> unit val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit (** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *) -val proc_get_attributes : Procname.t -> Cfg.Procdesc.t -> Sil.proc_attributes +val proc_get_attributes : Procname.t -> Cfg.Procdesc.t -> ProcAttributes.t val proc_get_method_annotation : Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 01c09dd05..96b859a6a 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -524,7 +524,7 @@ let call_should_be_skipped callee_pname summary = (* check skip flag *) || Specs.get_flag callee_pname proc_flag_skip <> None (* skip abstract methods *) - || summary.Specs.attributes.Sil.is_abstract + || summary.Specs.attributes.ProcAttributes.is_abstract (* treat calls with no specs as skip functions in angelic mode *) || (!Config.angelic_execution && Specs.get_specs_from_payload summary == []) @@ -643,12 +643,11 @@ let proc_desc_copy cfg pdesc pname pname' = (match Cfg.Procdesc.find_from_name cfg pname' with | Some pdesc' -> pdesc' | None -> - let open Cfg.Procdesc in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes = - { (Sil.copy_proc_attributes (get_attributes pdesc)) with - Sil.proc_name = pname'; }; + { (ProcAttributes.copy (Cfg.Procdesc.get_attributes pdesc)) with + ProcAttributes.proc_name = pname'; }; }) let method_exists right_proc_name methods = @@ -1257,7 +1256,8 @@ and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_p | None -> [(prop, path)] | Some callee_pdesc -> let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in - match Sil.get_sentinel_func_attribute_value proc_attributes.Sil.func_attributes with + match Sil.get_sentinel_func_attribute_value + proc_attributes.ProcAttributes.func_attributes with | None -> [(prop, path)] | Some sentinel_arg -> let formals = Cfg.Procdesc.get_formals callee_pdesc in @@ -1317,7 +1317,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = (* In case we call an objc instance method we add and extra spec *) (* were the receiver is null and the semantics of the call is nop*) if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics && - (Specs.get_attributes summary).Sil.is_objc_instance_method then + (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path else (* non-objective-c method call. Standard tabulation *) Tabulation.exe_function_call tenv cfg ret_ids pdesc callee_pname loc actual_params pre path diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 8f2af663b..ff60241b9 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -32,7 +32,7 @@ end (* PP *) (** State that persists in the .specs files. *) module ST = struct let add summary key value = - proc_flags_add summary.Specs.attributes.Sil.proc_flags key value + proc_flags_add summary.Specs.attributes.ProcAttributes.proc_flags key value let pname_add proc_name key value = let summary = Specs.get_summary_unsafe proc_name in @@ -43,14 +43,14 @@ module ST = struct let pname_find proc_name key = if Procname.Set.mem proc_name !files_open then let summary = Specs.get_summary_unsafe proc_name in - proc_flags_find summary.Specs.attributes.Sil.proc_flags key + proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key else begin match Specs.get_summary proc_name with | None -> raise Not_found | Some summary -> begin files_open := Procname.Set.add proc_name !files_open; - proc_flags_find summary.Specs.attributes.Sil.proc_flags key + proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key end end diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 3c2c7e9da..34e801cc3 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -49,7 +49,7 @@ module Err = struct let new_summ = { old_summ with Specs.attributes = { old_summ.Specs.attributes with - Sil.loc = Cfg.Procdesc.get_loc proc_desc }; + ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc }; Specs.nodes = nodes; Specs.payload = Specs.PrePosts specs } in Specs.add_summary proc_name new_summ diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index 611fcf1b4..def42c9ab 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -54,7 +54,7 @@ struct let old_summ = Specs.get_summary_unsafe proc_name in let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in let method_annotation = - (Specs.proc_get_attributes proc_name proc_desc).Sil.method_annotation in + (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation in let new_summ = { old_summ with @@ -63,7 +63,7 @@ struct Specs.attributes = { old_summ.Specs.attributes with - Sil.loc = Cfg.Procdesc.get_loc proc_desc; + ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc; method_annotation; }; } in @@ -177,7 +177,8 @@ struct let do_proc (init_pn, init_pd) = let filter callee_pn callee_pd = let is_private = - (Specs.proc_get_attributes callee_pn callee_pd).Sil.access = Sil.Private in + let attr = Specs.proc_get_attributes callee_pn callee_pd in + attr.ProcAttributes.access = Sil.Private in let same_class = let get_class_opt pn = if Procname.is_java pn then Some (Procname.java_get_class pn) @@ -305,12 +306,12 @@ struct let filter_special_cases () = if Procname.java_is_access_method proc_name || - (Specs.proc_get_attributes proc_name proc_desc).Sil.is_bridge_method + (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_bridge_method then None else begin let annotated_signature = Models.get_annotated_signature proc_desc proc_name in - if (Specs.proc_get_attributes proc_name proc_desc).Sil.is_abstract then + if (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_abstract then begin if Models.infer_library_return && EradicateChecks.classify_procedure proc_name proc_desc = "L" then diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index 223f69a05..2c6f01eb7 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -383,7 +383,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc let visible_params = list_drop_first n params in (* Drop the trailing hidden parameter if the constructor is synthetic. *) - if (Cfg.Procdesc.get_attributes pdesc).Sil.is_synthetic_method then + if (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then list_drop_last 1 visible_params else visible_params @@ -395,7 +395,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc (* Drop parameters from the signature which we do not check in a call. *) let drop_unchecked_signature_params pdesc pname annotated_signature = if Procname.is_constructor pname && - (Cfg.Procdesc.get_attributes pdesc).Sil.is_synthetic_method then + (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then list_drop_last 1 annotated_signature.Annotations.params else annotated_signature.Annotations.params in @@ -947,7 +947,7 @@ let typecheck_node let exceptions = match get_proc_desc callee_pname with | Some callee_pdesc -> - (Specs.proc_get_attributes callee_pname callee_pdesc).Sil.exceptions + (Specs.proc_get_attributes callee_pname callee_pdesc).ProcAttributes.exceptions | None -> [] in if exceptions <> [] then typestates_exn := typestate :: !typestates_exn diff --git a/infer/src/clang/cEnum_decl.ml b/infer/src/clang/cEnum_decl.ml index b9c363cf5..3dec73c5e 100644 --- a/infer/src/clang/cEnum_decl.ml +++ b/infer/src/clang/cEnum_decl.ml @@ -15,30 +15,9 @@ open CFrontend_utils let create_empty_procdesc () = let proc_name = Procname.from_string_c_fun "__INFER_$GLOBAL_VAR_env" in - let open Cfg.Procdesc in - let proc_attributes = - { - Sil.access = Sil.Default; - captured = []; - exceptions = []; - formals = []; - func_attributes = []; - is_abstract = false; - is_bridge_method = false; - is_defined = false; - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = Config.C_CPP; - loc = Location.loc_none; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; - ret_type = Sil.Tvoid; - } in - create { - cfg = Cfg.Node.create_cfg (); + let proc_attributes = ProcAttributes.default proc_name Config.C_CPP in + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = Cfg.Node.create_cfg (); proc_attributes = proc_attributes; } diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 85c7c24d9..3d319922e 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -229,7 +229,7 @@ let should_create_procdesc cfg procname defined generated = | Some prevoius_procdesc -> let is_defined_previous = Cfg.Procdesc.is_defined prevoius_procdesc in let is_generated_previous = - (Cfg.Procdesc.get_attributes prevoius_procdesc).Sil.is_generated in + (Cfg.Procdesc.get_attributes prevoius_procdesc).ProcAttributes.is_generated in if defined && ((not is_defined_previous) || (generated && is_generated_previous)) then (Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name prevoius_procdesc) true; @@ -256,32 +256,19 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let ret_type = get_return_type tenv ms in let captured' = list_map (fun (s, t, _) -> (s, t)) captured in let procdesc = - (* This part below is a boilerplate and the following list of *) - (* instructions should be moved in the Cfg.Procdesc module *) - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = Sil.Default; - captured = captured'; - exceptions = []; + { (ProcAttributes.default proc_name Config.C_CPP) with + ProcAttributes.captured = captured'; formals; func_attributes = attributes; - is_abstract = false; - is_bridge_method = false; is_defined = defined; is_generated; is_objc_instance_method = is_objc_inst_method; - is_synthetic_method = false; - language = Config.C_CPP; loc = loc_start; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; ret_type; } in - create { - cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg; proc_attributes; } in if defined then @@ -308,32 +295,17 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = | Some (ret_type, arg_types) -> ret_type, list_map (fun typ -> ("x", typ)) arg_types | None -> Sil.Tvoid, []) in - let loc = Location.loc_none in + let loc = Location.dummy in let _ = - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = Sil.Default; - captured = []; - exceptions = []; - formals; - func_attributes = []; - is_abstract = false; - is_bridge_method = false; - is_defined = false; - is_generated = false; + { (ProcAttributes.default proc_name Config.C_CPP) with + ProcAttributes.formals; is_objc_instance_method = is_objc_inst_method; - is_synthetic_method = false; - language = Config.C_CPP; loc; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; ret_type; } in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes = proc_attributes; } in () diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 7029ea11a..bf5b7f26a 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -278,30 +278,14 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = let formals = let param_strs = Procname.java_get_parameters proc_name in list_fold_right (fun typ_str params -> ("", lookup_typ typ_str) :: params) param_strs [] in - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = Sil.Default; - captured = []; - exceptions = []; - formals; - func_attributes = []; - is_abstract = false; - is_defined = false; - is_bridge_method = false; - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = Config.Java; + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.formals; loc; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; ret_type; } in - create { - cfg = harness_cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = harness_cfg; proc_attributes = proc_attributes; } in list_iter (fun p -> @@ -331,30 +315,13 @@ let setup_harness_cfg harness_name harness_cfg env proc_file_map tenv = | None -> assert false in let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in let procdesc = - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = Sil.Default; - captured = []; - exceptions = []; - formals = []; - func_attributes = []; - is_abstract = false; - is_bridge_method = false; - is_defined = true; - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = Config.Java; + { (ProcAttributes.default harness_name Config.Java) with + ProcAttributes.is_defined = true; loc = env.pc; - locals = []; - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name = harness_name; - ret_type = Sil.Tvoid; } in - create { - cfg = harness_cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = harness_cfg; proc_attributes; } in let harness_node = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 00f271746..46cd0514b 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -286,30 +286,20 @@ let create_local_procdesc program linereader cfg tenv node m = let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in let method_annotation = JAnnotation.translate_method am.Javalib.am_annotations in let procdesc = - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = trans_access am.Javalib.am_access; - captured = []; + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access am.Javalib.am_access; exceptions = list_map JBasics.cn_name am.Javalib.am_exceptions; formals; - func_attributes = []; is_abstract = true; is_bridge_method = am.Javalib.am_bridge; is_defined = true; - is_generated = false; - is_objc_instance_method = false; is_synthetic_method = am.Javalib.am_synthetic; - language = Config.Java; - loc = Location.dummy; - locals = []; method_annotation; - proc_flags = proc_flags_empty (); - proc_name; ret_type = JTransType.return_type program tenv ms meth_kind; } in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes; } in let start_kind = Cfg.Node.Start_node procdesc in @@ -323,30 +313,18 @@ let create_local_procdesc program linereader cfg tenv node m = let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in let method_annotation = JAnnotation.translate_method cm.Javalib.cm_annotations in let _procdesc = - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = trans_access cm.Javalib.cm_access; - captured = []; + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access cm.Javalib.cm_access; exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; formals; - func_attributes = []; - is_abstract = false; is_bridge_method = cm.Javalib.cm_bridge; - is_defined = false; - is_generated = false; - is_objc_instance_method = false; is_synthetic_method = cm.Javalib.cm_synthetic; - language = Config.Java; - loc = Location.dummy; - locals = []; method_annotation; - proc_flags = proc_flags_empty (); - proc_name; ret_type = JTransType.return_type program tenv ms meth_kind; } in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes = proc_attributes; } in () @@ -361,30 +339,21 @@ let create_local_procdesc program linereader cfg tenv node m = update_constr_loc cn ms loc_start; update_init_loc cn ms loc_exit; let procdesc = - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = trans_access cm.Javalib.cm_access; - captured = []; + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access cm.Javalib.cm_access; exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; formals; - func_attributes = []; - is_abstract = false; is_bridge_method = cm.Javalib.cm_bridge; is_defined = true; - is_generated = false; - is_objc_instance_method = false; is_synthetic_method = cm.Javalib.cm_synthetic; - language = Config.Java; loc = loc_start; locals; method_annotation; - proc_flags = proc_flags_empty (); - proc_name; ret_type = JTransType.return_type program tenv ms meth_kind; } in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes = proc_attributes; } in let start_kind = Cfg.Node.Start_node procdesc in @@ -410,7 +379,7 @@ let create_local_procdesc program linereader cfg tenv node m = create_new_procdesc () end -let create_external_procdesc program cfg tenv cn ms method_annotation kind = +let create_external_procdesc program cfg tenv cn ms kind = let return_type = match JBasics.ms_rtype ms with | None -> Sil.Tvoid @@ -418,30 +387,13 @@ let create_external_procdesc program cfg tenv cn ms method_annotation kind = let formals = formals_from_signature program tenv cn ms kind in let proc_name = JTransType.get_method_procname cn ms kind in ignore ( - let open Cfg.Procdesc in let proc_attributes = - { - Sil.access = Sil.Default; - captured = []; - exceptions = []; - formals; - func_attributes = []; - is_abstract = false; - is_bridge_method = false; - is_defined = false; - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = Config.Java; - loc = Location.dummy; - locals = []; - method_annotation; - proc_flags = proc_flags_empty (); - proc_name; + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.formals; ret_type = return_type; } in - create { - cfg = cfg; + Cfg.Procdesc.create { + Cfg.Procdesc.cfg = cfg; proc_attributes = proc_attributes; }) @@ -450,7 +402,7 @@ let rec get_method_procdesc program cfg tenv cn ms kind = let procname = JTransType.get_method_procname cn ms kind in match lookup_procdesc cfg procname with | Unknown -> - create_external_procdesc program cfg tenv cn ms Sil.method_annotation_empty kind; + create_external_procdesc program cfg tenv cn ms kind; get_method_procdesc program cfg tenv cn ms kind | Created status -> status diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index a5862841d..d6a346b9e 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -120,30 +120,17 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) match ret_tp_opt with | None -> Sil.Tvoid | Some ret_tp -> trans_typ ret_tp in - let (proc_attrs : Sil.proc_attributes) = + let (proc_attrs : ProcAttributes.t) = let open Sil in - { access = Sil.Default; - captured = []; - exceptions = []; - formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params; - func_attributes = []; - is_abstract = false; - is_bridge_method = false; + { (ProcAttributes.default proc_name Config.C_CPP) with + ProcAttributes.formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params; is_defined = true; (** is defined and not just declared *) - is_generated = false; - is_objc_instance_method = false; - is_synthetic_method = false; - language = Config.C_CPP; loc = source_only_location (); locals = []; (* TODO *) - method_annotation = Sil.method_annotation_empty; - proc_flags = proc_flags_empty (); - proc_name; ret_type; } in let (procdesc_builder : Cfg.Procdesc.proc_desc_builder) = - let open Cfg.Procdesc in - { cfg = cfg; + { Cfg.Procdesc.cfg = cfg; proc_attributes = proc_attrs; } in let procdesc = Cfg.Procdesc.create procdesc_builder in