[backend] Extend results directory with attributes for each procedure.

infer/src/backend/DB.ml

@@ -292,6 +292,7 @@ module Results_dir = struct
   let init () =
     create_dir !Config.results_dir;
     create_dir (specs_dir ());
+    create_dir (path_to_filename Abs_root [Config.attributes_dir_name]);
     create_dir (path_to_filename Abs_root [Config.sources_dir_name]);
     create_dir (path_to_filename Abs_root [Config.captured_dir_name]);
     if not (source_file_equal !current_source source_file_empty) then

infer/src/backend/attributesTable.ml

@@ -0,0 +1,39 @@
+(*
+ * 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.
+ *)
+
+open Utils
+module F = Format
+module L = Logging
+
+(** Module to manage the table of attributes. *)
+
+let serializer : ProcAttributes.t Serialization.serializer =
+  Serialization.create_serializer Serialization.attributes_key
+
+let attributes_filename pname =
+  let pname_file = Procname.to_filename pname in
+  pname_file ^ ".attr"
+
+(** path to the .attr file for the given procedure in the current results directory *)
+let res_dir_attr_filename pname =
+  DB.Results_dir.path_to_filename
+    DB.Results_dir.Abs_root [Config.attributes_dir_name; attributes_filename pname]
+
+let store_attributes proc_attributes =
+  let proc_name = proc_attributes.ProcAttributes.proc_name in
+  let attributes_file = res_dir_attr_filename proc_name in
+  let should_write = (* only overwrite defined procedures *)
+    proc_attributes.ProcAttributes.is_defined ||
+    not (DB.file_exists attributes_file) in
+  if should_write then
+    Serialization.to_file serializer attributes_file proc_attributes
+
+let load_attributes proc_name =
+  let attributes_file = res_dir_attr_filename proc_name in
+  Serialization.from_file serializer attributes_file

infer/src/backend/attributesTable.mli

@@ -0,0 +1,17 @@
+(*
+ * 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.
+ *)
+
+(** Module to manage the table of attributes. *)
+
+
+(** Save .attr file for the procedure into the attributes database. *)
+val store_attributes : ProcAttributes.t -> unit
+
+(** Load the attributes for the procedure from the attributes database. *)
+val load_attributes : Procname.t -> ProcAttributes.t option

infer/src/backend/callbacks.ml

@@ -138,11 +138,13 @@ let iterate_procedure_callbacks all_procs exe_env proc_name =
     Cfg.Procdesc.find_from_name cfg proc_name in
 
   let update_time proc_name elapsed =
-    let prev_summary = Specs.get_summary_unsafe proc_name in
+    match Specs.get_summary proc_name with
-    let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
+    | Some prev_summary ->
-    let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
+        let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
-    let summary = { prev_summary with Specs.stats = stats } in
+        let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
-    Specs.add_summary proc_name summary in
+        let summary = { prev_summary with Specs.stats = stats } in
+        Specs.add_summary proc_name summary
+    | None -> () in
 
   Option.may
     (fun (idenv, tenv, proc_name, proc_desc, language) ->
@@ -213,16 +215,8 @@ let iterate_callbacks store_summary call_graph exe_env =
     (* Return all values of the map *)
     list_map snd (StringMap.bindings cluster_map) in
   let reset_summary proc_name =
-    let cfg_opt =
-      try
-        Some (Exe_env.get_cfg exe_env proc_name) with
-      | Not_found -> None in
-    let procdesc_opt = match cfg_opt with
-      | Some cfg ->
-          Cfg.Procdesc.find_from_name cfg proc_name
-      | None -> None in
     let attributes_opt =
-      Option.map Cfg.Procdesc.get_attributes procdesc_opt in
+      Specs.proc_resolve_attributes proc_name in
     Specs.reset_summary call_graph proc_name attributes_opt in
 
 

infer/src/backend/cfg.ml

@@ -118,36 +118,6 @@ module Node = struct
       with Not_found -> () in
     Procname.Hash.iter mark_pdesc_if_unchanged new_procs
 
-  let compute_enabled_verbose = false
-
-  (** restrict the cfg to the given enabled (active and not shadowed) procedures *)
-  let cfg_restrict_enabled cfg source enabled =
-    match enabled with
-    | None -> ()
-    | Some enabled_procs ->
-        if compute_enabled_verbose then L.err "cfg_restrict_enabled: checking enabled in %s@." (DB.source_file_to_string source);
-        let is_enabled pname = Procname.Set.mem pname enabled_procs in
-        let in_address_set pname = Procname.Set.mem pname cfg.priority_set in
-        let node_list' =
-          let filter_node node = match node.nd_proc with
-            | None -> true
-            | 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.ProcAttributes.is_defined &&
-               not (is_enabled pname) &&
-               not (in_address_set pname) then
-              psetr := Procname.Set.add pname !psetr in
-          Procname.Hash.iter do_proc cfg.name_pdesc_tbl;
-          !psetr in
-        let remove_proc pname =
-          if compute_enabled_verbose then L.err "cfg_restrict_enabled: Removing proc not enabled from the cfg: %s@." (Procname.to_filename pname);
-          Procname.Hash.remove cfg.name_pdesc_tbl pname in
-        cfg.node_list := node_list';
-        Procname.Set.iter remove_proc procs_to_remove
-
   let node_id_gen cfg = incr cfg.node_id; !(cfg.node_id)
 
   let pdesc_tbl_add cfg proc_name proc_desc =
@@ -638,42 +608,6 @@ end
 type node = Node.t
 type cfg = Node.cfg
 
-(** Serializer for control flow graphs *)
-let cfg_serializer : cfg Serialization.serializer = Serialization.create_serializer Serialization.cfg_key
-
-(** Load a cfg from a file *)
-let load_cfg_from_file (filename : DB.filename) : cfg option =
-  Serialization.from_file cfg_serializer filename
-
-(** save a copy in the results dir of the source files of procedures defined in the cfg, unless an updated copy already exists *)
-let save_source_files cfg =
-  let process_proc pname pdesc =
-    let loc = Node.proc_desc_get_loc pdesc in
-    let source_file = loc.Location.file in
-    let source_file_str = DB.source_file_to_abs_path source_file in
-    let dest_file = DB.source_file_in_resdir source_file in
-    let dest_file_str = DB.filename_to_string dest_file in
-    let needs_copy =
-      Node.proc_desc_is_defined pdesc &&
-      Sys.file_exists source_file_str &&
-      (not (Sys.file_exists dest_file_str) ||
-       DB.file_modified_time (DB.filename_from_string source_file_str) > DB.file_modified_time dest_file) in
-    if needs_copy then
-      match Utils.copy_file source_file_str dest_file_str with
-      | Some _ -> ()
-      | None -> L.err "Error cannot create copy of source file %s@." source_file_str in
-  Node.iter_proc_desc cfg process_proc
-
-(** Save a cfg into a file *)
-let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg: cfg) =
-  if save_sources then save_source_files cfg;
-  if !Config.incremental_procs then
-    begin
-      match load_cfg_from_file filename with
-      | Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg
-      | None -> ()
-    end;
-  Serialization.to_file cfg_serializer filename cfg
 
 (* =============== START of module Procdesc =============== *)
 module Procdesc = struct
@@ -1000,3 +934,66 @@ let remove_seed_captured_vars_block captured_vars prop =
   let sigma = Prop.get_sigma prop in
   let sigma' = list_filter (fun hpred -> not (hpred_seed_captured hpred)) sigma in
   Prop.normalize (Prop.replace_sigma sigma' prop)
+
+(** Serializer for control flow graphs *)
+let cfg_serializer : cfg Serialization.serializer =
+  Serialization.create_serializer Serialization.cfg_key
+
+(** Load a cfg from a file *)
+let load_cfg_from_file (filename : DB.filename) : cfg option =
+  Serialization.from_file cfg_serializer filename
+
+(** save a copy in the results dir of the source files of procedures defined in the cfg,
+    unless an updated copy already exists *)
+let save_source_files cfg =
+  let process_proc pname pdesc =
+    let loc = Node.proc_desc_get_loc pdesc in
+    let source_file = loc.Location.file in
+    let source_file_str = DB.source_file_to_abs_path source_file in
+    let dest_file = DB.source_file_in_resdir source_file in
+    let dest_file_str = DB.filename_to_string dest_file in
+    let needs_copy =
+      Node.proc_desc_is_defined pdesc &&
+      Sys.file_exists source_file_str &&
+      (not (Sys.file_exists dest_file_str) ||
+       DB.file_modified_time (DB.filename_from_string source_file_str)
+       >
+       DB.file_modified_time dest_file) in
+    if needs_copy then
+      match Utils.copy_file source_file_str dest_file_str with
+      | Some _ -> ()
+      | None -> L.err "Error cannot create copy of source file %s@." source_file_str in
+  Node.iter_proc_desc cfg process_proc
+
+(** Save the .attr files for the procedures in the cfg. *)
+let save_attributes filename cfg =
+  let save_proc proc_desc =
+    let attributes = Procdesc.get_attributes proc_desc in
+    let loc = attributes.ProcAttributes.loc in
+    let attributes' =
+      if Location.equal loc Location.dummy then
+        let loc' = {loc with Location.file = !DB.current_source } in
+        {attributes with ProcAttributes.loc = loc'}
+      else
+        attributes in
+    (*
+    L.stderr "save_proc@.  proc_name:%a@.  filename:%s@.  current_source:%s@.  loc:%s@."
+      Procname.pp (Procdesc.get_proc_name proc_desc)
+      (DB.filename_to_string filename)
+      (DB.source_file_to_string !DB.current_source)
+      (Location.to_string loc);
+    *)
+    AttributesTable.store_attributes attributes' in
+  list_iter save_proc (get_all_procs cfg)
+
+(** Save a cfg into a file *)
+let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg) =
+  if save_sources then save_source_files cfg;
+  if !Config.incremental_procs then
+    begin
+      match load_cfg_from_file filename with
+      | Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg
+      | None -> ()
+    end;
+  save_attributes filename cfg;
+  Serialization.to_file cfg_serializer filename cfg

infer/src/backend/cfg.mli

@@ -157,9 +157,6 @@ module Node : sig
   (** Add declarations for local variables and return variable to the node *)
   val add_locals_ret_declaration : t -> (Mangled.t * Sil.typ) list -> unit
 
-  (** restrict the cfg to the given enabled (active and not shadowed) procedures *)
-  val cfg_restrict_enabled : cfg -> DB.source_file -> Procname.Set.t option -> unit
-
   (** Compare two nodes *)
   val compare : t -> t -> int
 

infer/src/backend/config.ml

@@ -27,9 +27,10 @@ let from_env_variable var_name =
     let _ = Sys.getenv var_name in true
   with Not_found -> false
 
-let specs_dir_name = "specs"
+let attributes_dir_name = "attributes"
 let captured_dir_name = "captured"
 let sources_dir_name = "sources"
+let specs_dir_name = "specs"
 
 let default_in_zip_results_dir = "infer"
 

infer/src/backend/exe_env.ml

@@ -52,7 +52,6 @@ type t =
     proc_map: file_data Procname.Hash.t; (** map from procedure name to file data *)
     file_map: (DB.source_file, file_data) Hashtbl.t; (** map from filaname to file data *)
     mutable active_opt : Procname.Set.t option; (** if not None, restrict the active procedures to the given set *)
-    mutable callees : Procname.Set.t; (** callees of active procedures *)
     mutable procs_defined_in_several_files : Procname.Set.t; (** Procedures defined in more than one file *)
   }
 
@@ -68,7 +67,6 @@ let create procset_opt =
     proc_map = Procname.Hash.create 17;
     file_map = Hashtbl.create 17;
     active_opt = procset_opt;
-    callees = Procname.Set.empty;
     procs_defined_in_several_files = Procname.Set.empty;
   }
 
@@ -84,26 +82,6 @@ let add_active_proc exe_env proc_name =
   | None -> ()
   | Some procset -> exe_env.active_opt <- Some (Procname.Set.add proc_name procset)
 
-(** Add a callee to the exe_env, and extend the file_map and proc_map. *)
-let add_callee (exe_env: t) (source_file : DB.source_file) (pname: Procname.t) =
-  exe_env.callees <- Procname.Set.add pname exe_env.callees;
-  let file_data_opt =
-    try Some (Hashtbl.find exe_env.file_map source_file)
-    with Not_found ->
-      let source_dir = DB.source_dir_from_source_file source_file in
-      let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in
-      (match Cg.load_from_file cg_fname with
-       | None -> None
-       | Some cg ->
-           let nLOC = Cg.get_nLOC cg in
-           let file_data = new_file_data source_file nLOC cg_fname in
-           Some file_data) in
-  match file_data_opt with
-  | None -> ()
-  | Some file_data ->
-      if (not (Procname.Hash.mem exe_env.proc_map pname))
-      then Procname.Hash.replace exe_env.proc_map pname file_data
-
 (** like add_cg, but use exclude_fun to determine files to be excluded *)
 let add_cg_exclude_fun (exe_env: t) (source_dir : DB.source_dir) exclude_fun =
   let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in
@@ -160,8 +138,21 @@ let get_file_data exe_env pname =
   try
     Procname.Hash.find exe_env.proc_map pname
   with Not_found ->
-    L.err "can't find tenv_cfg_object for %a@." Procname.pp pname;
+    begin
-    raise Not_found
+      match AttributesTable.load_attributes pname with
+      | None ->
+          L.err "can't find tenv_cfg_object for %a@." Procname.pp pname;
+          raise Not_found
+      | Some proc_attributes ->
+          let loc = proc_attributes.ProcAttributes.loc in
+          let source_file = loc.Location.file in
+          let nLOC = loc.Location.nLOC in
+          let source_dir = DB.source_dir_from_source_file source_file in
+          let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in
+          let file_data = new_file_data source_file nLOC cg_fname in
+          Procname.Hash.replace exe_env.proc_map pname file_data;
+          file_data
+    end
 
 (** return the source file associated to the procedure *)
 let get_source exe_env pname =
@@ -188,7 +179,7 @@ let procs_enabled exe_env source =
           let pset'' = Procname.Set.add proc_name pset' in
           res := Procname.Set.union pset'' !res in
       Procname.Set.iter do_pname pset;
-      Some (Procname.Set.union !res exe_env.callees) (* keep callees in the cfg *)
+      Some !res
   | None -> None
 
 let file_data_to_cfg exe_env file_data =
@@ -199,7 +190,6 @@ let file_data_to_cfg exe_env file_data =
             L.err "Cannot find cfg for %s@." (DB.filename_to_string file_data.tenv_file);
             assert false
         | Some cfg -> cfg in
-      Cfg.Node.cfg_restrict_enabled cfg file_data.source (procs_enabled exe_env file_data.source);
       file_data.cfg <- Some cfg;
       cfg
   | Some cfg -> cfg

infer/src/backend/exe_env.mli

@@ -24,9 +24,6 @@ val freeze : initial -> t
 (** create a new execution environment, given an optional set restricting the active procedures *)
 val create : Procname.Set.t option -> initial
 
-(** Add a callee to the exe_env, and extend the file_map and proc_map. *)
-val add_callee : t -> DB.source_file -> Procname.t -> unit
-
 (** add call graph from the source dir in the spec db, with relative tenv and cfg, to the execution environment *)
 val add_cg : initial -> DB.source_dir -> Cg.t option
 

infer/src/backend/fork.ml

@@ -58,7 +58,7 @@ let should_perform_transition gr proc_name : Procname.t list =
 (** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
 let transition_footprint_re_exe proc_name joined_pres =
   L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name;
-  let summary = Specs.get_summary_unsafe proc_name in
+  let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in
   let summary' =
     if !Config.only_footprint then
       { summary with
@@ -166,7 +166,7 @@ let trace = ref false
 let procs_become_done gr pname : Procname.t list =
   let recursive_dependents = Cg.get_recursive_dependents gr pname in
   let nonrecursive_dependents = Cg.get_nonrecursive_dependents gr pname in
-  let summary = Specs.get_summary_unsafe pname in
+  let summary = Specs.get_summary_unsafe "procs_become_done" pname in
   let is_done = Specs.get_timestamp summary <> 0 &&
                 (!Config.only_footprint || Specs.get_phase pname == Specs.RE_EXECUTION) &&
                 Procname.Set.for_all (proc_is_done gr) nonrecursive_dependents &&
@@ -184,7 +184,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.ProcAttributes.loc
+        (Specs.get_summary_unsafe "post_process_procs" pn).Specs.attributes.ProcAttributes.loc
         "No specs found for %a@." Procname.pp pn
     end in
   let cg = Exe_env.get_cg exe_env in
@@ -305,7 +305,7 @@ end
 let main_algorithm exe_env analyze_proc filter_out process_result : unit =
   let call_graph = Exe_env.get_cg exe_env in
   let filter_initial (pname, w) =
-    let summary = Specs.get_summary_unsafe pname in
+    let summary = Specs.get_summary_unsafe "main_algorithm" pname in
     Specs.get_timestamp summary = 0 in
   wpnames_todo := WeightedPnameSet.filter filter_initial (compute_weighed_pnameset call_graph);
   let wpnames_address_of = (* subset of the procedures whose address is taken *)
@@ -319,16 +319,19 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
     (* Return true if [pname] is not up to date and it can be analyzed right now *)
     Procname.Set.for_all
       (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) &&
-    (Specs.get_timestamp (Specs.get_summary_unsafe pname) = 0
+    (Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0
      || 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.ProcAttributes.loc.Location.file;
+      (Specs.get_summary_unsafe "main_algorithm" pname)
+      .Specs.attributes.ProcAttributes.loc.Location.file;
     if !trace then
       begin
         let whole_seconds = false in
         L.err "@[<v 3>   *********** Summary of %a ***********@," Procname.pp pname;
-        L.err "%a@]@\n" (Specs.pp_summary pe_text whole_seconds) (Specs.get_summary_unsafe pname)
+        L.err "%a@]@\n"
+          (Specs.pp_summary pe_text whole_seconds)
+          (Specs.get_summary_unsafe "main_algorithm" pname)
       end;
     if filter_out call_graph pname
     then
@@ -376,7 +379,7 @@ let interprocedural_algorithm
     try _analyze_proc exe_env pname with
     | exn ->
         Reporting.log_error pname exn;
-        let prev_summary = Specs.get_summary_unsafe pname in
+        let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in
         let timestamp = max 1 (prev_summary.Specs.timestamp) in
         let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in
         let summ =

infer/src/backend/inferanalyze.ml

@@ -232,7 +232,7 @@ module Simulator = struct (** Simulate the analysis only *)
   let analyze_proc exe_env tenv proc_name =
     L.err "in analyze_proc %a@." Procname.pp proc_name;
     (* for i = 1 to Random.int 1000000 do () done; *)
-    let prev_summary = Specs.get_summary_unsafe proc_name in
+    let prev_summary = Specs.get_summary_unsafe "Simulator" proc_name in
     let timestamp = max 1 (prev_summary.Specs.timestamp) in
     { prev_summary with Specs.timestamp = timestamp }
 
@@ -329,7 +329,7 @@ type cluster_elem =
   { ce_file : DB.source_file;
     ce_naprocs : int; (** number of active procedures defined in the file *)
     ce_active_procs : Procname.t list; (** list of active procedures *)
-    ce_source_map : DB.source_file Procname.Map.t; (** map from undefined procedures to the file where they are defined *) }
+  }
 
 (** cluster of files *)
 type cluster =
@@ -385,7 +385,10 @@ let create_minimal_clusters file_cg exe_env to_analyze_map : cluster list =
     if !trace_clusters then L.err "      [create_cluster_elem] %s@." (DB.source_file_to_string source_file);
     DB.current_source := source_file;
     match file_pname_to_cg file_pname with
-    | None -> { ce_file = source_file; ce_naprocs = 0; ce_active_procs = []; ce_source_map = Procname.Map.empty }
+    | None -> {
+        ce_file = source_file;
+        ce_naprocs = 0;
+        ce_active_procs = [];}
     | Some cg ->
         (* decide whether a proc is active using pname_to_fname, i.e. whether this is the file associated to it *)
         let proc_is_selected pname = match !select_proc with
@@ -396,28 +399,14 @@ let create_minimal_clusters file_cg exe_env to_analyze_map : cluster list =
           DB.source_file_equal (Exe_env.get_source exe_env pname) source_file in
         let active_procs = list_filter proc_is_active (Procname.Set.elements changed_procs) in
         let naprocs = list_length active_procs in
-        let source_map =
-          let all_procs, _ = Cg.get_nodes_and_edges cg in
-          let mapr = ref Procname.Map.empty in
-          let do_proc (pn, isdefined) =
-            let extend_map proc_name =
-              try
-                let source = Exe_env.get_source exe_env proc_name in
-                mapr := Procname.Map.add proc_name source !mapr;
-              with Not_found -> () in
-            if isdefined && Procname.is_java pn then
-              let tenv = Exe_env.get_tenv exe_env pn in
-              (* Add the overridden methods, so they can be found by the cluster. *)
-              PatternMatch.proc_iter_overridden_methods extend_map tenv pn
-            else
-              (* Add the procedures that are called but not defined in the current file. *)
-              extend_map pn in
-          list_iter do_proc all_procs;
-          !mapr in
         total_files := !total_files + 1;
         total_procs := !total_procs + naprocs;
         total_LOC := !total_LOC + (Cg.get_nLOC cg);
-        { ce_file = source_file; ce_naprocs = naprocs; ce_active_procs = active_procs; ce_source_map = source_map } in
+        {
+          ce_file = source_file;
+          ce_naprocs = naprocs;
+          ce_active_procs = active_procs;
+        } in
   let choose_next_file list = (* choose next file from the weakly ordered list *)
     let file_has_no_unseen_dependents fname =
       Procname.Set.subset (Cg.get_dependents file_cg fname) !seen in
@@ -468,17 +457,11 @@ let clusters_nfiles clusters = list_fold_left (fun n cluster -> cluster_nfiles c
 let clusters_naprocs clusters = list_fold_left (fun n cluster -> cluster_naprocs cluster + n) 0 clusters
 
 let print_clusters_stats clusters =
-  let pp_source_map_ce fmt cluster_elem =
-    let do_map_elem proc_name source_file = F.fprintf fmt "%s " (Procname.to_string proc_name) in
-    Procname.Map.iter do_map_elem cluster_elem.ce_source_map in
-  let pp_source_map fmt cluster =
-    list_iter (pp_source_map_ce fmt) cluster in
   let pp_cluster num cluster =
-    L.err "cluster #%d files: %d active procedures: %d source_map: %a@."
+    L.err "cluster #%d files: %d active procedures: %d@."
       num
       (cluster_nfiles cluster)
-      (cluster_naprocs cluster)
+      (cluster_naprocs cluster) in
-      pp_source_map cluster in
   let i = ref 0 in
   list_iter
     (fun cluster ->
@@ -786,19 +769,13 @@ let compute_files_changed_map _exe_env (source_dirs : DB.source_dir list) exclud
 let exe_env_from_cluster cluster =
   let _exe_env = Exe_env.create (Some (cluster_to_active_procs cluster)) in
   let source_files, callees =
-    let fold_callees pn file callees =
-      (pn, file) :: callees in
     let fold_cluster_elem (source_files, callees) ce =
-      let callees = Procname.Map.fold fold_callees ce.ce_source_map callees in
       let source_files = DB.source_dir_from_source_file ce.ce_file :: source_files in
       source_files, callees in
     list_fold_left fold_cluster_elem ([], []) cluster in
   let sorted_files = list_sort DB.source_dir_compare source_files in
   list_iter (fun src_dir -> ignore(Exe_env.add_cg _exe_env src_dir)) sorted_files;
   let exe_env = Exe_env.freeze _exe_env in
-  let do_callee (pn, file) =
-    Exe_env.add_callee exe_env file pn in
-  list_iter do_callee callees;
   exe_env
 
 (** Analyze a cluster of files *)

infer/src/backend/interproc.ml

@@ -530,7 +530,7 @@ let forward_tabulate cfg tenv =
     let sid_curr_node = Cfg.Node.get_id curr_node 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 proc_name in
+    let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
     mark_visited summary curr_node; (* mark nodes visited in fp and re phases *)
     let session =
       incr summary.Specs.sessions;
@@ -549,7 +549,7 @@ let forward_tabulate cfg tenv =
       Paths.PathSet.iter exe pathset in
     let log_string proc_name =
       let phase_string = (if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE") in
-      let summary = Specs.get_summary_unsafe proc_name 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
     let doit () =
@@ -879,7 +879,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
   let start_node = Cfg.Procdesc.get_start_node pdesc in
 
   let check_recursion_level () =
-    let summary = Specs.get_summary_unsafe pname in
+    let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
     let recursion_level = Specs.get_timestamp summary in
     if recursion_level > !Config.max_recursion then
       begin
@@ -1105,7 +1105,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
   let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in
   let specs = get_results () in
   let elapsed = Unix.gettimeofday () -. init_time in
-  let prev_summary = Specs.get_summary_unsafe proc_name in
+  let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in
   let updated_summary =
     update_summary prev_summary specs proc_name elapsed res in
   if (!Config.curr_language <> Config.Java && Config.report_assertion_failure)
@@ -1182,7 +1182,8 @@ let check_skipped_procs procs_and_defined_children =
   let skipped_procs = ref Procname.Set.empty in
   let proc_check_skips (pname, dep) =
     let process_skip () =
-      let call_stats = (Specs.get_summary_unsafe pname).Specs.stats.Specs.call_stats in
+      let call_stats =
+        (Specs.get_summary_unsafe "check_skipped_procs" pname).Specs.stats.Specs.call_stats in
       let do_tr_elem pn = function
         | Specs.CallStats.CR_skip, _ ->
             skipped_procs := Procname.Set.add pn !skipped_procs
@@ -1285,7 +1286,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg =
     if proc_shadowed proc_desc then
       L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name
     else
-      let summary = Specs.get_summary_unsafe proc_name in
+      let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in
       let stats = summary.Specs.stats in
       let err_log = summary.Specs.attributes.ProcAttributes.err_log in
       incr num_proc;

infer/src/backend/ondemand.ml

@@ -46,7 +46,7 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name =
       Specs.set_status proc_name Specs.ACTIVE in
 
     let postprocess () =
-      let summary = Specs.get_summary_unsafe proc_name in
+      let summary = Specs.get_summary_unsafe "ondemand" proc_name in
       let summary' =
         { summary with
           Specs.status = Specs.INACTIVE;
@@ -96,7 +96,7 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name =
 
 (** Mark the return type @Nullable by modifying the spec. *)
 let proc_add_return_nullable curr_pname =
-  let summary = Specs.get_summary_unsafe curr_pname in
+  let summary = Specs.get_summary_unsafe "proc_add_return_nullable" curr_pname in
   let proc_attributes = Specs.get_attributes summary in
   let method_annotation = proc_attributes.ProcAttributes.method_annotation in
   let method_annotation' = Annotations.method_annotation_mark_return

infer/src/backend/serialization.ml

@@ -19,7 +19,10 @@ type 'a serializer = (string -> 'a option) * (DB.filename -> 'a option) * (DB.fi
 type key = int
 
 (** current key for tenv, procedure summary, cfg, error trace, call graph *)
-let tenv_key, summary_key, cfg_key, trace_key, cg_key, analysis_results_key, cluster_key = (425184201, 160179325, 1062389858, 221487792, 477305409, 799050016, 579094948)
+let tenv_key, summary_key, cfg_key, trace_key, cg_key,
+    analysis_results_key, cluster_key, attributes_key =
+  425184201, 160179325, 1062389858, 221487792, 477305409,
+  799050016, 579094948, 972393003
 
 (** version of the binary files, to be incremented for each change *)
 let version = 24

infer/src/backend/serialization.mli

@@ -18,35 +18,39 @@ type 'a serializer
 (** Serialization key, used to distinguish versions of serializers and avoid assert faults *)
 type key
 
-(** current key for tenv *)
+(** current key for an analysis results value *)
-val tenv_key : key
+val analysis_results_key : key
 
-(** current key for a procedure summary *)
+(** current key for proc attributes *)
-val summary_key : key
+val attributes_key : key
 
 (** current key for a cfg *)
 val cfg_key : key
 
-(** current key for an error trace *)
-val trace_key : key
-
 (** current key for a call graph *)
 val cg_key : key
 
+(** create a serializer from a file name
+    given an integer key used as double-check of the file type *)
+val create_serializer : key -> 'a serializer
+
 (** current key for a cluster *)
 val cluster_key : key
 
-(** current key for an analysis results value *)
+(** extract a from_file function from a serializer *)
-val analysis_results_key : key
+val from_file : 'a serializer -> DB.filename -> 'a option
-
-(** create a serializer from a file name, given an integer key used as double-check of the file type *)
-val create_serializer : key -> 'a serializer
 
 (** extract a from_string function from a serializer *)
 val from_string : 'a serializer -> string -> 'a option
 
-(** extract a from_file function from a serializer *)
+(** current key for a procedure summary *)
-val from_file : 'a serializer -> DB.filename -> 'a option
+val summary_key : key
+
+(** current key for tenv *)
+val tenv_key : key
 
 (** extract a to_file function from a serializer *)
 val to_file : 'a serializer -> DB.filename -> 'a -> unit
+
+(** current key for an error trace *)
+val trace_key : key

infer/src/backend/specs.ml

@@ -521,7 +521,8 @@ let specs_models_filename pname =
 let summary_exists_in_models pname =
   Sys.file_exists (DB.filename_to_string (specs_models_filename pname))
 
-let summary_serializer : summary Serialization.serializer = Serialization.create_serializer Serialization.summary_key
+let summary_serializer : summary Serialization.serializer =
+  Serialization.create_serializer Serialization.summary_key
 
 (** Save summary for the procedure into the spec database *)
 let store_summary pname (summ: summary) =
@@ -610,10 +611,11 @@ let get_summary proc_name =
   | Some (summary, _) -> Some summary
   | None -> None
 
-let get_summary_unsafe proc_name =
+let get_summary_unsafe s proc_name =
   match get_summary proc_name with
   | None ->
-      raise (Failure ("Specs.get_summary_unsafe: " ^ (Procname.to_string proc_name) ^ "Not_found"))
+      raise (Failure (
+          "[" ^ s ^ "] Specs.get_summary_unsafe: " ^ (Procname.to_string proc_name) ^ "Not_found"))
   | Some summary -> summary
 
 (** Check if the procedure is from a library:
@@ -625,17 +627,14 @@ let proc_is_library proc_attributes =
     | Some _ -> false
   else false
 
-(** Try to find the attributes for a defined proc, by first looking at the procdesc
+(** Try to find the attributes for a defined proc.
-    then looking at .specs files if required.
+    First look at specs (to get attributes computed by analysis)
-    Return the attributes for an underfined procedure otherwise.
+    then look at the attributes table.
     If no attributes can be found, return None.
 *)
-let proc_resolve_attributes get_proc_desc proc_name =
+let proc_resolve_attributes proc_name =
-  let from_proc_desc () =  match get_proc_desc proc_name with
+  let from_attributes_table () =
-    | Some proc_desc ->
+    AttributesTable.load_attributes proc_name in
-        Some (Cfg.Procdesc.get_attributes proc_desc)
-    | None ->
-        None in
   let from_specs () = match get_summary proc_name with
     | Some summary ->
         Some summary.attributes
@@ -645,23 +644,19 @@ let proc_resolve_attributes get_proc_desc proc_name =
       if attributes.ProcAttributes.is_defined
       then Some attributes
       else begin
-        match from_proc_desc () with
+        match from_attributes_table () with
         | Some attributes' ->
             Some attributes'
         | None ->
             Some attributes
       end
   | None ->
-      from_proc_desc ()
+      from_attributes_table ()
 
 (** Like proc_resolve_attributes but start from a proc_desc. *)
 let pdesc_resolve_attributes proc_desc =
   let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
-  let get_proc_desc proc_name' =
+  match proc_resolve_attributes proc_name with
-    if Procname.equal proc_name proc_name'
-    then Some proc_desc
-    else None in
-  match proc_resolve_attributes get_proc_desc proc_name with
   | Some proc_attributes ->
       proc_attributes
   | None ->
@@ -682,10 +677,10 @@ let get_status summary =
   summary.status
 
 let is_active proc_name =
-  get_status (get_summary_unsafe proc_name) = ACTIVE
+  get_status (get_summary_unsafe "is_active" proc_name) = ACTIVE
 
 let is_inactive proc_name =
-  get_status (get_summary_unsafe proc_name) = INACTIVE
+  get_status (get_summary_unsafe "is_active" proc_name) = INACTIVE
 
 let get_timestamp summary =
   summary.timestamp

infer/src/backend/specs.mli

@@ -196,7 +196,7 @@ val get_specs_from_payload : summary -> Prop.normal spec list
 val get_summary : Procname.t -> summary option
 
 (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *)
-val get_summary_unsafe : Procname.t -> summary
+val get_summary_unsafe : string -> Procname.t -> summary
 
 (** Return the current timestamp for the summary *)
 val get_timestamp : summary -> int
@@ -249,13 +249,12 @@ val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit
 (** Like proc_resolve_attributes but start from a proc_desc. *)
 val pdesc_resolve_attributes : Cfg.Procdesc.t -> ProcAttributes.t
 
-(** Try to find the attributes for a defined proc, by first looking at the procdesc
+(** Try to find the attributes for a defined proc.
-    then looking at .specs files if required.
+    First look at specs (to get attributes computed by analysis)
-    Return the attributes for an underfined procedure otherwise.
+    then look at the attributes table.
     If no attributes can be found, return None.
 *)
-val proc_resolve_attributes :
+val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
-  (Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> ProcAttributes.t option
 
 (** Check if the procedure is from a library:
     It's not defined, and there is no spec file for it. *)

infer/src/backend/symExec.ml

@@ -1264,7 +1264,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop
 
 and sym_exe_check_variadic_sentinel_if_present
     cfg pdesc tenv prop path actual_params callee_pname loc =
-  match Specs.proc_resolve_attributes (Cfg.Procdesc.find_from_name cfg) callee_pname with
+  match Specs.proc_resolve_attributes callee_pname with
   | None ->
       [(prop, path)]
   | Some callee_attributes ->

infer/src/checkers/checkers.ml

@@ -35,14 +35,14 @@ module ST = struct
     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
+    let summary = Specs.get_summary_unsafe "ST.pname_add" proc_name in
     add summary key value
 
   let files_open = ref Procname.Set.empty
 
   let pname_find proc_name key =
     if Procname.Set.mem proc_name !files_open then
-      let summary = Specs.get_summary_unsafe proc_name in
+      let summary = Specs.get_summary_unsafe "ST.pname_find" proc_name in
       proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key
     else begin
       match Specs.get_summary proc_name with

infer/src/checkers/codeQuery.ml

@@ -37,7 +37,7 @@ let query_ast =
 module Err = struct
   (** Update the summary with stats from the checker. *)
   let update_summary proc_name proc_desc =
-    let old_summ = Specs.get_summary_unsafe proc_name in
+    let old_summ = Specs.get_summary_unsafe "codeQuery" proc_name in
     let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in
     let specs =
       let spec =

infer/src/checkers/eradicate.ml

@@ -51,23 +51,25 @@ module MkCallback
 struct
   (** Update the summary with stats from the checker. *)
   let update_summary proc_name proc_desc final_typestate_opt =
-    let old_summ = Specs.get_summary_unsafe proc_name in
+    match Specs.get_summary proc_name with
-    let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in
+    | Some old_summ ->
-    let method_annotation =
+        let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in
-      (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
+        let method_annotation =
-    let new_summ =
+          (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
-      {
+        let new_summ =
-        old_summ with
-        Specs.nodes = nodes;
-        Specs.payload = Extension.mkpayload final_typestate_opt;
-        Specs.attributes =
           {
-            old_summ.Specs.attributes with
+            old_summ with
-            ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc;
+            Specs.nodes = nodes;
-            method_annotation;
+            Specs.payload = Extension.mkpayload final_typestate_opt;
-          };
+            Specs.attributes =
-      } in
+              {
-    Specs.add_summary proc_name new_summ
+                old_summ.Specs.attributes with
+                ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc;
+                method_annotation;
+              };
+          } in
+        Specs.add_summary proc_name new_summ
+    | None -> ()
 
   let callback1
       find_canonical_duplicate calls_this checks get_proc_desc idenv tenv curr_pname
@@ -185,18 +187,23 @@ struct
         let get_private_called (initializers : init list) : init list =
           let res = ref [] in
           let do_proc (init_pn, init_pd) =
-            let filter callee_pn callee_pd =
+            let filter callee_pn callee_attributes =
               let is_private =
-                let attr = Specs.pdesc_resolve_attributes callee_pd in
+                callee_attributes.ProcAttributes.access = Sil.Private 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)
                   else None in
                 get_class_opt init_pn = get_class_opt callee_pn in
               is_private && same_class in
-            let private_called = PatternMatch.proc_calls get_proc_desc init_pn init_pd filter in
+            let private_called = PatternMatch.proc_calls
-            res := private_called @ !res in
+                Specs.proc_resolve_attributes init_pn init_pd filter in
+            let do_called (callee_pn, callee_attributes) =
+              match get_proc_desc callee_pn with
+              | Some callee_pd ->
+                  res := (callee_pn, callee_pd) :: !res
+              | None -> () in
+            list_iter do_called private_called in
           list_iter do_proc initializers;
           !res in
 
@@ -233,29 +240,34 @@ struct
         list_rev !final_typestates
 
       let pname_and_pdescs_with f =
-        list_map
+        let res = ref [] in
-          (fun n -> match get_proc_desc n with
+        let filter pname = match Specs.proc_resolve_attributes pname with
-             | Some d -> [(n, d)]
+          | Some proc_attributes -> f (pname, proc_attributes)
-             | None -> [])
+          | None -> false in
-          all_procs
+        let do_proc pname =
-        |> list_flatten
+          if filter pname then
-        |> list_filter f
+            match get_proc_desc pname with
+            | Some pdesc ->
+                res := (pname, pdesc) :: !res
+            | None -> () in
+        list_iter do_proc all_procs;
+        list_rev !res
 
       (** Typestates after the current procedure and all initializer procedures. *)
       let final_initializer_typestates_lazy = lazy
         begin
-          let is_initializer pdesc pname =
+          let is_initializer pname proc_attributes =
-            PatternMatch.method_is_initializer tenv (Cfg.Procdesc.get_attributes pdesc) ||
+            PatternMatch.method_is_initializer tenv proc_attributes ||
             let ia, _ =
-              (Models.get_modelled_annotated_signature
+              (Models.get_modelled_annotated_signature proc_attributes).Annotations.ret in
-                 (Cfg.Procdesc.get_attributes pdesc)).Annotations.ret in
             Annotations.ia_is_initializer ia in
           let initializers_current_class =
             pname_and_pdescs_with
-              (fun (pname, pdesc) ->
+              (function (pname, proc_attributes) ->
-                 is_initializer pdesc pname &&
+                is_initializer pname proc_attributes &&
-                 Procname.java_get_class pname = Procname.java_get_class curr_pname) in
+                Procname.java_get_class pname = Procname.java_get_class curr_pname) in
-          final_typestates ((curr_pname, curr_pdesc):: initializers_current_class)
+          final_typestates
+            ((curr_pname, curr_pdesc) :: initializers_current_class)
         end
 
       (** Typestates after all constructors. *)
@@ -263,9 +275,9 @@ struct
         begin
           let constructors_current_class =
             pname_and_pdescs_with
-              (fun (n, d) ->
+              (fun (pname, proc_attributes) ->
-                 Procname.is_constructor n &&
+                 Procname.is_constructor pname &&
-                 Procname.java_get_class n = Procname.java_get_class curr_pname) in
+                 Procname.java_get_class pname = Procname.java_get_class curr_pname) in
           final_typestates constructors_current_class
         end
 

infer/src/checkers/eradicateChecks.ml

@@ -536,7 +536,7 @@ let check_overridden_annotations
       ignore (list_fold_left2 compare initial_pos current_params overridden_params) in
 
   let check overriden_proc_name =
-    match Specs.proc_resolve_attributes get_proc_desc overriden_proc_name with
+    match Specs.proc_resolve_attributes overriden_proc_name with
     | Some attributes ->
         let overridden_signature = Models.get_modelled_annotated_signature attributes in
         check_return overriden_proc_name overridden_signature;

infer/src/checkers/patternMatch.ml

@@ -302,14 +302,15 @@ let java_get_vararg_values node pvar idenv pdesc =
     | None -> () in
   !values
 
-let proc_calls get_proc_desc pname pdesc filter : (Procname.t * Cfg.Procdesc.t) list =
+let proc_calls resolve_attributes pname pdesc filter : (Procname.t * ProcAttributes.t) list =
   let res = ref [] in
   let do_instruction node instr = match instr with
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) ->
         begin
-          match get_proc_desc callee_pn with
+          match resolve_attributes callee_pn with
-          | Some callee_pd ->
+          | Some callee_attributes ->
-              if filter callee_pn callee_pd then res := (callee_pn, callee_pd) :: !res
+              if filter callee_pn callee_attributes then
+                res := (callee_pn, callee_attributes) :: !res
           | None -> ()
         end
     | _ -> () in

infer/src/checkers/patternMatch.mli

@@ -48,10 +48,12 @@ val java_get_vararg_values : Cfg.Node.t -> Sil.pvar -> Idenv.t -> Cfg.Procdesc.t
 
 val java_proc_name_with_class_method : Procname.t -> string -> string -> bool
 
-(** [proc_calls get_proc_desc pn pd filter] returns the callees that satisfy [filter]. *)
+(** Return the callees that satisfy [filter]. *)
-val proc_calls : (Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> Cfg.Procdesc.t ->
+val proc_calls :
-  (Procname.t -> Cfg.Procdesc.t -> bool) ->
+  (Procname.t -> ProcAttributes.t option) ->
-  (Procname.t * Cfg.Procdesc.t) list
+  Procname.t -> Cfg.Procdesc.t ->
+  (Procname.t -> ProcAttributes.t -> bool) ->
+  (Procname.t * ProcAttributes.t) list
 
 (** Iterate over all the methods overridden by the procedure.
     Only Java supported at the moment. *)

infer/src/checkers/typeCheck.ml

@@ -46,9 +46,8 @@ module ComplexExpressions = struct
   let procname_instanceof = Procname.equal SymExec.ModelBuiltins.__instanceof
 
   let procname_is_false_on_null get_proc_desc pn =
-    match get_proc_desc pn with
+    match Specs.proc_resolve_attributes pn with
-    | Some pdesc ->
+    | Some proc_attributes ->
-        let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
         let annotated_signature =
           Models.get_modelled_annotated_signature proc_attributes in
         let ret_ann, _ = annotated_signature.Annotations.ret in
@@ -58,9 +57,8 @@ module ComplexExpressions = struct
 
   let procname_is_true_on_null get_proc_desc pn =
     let annotated_true_on_null () =
-      match get_proc_desc pn with
+      match Specs.proc_resolve_attributes pn with
-      | Some pdesc ->
+      | Some proc_attributes ->
-          let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
           let annotated_signature =
             Models.get_modelled_annotated_signature proc_attributes in
           let ret_ann, _ = annotated_signature.Annotations.ret in
@@ -558,12 +556,12 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
   | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when SymExec.function_is_builtin pn ->
       typestate (* skip othe builtins *)
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
-    when get_proc_desc callee_pname <> None ->
+    when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None ->
-      Ondemand.do_analysis get_proc_desc curr_pname callee_pname;
+      if Ondemand.enabled () then
+        Ondemand.do_analysis get_proc_desc curr_pname callee_pname;
       let callee_attributes =
-        match get_proc_desc callee_pname with
+        match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
-        | Some pdesc ->
+        | Some proc_attributes -> proc_attributes
-            Specs.pdesc_resolve_attributes pdesc
         | None -> assert false in
       let callee_loc = callee_attributes.ProcAttributes.loc in
 
@@ -1003,7 +1001,7 @@ let typecheck_node
   let handle_exceptions typestate instr = match instr with
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) ->
         let callee_attributes_opt =
-          Specs.proc_resolve_attributes get_proc_desc callee_pname in
+          Specs.proc_resolve_attributes callee_pname in
         (* check if the call might throw an exception *)
         let has_exceptions = match callee_attributes_opt with
           | Some callee_attributes ->