diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml
index b64bbcbae..3434babe3 100644
--- a/infer/src/backend/callbacks.ml
+++ b/infer/src/backend/callbacks.ml
@@ -221,11 +221,9 @@ let iterate_callbacks store_summary call_graph exe_env =
       | Some cfg ->
           Cfg.Procdesc.find_from_name cfg proc_name
       | None -> None in
-    let loc = match procdesc_opt with
-      | Some proc_desc ->
-          Cfg.Procdesc.get_loc proc_desc
-      | None -> Location.dummy in
-    Specs.reset_summary call_graph proc_name loc in
+    let attributes_opt =
+      Option.map Cfg.Procdesc.get_attributes procdesc_opt in
+    Specs.reset_summary call_graph proc_name attributes_opt in
 
 
   (* Make sure summaries exists. *)
diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml
index 5ccdf2989..c0931d224 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.dummy)
+      (fun (pname, in_out_calls) -> Specs.reset_summary cg pname None)
       (Cg.get_nodes_and_calls cg)
 
   (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 1722f4118..7585c6006 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -1048,9 +1048,8 @@ let report_runtime_exceptions tenv cfg pdesc summary =
     && Procname.java_is_static pname
     && (Procname.java_get_method pname) = "main" in
   let is_annotated =
-    let annotated_signature =
-      Annotations.get_annotated_signature
-        Specs.proc_get_method_annotation pdesc pname in
+    let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
+    let annotated_signature = Annotations.get_annotated_signature proc_attributes in
     let ret_annotation, _ = annotated_signature.Annotations.ret in
     Annotations.ia_is_verify ret_annotation in
   let is_unavoidable pre =
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 0631b50c4..afc5a9600 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -935,7 +935,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
   let nullable_obj_str = ref None in
   (* return true if deref_exp is only pointed to by fields/params with @Nullable annotations *)
   let is_only_pt_by_nullable_fld_or_param deref_exp =
-    let ann_sig = Models.get_annotated_signature pdesc (Cfg.Procdesc.get_proc_name pdesc) in
+    let ann_sig = Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes pdesc) in
     list_for_all
       (fun hpred ->
          match hpred with
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 8d36dd11d..44cd306f5 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -617,28 +617,55 @@ let get_summary_unsafe proc_name =
   | Some summary -> summary
 
 (** Check if the procedure is from a library:
-    It's not defined in the current proc desc, and there is no spec file for it. *)
-let proc_is_library proc_name proc_desc =
-  let defined = Cfg.Procdesc.is_defined proc_desc in
-  if not defined then
-    match get_summary proc_name with
+    It's not defined, and there is no spec file for it. *)
+let proc_is_library proc_attributes =
+  if not proc_attributes.ProcAttributes.is_defined then
+    match get_summary proc_attributes.ProcAttributes.proc_name with
     | None -> true
     | Some _ -> false
   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 : 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
-    match get_summary proc_name with
-    | None -> from_proc_desc
+(** Try to find the attributes for a defined proc, by first looking at the procdesc
+    then looking at .specs files if required.
+    Return the attributes for an underfined procedure otherwise.
+    If no attributes can be found, return None.
+*)
+let proc_resolve_attributes get_proc_desc proc_name =
+  let from_proc_desc () =  match get_proc_desc proc_name with
+    | Some proc_desc ->
+        Some (Cfg.Procdesc.get_attributes proc_desc)
+    | None ->
+        None in
+  let from_specs () = match get_summary proc_name with
     | Some summary ->
-        summary.attributes (* get attributes from .specs file *)
-  else from_proc_desc
-
-let proc_get_method_annotation proc_name proc_desc =
-  (proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation
+        Some summary.attributes
+    | None -> None in
+  match from_proc_desc () with
+  | Some attributes ->
+      if attributes.ProcAttributes.is_defined
+      then Some attributes
+      else begin
+        match from_specs () with
+        | Some attributes' ->
+            Some attributes'
+        | None -> Some attributes
+      end
+  | None ->
+      from_specs ()
+
+(** 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' =
+    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 ->
+      (* this should not happen *)
+      assert false
 
 let get_origin proc_name =
   match get_summary_origin proc_name with
@@ -770,11 +797,14 @@ let init_summary
     } in
   Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir)
 
-let reset_summary call_graph proc_name loc =
+(** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
+let reset_summary call_graph proc_name attributes_opt =
   let dependents = Cg.get_defined_children call_graph proc_name in
-  let proc_attributes =
-    { (ProcAttributes.default proc_name !Config.curr_language) with
-      loc; } in
+  let proc_attributes = match attributes_opt with
+    | Some attributes ->
+        attributes
+    | None ->
+        ProcAttributes.default proc_name !Config.curr_language in
   init_summary (
     Procname.Set.elements dependents,
     [],
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 7ca19b75e..0ae1f073d 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -222,7 +222,8 @@ val init_summary :
    ProcAttributes.t) (** attributes of the procedure *)
   -> unit
 
-val reset_summary : Cg.t -> Procname.t -> Location.t -> unit
+(** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
+val reset_summary : Cg.t -> Procname.t -> ProcAttributes.t option -> unit
 
 (** Load procedure summary from the given file *)
 val load_summary : DB.filename -> summary option
@@ -245,14 +246,20 @@ val pp_specs : printenv -> Format.formatter -> Prop.normal spec list -> unit
 (** Print the summary, the bool indicates whether to print whole seconds only *)
 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 -> ProcAttributes.t
+(** Like proc_resolve_attributes but start from a proc_desc. *)
+val pdesc_resolve_attributes : Cfg.Procdesc.t -> ProcAttributes.t
 
-val proc_get_method_annotation : Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
+(** Try to find the attributes for a defined proc, by first looking at the procdesc
+    then looking at .specs files if required.
+    Return the attributes for an underfined procedure otherwise.
+    If no attributes can be found, return None.
+*)
+val proc_resolve_attributes :
+  (Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> ProcAttributes.t option
 
 (** Check if the procedure is from a library:
-    It's not defined in the current proc desc, and there is no spec file for it. *)
-val proc_is_library : Procname.t -> Cfg.Procdesc.t -> bool
+    It's not defined, and there is no spec file for it. *)
+val proc_is_library : ProcAttributes.t -> bool
 
 (** Re-initialize a dependency map *)
 val re_initialize_dependency_map : dependency_map_t -> dependency_map_t
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 96b859a6a..ebbf8e484 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -561,8 +561,7 @@ let check_constant_string_dereference lexp =
   | _ -> None
 
 (** Normalize an expression and check for arithmetic problems *)
-let exp_norm_check_arith pdesc prop exp =
-  let pname = Cfg.Procdesc.get_proc_name pdesc in
+let exp_norm_check_arith pname prop exp =
   match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
   | Some (Prop.Div0 div), prop' ->
       let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
@@ -761,9 +760,11 @@ let redirect_shared_ptr tenv cfg pname actual_params =
           pname'
     else pname
 
-(** recognize calls to the constructor java.net.URL and splits the argument string to be only the protocol.  *)
-let call_constructor_url_update_args tenv cfg pname actual_params =
-  let url_pname = Procname.mangled_java ((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in
+(** recognize calls to the constructor java.net.URL and splits the argument string
+    to be only the protocol.  *)
+let call_constructor_url_update_args pname actual_params =
+  let url_pname = Procname.mangled_java
+      ((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in
   if (Procname.equal url_pname pname) then
     (match actual_params with
      | [this; (Sil.Const (Sil.Cstr s), atype)] ->
@@ -781,7 +782,7 @@ let call_constructor_url_update_args tenv cfg pname actual_params =
 (** Handles certain method calls in a special way *)
 let handle_special_cases_call tenv cfg pname actual_params =
   if (!Config.curr_language = Config.Java) then
-    pname, (call_constructor_url_update_args tenv cfg pname actual_params)
+    pname, (call_constructor_url_update_args pname actual_params)
   else if (!Config.curr_language = Config.C_CPP) then
     (redirect_shared_ptr tenv cfg pname actual_params), actual_params
   else pname, actual_params
@@ -876,7 +877,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
   | Sil.Letderef (id, rhs_exp, typ, loc) ->
       begin
         try
-          let n_rhs_exp, prop = exp_norm_check_arith pdesc _prop rhs_exp in
+          let n_rhs_exp, prop = exp_norm_check_arith pname _prop rhs_exp in
           let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_rhs_exp in
           match check_constant_string_dereference n_rhs_exp' with
           | Some value ->
@@ -896,8 +897,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
   | Sil.Set (lhs_exp, typ, rhs_exp, loc) ->
       begin
         try
-          let n_lhs_exp, _prop' = exp_norm_check_arith pdesc _prop lhs_exp in
-          let n_rhs_exp, prop = exp_norm_check_arith pdesc _prop' rhs_exp in
+          let n_lhs_exp, _prop' = exp_norm_check_arith pname _prop lhs_exp in
+          let n_rhs_exp, prop = exp_norm_check_arith pname _prop' rhs_exp in
           let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in
           let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_lhs_exp in
           let iter_list = Rearrange.rearrange pdesc tenv n_lhs_exp' typ prop loc in
@@ -927,14 +928,15 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
         | _ -> () in
       check_already_dereferenced pname cond _prop;
       check_condition_always_true_false ();
-      let n_cond, prop = exp_norm_check_arith pdesc _prop cond in
+      let n_cond, prop = exp_norm_check_arith pname _prop cond in
       ret_old_path (Propset.to_proplist (prune_prop tenv n_cond prop))
-  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun fn), args, loc, call_flags) when function_is_builtin fn ->
-      let sym_exe_builtin = Builtin.get_sym_exe_builtin fn in
-      sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args fn loc
+  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, call_flags)
+    when function_is_builtin callee_pname ->
+      let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in
+      sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) ->
       (** Generic fun call with known name *)
-      let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_params in
+      let (prop_r, _n_actual_params) = normalize_params pname _prop actual_params in
       let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in
       let resolved_pname =
         if call_flags.Sil.cf_virtual then
@@ -961,7 +963,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
           ret_ids ret_typ_opt n_actual_params resolved_pname loc in
       let sentinel_result =
         if !Config.curr_language = Config.C_CPP then
-          sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop_r path actual_params callee_pname loc
+          sym_exe_check_variadic_sentinel_if_present
+            cfg pdesc tenv prop_r path actual_params callee_pname loc
         else [(prop_r, path)] in
       let do_call (prop, path) =
         match Specs.get_summary resolved_pname with
@@ -973,7 +976,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
               cfg pdesc tenv prop path ret_ids n_actual_params summary loc in
       list_flatten (list_map do_call sentinel_result)
   | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *)
-      let (prop_r, n_actual_params) = normalize_params pdesc _prop actual_params in
+      let (prop_r, n_actual_params) = normalize_params pname _prop actual_params in
       if call_flags.Sil.cf_is_objc_block then
         Rearrange.check_call_to_objc_block_error pdesc prop_r fun_exp loc;
       Rearrange.check_dereference_error pdesc prop_r fun_exp loc;
@@ -1032,7 +1035,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
   | Sil.Stackop _ -> (* this should be handled at the propset level *)
       assert false
   | Sil.Goto_node (node_e, loc) ->
-      let n_node_e, prop = exp_norm_check_arith pdesc _prop node_e in
+      let n_node_e, prop = exp_norm_check_arith pname _prop node_e in
       begin
         match n_node_e with
         | Sil.Const (Sil.Cint i) ->
@@ -1251,17 +1254,21 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop
   (* error on the first premature nil argument *)
   list_fold_left check_allocated [(prop, path)] non_terminal_argsi
 
-and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_params callee_pname loc =
-  match Cfg.Procdesc.find_from_name cfg callee_pname with
-  | None -> [(prop, path)]
-  | Some callee_pdesc ->
-      let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in
+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
+  | None ->
+      [(prop, path)]
+  | Some callee_attributes ->
       match Sil.get_sentinel_func_attribute_value
-              proc_attributes.ProcAttributes.func_attributes with
+              callee_attributes.ProcAttributes.func_attributes with
       | None -> [(prop, path)]
       | Some sentinel_arg ->
-          let formals = Cfg.Procdesc.get_formals callee_pdesc in
-          sym_exe_check_variadic_sentinel cfg pdesc tenv prop path (list_length formals) actual_params sentinel_arg callee_pname loc
+          let formals = callee_attributes.ProcAttributes.formals in
+          sym_exe_check_variadic_sentinel
+            cfg pdesc tenv prop path (list_length formals)
+            actual_params sentinel_arg callee_pname loc
+
 
 (** Perform symbolic execution for a function call *)
 and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc =
@@ -1468,8 +1475,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp, typ)] when list_length ret_ids <= 1 ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
         let return_result_for_array_size e prop ret_ids = return_result e prop ret_ids in
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         begin
           try
             let hpred = list_find (function
@@ -1500,8 +1508,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ); (size, _)], [] ->
-        let n_lexp, _prop' = exp_norm_check_arith pdesc _prop lexp in
-        let n_size, prop = exp_norm_check_arith pdesc _prop' size in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, _prop' = exp_norm_check_arith pname _prop lexp in
+        let n_size, prop = exp_norm_check_arith pname _prop' size in
         begin
           try
             let hpred, sigma' = list_partition (function
@@ -1534,8 +1543,9 @@ module ModelBuiltins = struct
   let execute___print_value cfg pdesc instr tenv prop path ret_ids args callee_pname loc
     : Builtin.ret_typ =
     L.err "__print_value: ";
+    let pname = Cfg.Procdesc.get_proc_name pdesc in
     let do_arg (lexp, typ) =
-      let n_lexp, _ = exp_norm_check_arith pdesc prop lexp in
+      let n_lexp, _ = exp_norm_check_arith pname prop lexp in
       L.err "%a " (Sil.pp_exp pe_text) n_lexp in
     list_iter do_arg args;
     L.err "@.";
@@ -1598,7 +1608,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp, typ)] when list_length ret_ids <= 1 ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let props = create_type tenv n_lexp typ prop in
         let aux prop =
           begin
@@ -1636,8 +1647,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 ->
-        let val1, __prop = exp_norm_check_arith pdesc _prop _val1 in
-        let texp2, prop = exp_norm_check_arith pdesc __prop _texp2 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let val1, __prop = exp_norm_check_arith pname _prop _val1 in
+        let texp2, prop = exp_norm_check_arith pname __prop _texp2 in
         let exe_one_prop prop =
           if Sil.exp_equal texp2 Sil.exp_zero then
             [(return_result Sil.exp_zero prop ret_ids, path)]
@@ -1719,7 +1731,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         set_resource_attribute prop path n_lexp loc Sil.Rfile
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1728,7 +1741,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         set_resource_attribute prop path n_lexp loc Sil.Rlock
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1738,7 +1752,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [_ ; (lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         set_resource_attribute prop path n_lexp loc Sil.Rignore
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1747,7 +1762,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew)
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1756,7 +1772,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let prop' = match Prop.get_taint_attribute prop n_lexp with
           | _ ->
               let check_attr_change att_old att_new = () in
@@ -1770,7 +1787,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let prop' = match Prop.get_taint_attribute prop n_lexp with
           | _ ->
               let check_attr_change att_old att_new = () in
@@ -1784,7 +1802,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp, typ)] ->
-        let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let ret_val = ref None in
         let return_val p = match !ret_val with
           | Some e -> return_result e p ret_ids
@@ -1819,8 +1838,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp1, typ1); (lexp2, typ2)] ->
-        let n_lexp1, _prop1 = exp_norm_check_arith pdesc _prop lexp1 in
-        let n_lexp2, prop = exp_norm_check_arith pdesc _prop1 lexp2 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp1, _prop1 = exp_norm_check_arith pname _prop lexp1 in
+        let n_lexp2, prop = exp_norm_check_arith pname _prop1 lexp2 in
         let foot_var = lazy (Sil.Var (Ident.create_fresh Ident.kfootprint)) in
         let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in
         let has_fld_hidden fsel = list_exists filter_fld_hidden fsel in
@@ -1846,9 +1866,10 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp, typ)] when list_length ret_ids <= 1 ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
         (match ret_ids with
          | [ret_id] ->
-             let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+             let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
              [(return_result (Sil.BinOp(Sil.Ne, n_lexp, (Sil.Const(Sil.Cattribute((Sil.Auntaint)))))) prop ret_ids, path)]
          | _ -> [(_prop, path)])
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@@ -1928,9 +1949,10 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args, ret_ids with
     | [(lexp, typ)], _ ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
         let prop = return_result lexp _prop ret_ids in
         if !Config.objc_memory_model_on then
-          let n_lexp, prop = exp_norm_check_arith pdesc prop lexp in
+          let n_lexp, prop = exp_norm_check_arith pname prop lexp in
           let check_attr_change att_old att_new = () in
           let prop' = Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp Sil.Aautorelease in
           [(prop', path)]
@@ -1967,8 +1989,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 ->
-        let val1, __prop = exp_norm_check_arith pdesc _prop _val1 in
-        let texp2, prop = exp_norm_check_arith pdesc __prop _texp2 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let val1, __prop = exp_norm_check_arith pname _prop _val1 in
+        let texp2, prop = exp_norm_check_arith pname __prop _texp2 in
         (try
            let hpred = list_find (function
                | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
@@ -2028,7 +2051,8 @@ module ModelBuiltins = struct
     match args with
     | [(lexp, typ)] ->
         begin
-          let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in
+          let pname = Cfg.Procdesc.get_proc_name pdesc in
+          let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
           let prop_nonzero = (* case n_lexp!=0 *)
             Propset.to_proplist (prune_polarity tenv true n_lexp prop) in
           let prop_zero = (* case n_lexp==0 *)
@@ -2044,6 +2068,7 @@ module ModelBuiltins = struct
 
   let execute_alloc mk can_return_null cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
     : Builtin.ret_typ =
+    let pname = Cfg.Procdesc.get_proc_name pdesc in
     let rec evaluate_char_sizeof e = match e with
       | Sil.Var _ -> e
       | Sil.UnOp (uop, e', typ) ->
@@ -2067,7 +2092,7 @@ module ModelBuiltins = struct
       | [ret_id] -> ret_id
       | _ -> Ident.create_fresh Ident.kprimed in
     let size_exp', prop =
-      let n_size_exp, prop = exp_norm_check_arith pdesc _prop size_exp in
+      let n_size_exp, prop = exp_norm_check_arith pname _prop size_exp in
       let n_size_exp' = evaluate_char_sizeof n_size_exp in
       Prop.exp_normalize_prop prop n_size_exp', prop in
     let cnt_te = handle_sizeof_exp size_exp' in
@@ -2128,7 +2153,8 @@ module ModelBuiltins = struct
     match args with
     | [(ret_exn, _)] ->
         begin
-          let n_ret_exn, prop = exp_norm_check_arith pdesc _prop ret_exn in
+          let pname = Cfg.Procdesc.get_proc_name pdesc in
+          let n_ret_exn, prop = exp_norm_check_arith pname _prop ret_exn in
           match n_ret_exn with
           | Sil.Const (Sil.Cexn exp) ->
               let prop_with_exn = return_result exp prop ret_ids in
@@ -2141,7 +2167,8 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | (_arg1, _):: _ ->
-        let arg1, prop = exp_norm_check_arith pdesc _prop _arg1 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let arg1, prop = exp_norm_check_arith pname _prop _arg1 in
         let prop' = return_result arg1 prop ret_ids in
         [(prop', path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@@ -2150,9 +2177,10 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp1, _); (lexp2, _); (lexp3, _)] ->
-        let n_lexp1, prop = exp_norm_check_arith pdesc _prop lexp1 in
-        let n_lexp2, prop = exp_norm_check_arith pdesc _prop lexp2 in
-        let n_lexp3, prop = exp_norm_check_arith pdesc _prop lexp3 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp1, prop = exp_norm_check_arith pname _prop lexp1 in
+        let n_lexp2, prop = exp_norm_check_arith pname _prop lexp2 in
+        let n_lexp3, prop = exp_norm_check_arith pname _prop lexp3 in
         (match n_lexp1, n_lexp2, n_lexp3 with
          | Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
              (let n = Sil.Int.to_int n_sil in
@@ -2175,8 +2203,9 @@ module ModelBuiltins = struct
     : Builtin.ret_typ =
     match args with
     | [(lexp1, _); (lexp2, _)] ->
-        let n_lexp1, _prop' = exp_norm_check_arith pdesc _prop lexp1 in
-        let n_lexp2, prop = exp_norm_check_arith pdesc _prop' lexp2 in
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp1, _prop' = exp_norm_check_arith pname _prop lexp1 in
+        let n_lexp2, prop = exp_norm_check_arith pname _prop' lexp2 in
         (match n_lexp1, n_lexp2 with
          | Sil.Const (Sil.Ctuple el), Sil.Const (Sil.Cint i) ->
              let n = Sil.Int.to_int i in
diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml
index 77749581c..d15156c2b 100644
--- a/infer/src/checkers/annotations.ml
+++ b/infer/src/checkers/annotations.ml
@@ -146,23 +146,28 @@ let ia_is ann ia = match ann with
 
 type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
 
-(** Get a method signature with annotations from a proc_name and proc_desc,
-    or search in the .specs file if it is not defined in the proc_desc. *)
-let get_annotated_signature get_method_annotation proc_desc proc_name : annotated_signature =
-  let method_annotation = get_method_annotation proc_name proc_desc in
-  let formals = Cfg.Procdesc.get_formals proc_desc in
-  let ret_type = Cfg.Procdesc.get_ret_type proc_desc in
-  let (ia, ial) = method_annotation in
+
+(** Get a method signature with annotations from a proc_attributes. *)
+let get_annotated_signature proc_attributes : annotated_signature =
+  let method_annotation = proc_attributes.ProcAttributes.method_annotation in
+  let formals = proc_attributes.ProcAttributes.formals in
+  let ret_type = proc_attributes.ProcAttributes.ret_type in
+  let (ia, ial0) = method_annotation in
   let natl =
     let rec extract ial parl = match ial, parl with
-      | ia :: ial', (name, typ) :: parl' -> (name, ia, typ) :: extract ial' parl'
-      | [], (name, typ) :: parl' -> (name, Sil.item_annotation_empty, typ) :: extract [] parl'
-      | [], [] -> []
-      | _ :: _, [] -> assert false in
-    list_rev (extract (list_rev ial) (list_rev formals)) in
+      | ia :: ial', (name, typ) :: parl' ->
+          (name, ia, typ) :: extract ial' parl'
+      | [], (name, typ) :: parl' ->
+          (name, Sil.item_annotation_empty, typ) :: extract [] parl'
+      | [], [] ->
+          []
+      | _ :: _, [] ->
+          assert false in
+    list_rev (extract (list_rev ial0) (list_rev formals)) in
   let annotated_signature = { ret = (ia, ret_type); params = natl } in
   annotated_signature
 
+
 (** Check if the annotated signature is for a wrapper of an anonymous inner class method.
     These wrappers have the same name as the original method, every type is Object, and the parameters
     are called x0, x1, x2. *)
diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli
index 4e83f081c..78611aaa4 100644
--- a/infer/src/checkers/annotations.mli
+++ b/infer/src/checkers/annotations.mli
@@ -44,9 +44,8 @@ val equal : annotated_signature -> annotated_signature -> bool
 
 type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
 
-(** Get the annotated signature of the procedure *)
-val get_annotated_signature :
-  get_method_annotation -> Cfg.Procdesc.t -> Procname.t -> annotated_signature
+(** Get a method signature with annotations from a proc_attributes. *)
+val get_annotated_signature : ProcAttributes.t -> annotated_signature
 
 (** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *)
 val get_field_type_and_annotation :
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index ff60241b9..bef68ac3e 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -76,6 +76,7 @@ module ST = struct
         (Option.default "" advice)
         [("always_report", string_of_bool always_report)] in
     let exn = exception_kind kind localized_description in
+    let proc_attributes = Specs.pdesc_resolve_attributes proc_desc in
 
     (* Errors can be suppressed with annotations. An error of kind CHECKER_ERROR_NAME can be
        suppressed with the following annotations:
@@ -101,11 +102,11 @@ module ST = struct
 
       let is_method_suppressed =
         Annotations.ma_has_annotation_with
-          (Specs.proc_get_method_annotation proc_name proc_desc)
+          proc_attributes.ProcAttributes.method_annotation
           annotation_matches in
 
       let is_field_suppressed =
-        match field_name, PatternMatch.get_this_type proc_desc with
+        match field_name, PatternMatch.get_this_type proc_attributes with
         | Some field_name, Some t -> begin
             match (Annotations.get_field_type_and_annotation field_name t) with
             | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches
@@ -114,7 +115,7 @@ module ST = struct
         | _ -> false in
 
       let is_class_suppressed =
-        match (PatternMatch.get_this_type proc_desc) with
+        match PatternMatch.get_this_type proc_attributes with
         | Some t -> begin
             match (PatternMatch.type_get_annotation t) with
             | Some ia -> Annotations.ia_has_annotation_with ia annotation_matches
@@ -338,7 +339,7 @@ let callback_test_state all_procs get_proc_desc idenv tenv proc_name proc_desc =
 
 (** Check the uses of VisibleForTesting *)
 let callback_checkVisibleForTesting all_procs get_proc_desc idenv tenv proc_name proc_desc =
-  let ma = Specs.proc_get_method_annotation proc_name proc_desc in
+  let ma = (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
   if Annotations.ma_contains ma [Annotations.visibleForTesting] then
     begin
       let loc = Cfg.Procdesc.get_loc proc_desc in
diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml
index def42c9ab..1525a3c19 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).ProcAttributes.method_annotation in
+      (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
     let new_summ =
       {
         old_summ with
@@ -177,7 +177,7 @@ struct
           let do_proc (init_pn, init_pd) =
             let filter callee_pn callee_pd =
               let is_private =
-                let attr = Specs.proc_get_attributes callee_pn callee_pd in
+                let attr = Specs.pdesc_resolve_attributes callee_pd in
                 attr.ProcAttributes.access = Sil.Private in
               let same_class =
                 let get_class_opt pn =
@@ -215,7 +215,8 @@ struct
         (** Get the final typestates of all the initializers. *)
         let final_typestates = ref [] in
         let get_final_typestate (pname, pdesc) =
-          let ann_sig = Models.get_annotated_signature pdesc pname in
+          let ann_sig =
+            Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in
           let loc = Cfg.Procdesc.get_loc pdesc in
           let idenv_pn = Idenv.create_from_idenv idenv pdesc in
           match typecheck_proc false idenv_pn pname pdesc ann_sig loc with
@@ -238,8 +239,10 @@ struct
       let final_initializer_typestates_lazy = lazy
         begin
           let is_initializer pdesc pname =
-            PatternMatch.method_is_initializer tenv pname pdesc ||
-            let ia, _ = (Models.get_annotated_signature pdesc pname).Annotations.ret in
+            PatternMatch.method_is_initializer tenv (Cfg.Procdesc.get_attributes pdesc) ||
+            let ia, _ =
+              (Models.get_modelled_annotated_signature
+                 (Cfg.Procdesc.get_attributes pdesc)).Annotations.ret in
             Annotations.ia_is_initializer ia in
           let initializers_current_class =
             pname_and_pdescs_with
@@ -306,15 +309,17 @@ struct
 
     let filter_special_cases () =
       if Procname.java_is_access_method proc_name ||
-         (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_bridge_method
+         (Specs.pdesc_resolve_attributes 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).ProcAttributes.is_abstract then
+          let annotated_signature =
+            Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in
+          if (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_abstract then
             begin
               if Models.infer_library_return &&
-                 EradicateChecks.classify_procedure proc_name proc_desc = "L" then
+                 EradicateChecks.classify_procedure (Cfg.Procdesc.get_attributes proc_desc) = "L"
+              then
                 (let ret_is_nullable = (* get the existing annotation *)
                    let ia, _ = annotated_signature.Annotations.ret in
                    Annotations.ia_is_nullable ia in
diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml
index dfe0ef264..bec28b30d 100644
--- a/infer/src/checkers/eradicateChecks.ml
+++ b/infer/src/checkers/eradicateChecks.ml
@@ -55,13 +55,14 @@ let explain_expr node e =
   | None -> None
 
 (** Classify a procedure. *)
-let classify_procedure pn pd =
+let classify_procedure proc_attributes =
+  let pn = proc_attributes.ProcAttributes.proc_name in
   let unique_id = Procname.to_unique_id pn in
   let classification =
     if Models.is_modelled_nullable pn then "M" (* modelled *)
     else if Models.is_ret_library pn then "R" (* return library *)
-    else if Specs.proc_is_library pn pd then "L" (* library *)
-    else if not (Cfg.Procdesc.is_defined pd) then "S" (* skip *)
+    else if Specs.proc_is_library proc_attributes then "L" (* library *)
+    else if not proc_attributes.ProcAttributes.is_defined then "S" (* skip *)
     else if string_is_prefix "com.facebook" unique_id then "F" (* FB *)
     else "?" in
   classification
@@ -248,7 +249,7 @@ let check_constructor_initialization
   State.set_node start_node;
   if Procname.is_constructor curr_pname
   then begin
-    match PatternMatch.get_this_type curr_pdesc with
+    match PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc) with
     | Some (Sil.Tptr (Sil.Tstruct (ftal, _, _, nameo, _, _, _) as ts, _)) ->
         let do_fta (fn, ft, ia) =
           let annotated_with f = match get_field_annotation fn ts with
@@ -375,7 +376,8 @@ let check_return_annotation
         return_not_nullable
     | _ ->
         false in
-  if Models.infer_library_return && classify_procedure curr_pname curr_pdesc = "L"
+  if Models.infer_library_return &&
+     classify_procedure (Cfg.Procdesc.get_attributes curr_pdesc) = "L"
   then pp_inferred_return_annotation return_not_nullable curr_pname
 
 (** Check the receiver of a virtual call. *)
@@ -418,9 +420,10 @@ let check_call_receiver
 
 (** Check the parameters of a call. *)
 let check_call_parameters
-    find_canonical_duplicate curr_pname node typestate callee_pname
-    callee_pdesc sig_params call_params loc annotated_signature
+    find_canonical_duplicate curr_pname node typestate callee_attributes
+    sig_params call_params loc annotated_signature
     instr_ref typecheck_expr print_current_state : unit =
+  let callee_pname = callee_attributes.ProcAttributes.proc_name in
   let has_this = is_virtual sig_params in
   let tot_param_num = list_length sig_params - (if has_this then 1 else 0) in
   let rec check sparams cparams = match sparams, cparams with
@@ -455,7 +458,7 @@ let check_call_parameters
             let origin_descr = TypeAnnotation.descr_origin ta2 in
 
             let param_num = list_length sparams' + (if has_this then 0 else 1) in
-            let callee_loc = Cfg.Procdesc.get_loc callee_pdesc in
+            let callee_loc = callee_attributes.ProcAttributes.loc in
             report_error
               find_canonical_duplicate
               node
@@ -477,7 +480,7 @@ let check_call_parameters
     if check_library_calls then true
     else
       Models.is_modelled_nullable callee_pname ||
-      Cfg.Procdesc.is_defined callee_pdesc ||
+      callee_attributes.ProcAttributes.is_defined ||
       Specs.get_summary callee_pname <> None in
   if should_check_parameters then
     (* left to right to avoid guessing the different lengths *)
@@ -530,13 +533,12 @@ let check_overridden_annotations
       ignore (list_fold_left2 compare initial_pos current_params overridden_params) in
 
   let check overriden_proc_name =
-    (* TODO (#5280260): investigate why proc_desc may not be found *)
-    match get_proc_desc overriden_proc_name with
-    | Some overriden_proc_desc ->
-        let overriden_signature =
-          Models.get_annotated_signature overriden_proc_desc overriden_proc_name in
-        check_return overriden_proc_name overriden_signature;
-        check_params overriden_proc_name overriden_signature
-    | None -> () in
+    match Specs.proc_resolve_attributes get_proc_desc overriden_proc_name with
+    | Some attributes ->
+        let overridden_signature = Models.get_modelled_annotated_signature attributes in
+        check_return overriden_proc_name overridden_signature;
+        check_params overriden_proc_name overridden_signature
+    | None ->
+        () in
 
   PatternMatch.proc_iter_overridden_methods check tenv proc_name
diff --git a/infer/src/checkers/models.ml b/infer/src/checkers/models.ml
index 6c433df4f..3a6e3754b 100644
--- a/infer/src/checkers/models.ml
+++ b/infer/src/checkers/models.ml
@@ -114,21 +114,21 @@ let ret_library_table : table_t Lazy.t =
 lazy (Marshal.from_string Eradicate_library.marshalled_library_table 0)
 *)
 
+
 (** Return the annotated signature of the procedure, taking into account models. *)
-let get_annotated_signature callee_pdesc callee_pname =
-  let annotated_signature =
-    Annotations.get_annotated_signature
-      Specs.proc_get_method_annotation callee_pdesc callee_pname in
-  let proc_id = Procname.to_unique_id callee_pname in
+let get_modelled_annotated_signature proc_attributes =
+  let proc_name = proc_attributes.ProcAttributes.proc_name in
+  let annotated_signature = Annotations.get_annotated_signature proc_attributes in
+  let proc_id = Procname.to_unique_id proc_name in
   let infer_parameters ann_sig =
     let mark_par =
-      if Inference.enabled then Inference.proc_parameters_marked callee_pname
+      if Inference.enabled then Inference.proc_parameters_marked proc_name
       else None in
     match mark_par with
     | None -> ann_sig
     | Some bs ->
         let mark = (false, bs) in
-        Annotations.annotated_signature_mark callee_pname Annotations.Nullable ann_sig mark in
+        Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark in
   let infer_return ann_sig =
     let mark_r =
       let from_library =
@@ -137,16 +137,17 @@ let get_annotated_signature callee_pdesc callee_pname =
             Hashtbl.find (Lazy.force ret_library_table) proc_id
           with Not_found -> false
         else false in
-      let from_inference = Inference.enabled && Inference.proc_return_is_marked callee_pname in
+      let from_inference = Inference.enabled &&
+                           Inference.proc_return_is_marked proc_name in
       from_library || from_inference in
     if mark_r
-    then Annotations.annotated_signature_mark_return callee_pname Annotations.Nullable ann_sig
+    then Annotations.annotated_signature_mark_return proc_name Annotations.Nullable ann_sig
     else ann_sig in
   let lookup_models_nullable ann_sig =
     if use_models then
       try
         let mark = Hashtbl.find annotated_table_nullable proc_id in
-        Annotations.annotated_signature_mark callee_pname Annotations.Nullable ann_sig mark
+        Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark
       with Not_found ->
         ann_sig
     else ann_sig in
@@ -154,7 +155,7 @@ let get_annotated_signature callee_pdesc callee_pname =
     if use_models then
       try
         let mark = Hashtbl.find annotated_table_present proc_id in
-        Annotations.annotated_signature_mark callee_pname Annotations.Present ann_sig mark
+        Annotations.annotated_signature_mark proc_name Annotations.Present ann_sig mark
       with Not_found ->
         ann_sig
     else ann_sig in
@@ -162,7 +163,7 @@ let get_annotated_signature callee_pdesc callee_pname =
     if use_models
        && Hashtbl.mem annotated_table_strict proc_id
     then
-      Annotations.annotated_signature_mark_return_strict callee_pname ann_sig
+      Annotations.annotated_signature_mark_return_strict proc_name ann_sig
     else
       ann_sig in
 
@@ -173,6 +174,7 @@ let get_annotated_signature callee_pdesc callee_pname =
   |> infer_return
   |> infer_parameters
 
+
 (** Return true when the procedure has been modelled for nullable. *)
 let is_modelled_nullable proc_name =
   if use_models then
diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml
index 381d5faaa..bbc1da7ad 100644
--- a/infer/src/checkers/patternMatch.ml
+++ b/infer/src/checkers/patternMatch.ml
@@ -32,7 +32,7 @@ let is_direct_subtype_of this_type super_type_name =
   | _ -> false
 
 (** The type the method is invoked on *)
-let get_this_type proc_desc = match Cfg.Procdesc.get_formals proc_desc with
+let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals with
   | (n, t):: args -> Some t
   | _ -> None
 
@@ -275,12 +275,11 @@ let type_has_initializer
 (** Check if the method is one of the known initializer methods. *)
 let method_is_initializer
     (tenv: Sil.tenv)
-    (proc_name: Procname.t)
-    (proc_desc: Cfg.Procdesc.t) : bool =
-  match get_this_type proc_desc with
+    (proc_attributes: ProcAttributes.t) : bool =
+  match get_this_type proc_attributes with
   | Some this_type ->
       if type_has_initializer tenv this_type then
-        let mname = Procname.java_get_method proc_name in
+        let mname = Procname.java_get_method (proc_attributes.ProcAttributes.proc_name) in
         list_exists (string_equal mname) initializer_methods
       else
         false
diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli
index 8ed45c912..5beb76434 100644
--- a/infer/src/checkers/patternMatch.mli
+++ b/infer/src/checkers/patternMatch.mli
@@ -18,7 +18,7 @@ val get_java_method_call_formal_signature :
   Sil.instr -> (string * string * string list * string) option
 
 (** Get the this type of a procedure *)
-val get_this_type : Cfg.Procdesc.t -> Sil.typ option
+val get_this_type : ProcAttributes.t -> Sil.typ option
 
 (** Get the name of a type *)
 val get_type_name : Sil.typ -> string
@@ -29,7 +29,7 @@ val get_vararg_type_names : Cfg.Node.t -> Sil.pvar -> string list
 val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.t -> string list -> bool
 
 (** Check if the method is one of the known initializer methods. *)
-val method_is_initializer : Sil.tenv -> Procname.t -> Cfg.Procdesc.t -> bool
+val method_is_initializer : Sil.tenv -> ProcAttributes.t -> bool
 
 (** Is this a getter proc name? *)
 val is_getter : Procname.t -> bool
diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml
index 2103aeee4..e2c27f088 100644
--- a/infer/src/checkers/repeatedCallsChecker.ml
+++ b/infer/src/checkers/repeatedCallsChecker.ml
@@ -99,12 +99,10 @@ struct
         let proc_throws pn = Dataflow.DontKnow
       end) in
 
-    if Cfg.Procdesc.is_defined pdesc then
-      let transitions = DFAllocCheck.run pdesc None in
-      match transitions (Cfg.Procdesc.get_exit_node pdesc) with
-      | DFAllocCheck.Transition (loc, _, _) -> loc
-      | DFAllocCheck.Dead_state -> None
-    else None
+    let transitions = DFAllocCheck.run pdesc None in
+    match transitions (Cfg.Procdesc.get_exit_node pdesc) with
+    | DFAllocCheck.Transition (loc, _, _) -> loc
+    | DFAllocCheck.Dead_state -> None
 
   (** Check repeated calls to the same procedure. *)
   let check_instr get_proc_desc curr_pname curr_pdesc node extension instr normalized_etl =
@@ -127,11 +125,11 @@ struct
             normalized_etl,
             loc,
             call_flags) in
-        let report callee_pdesc =
+        let report proc_desc =
           match get_old_call instr_normalized_args extension with
           | Some (Sil.Call (_, _, _, loc_old, _)) ->
               begin
-                match proc_performs_allocation callee_pdesc AllPaths with
+                match proc_performs_allocation proc_desc AllPaths with
                 | Some alloc_loc ->
                     let description =
                       Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)"
@@ -147,7 +145,9 @@ struct
 
         let () = match get_proc_desc callee_pname with
           | None -> ()
-          | Some callee_pdesc -> report callee_pdesc in
+          | Some proc_desc ->
+              if Cfg.Procdesc.is_defined proc_desc
+              then report proc_desc in
         add_call instr_normalized_args extension
     | _ -> extension
 
diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml
index 2c6f01eb7..a187d7cef 100644
--- a/infer/src/checkers/typeCheck.ml
+++ b/infer/src/checkers/typeCheck.ml
@@ -365,9 +365,10 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
     then calls_this := true in
 
   (* Drops hidden and synthetic parameters which we do not check in a call. *)
-  let drop_unchecked_params calls_this pdesc pname params =
+  let drop_unchecked_params calls_this proc_attributes params =
+    let pname = proc_attributes.ProcAttributes.proc_name in
     if Procname.is_constructor pname then
-      match PatternMatch.get_this_type pdesc with
+      match PatternMatch.get_this_type proc_attributes with
       | Some this_type ->
           begin
             constructor_check_calls_this calls_this pname;
@@ -379,11 +380,11 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
             let rec drop_n_args ntl = match ntl with
               | fp:: tail when is_hidden_parameter fp -> 1 + drop_n_args tail
               | _ -> 0 in
-            let n = drop_n_args (Cfg.Procdesc.get_formals pdesc) in
+            let n = drop_n_args proc_attributes.ProcAttributes.formals in
             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).ProcAttributes.is_synthetic_method then
+            if proc_attributes.ProcAttributes.is_synthetic_method then
               list_drop_last 1 visible_params
             else
               visible_params
@@ -393,9 +394,9 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
       params in
 
   (* 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).ProcAttributes.is_synthetic_method then
+  let drop_unchecked_signature_params proc_attributes annotated_signature =
+    if Procname.is_constructor (proc_attributes.ProcAttributes.proc_name) &&
+       proc_attributes.ProcAttributes.is_synthetic_method then
       list_drop_last 1 annotated_signature.Annotations.params
     else
       annotated_signature.Annotations.params in
@@ -532,12 +533,14 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
       typestate (* skip othe builtins *)
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
     when get_proc_desc callee_pname <> None ->
-      let callee_pdesc = match get_proc_desc callee_pname with
-        | Some callee_pdesc -> callee_pdesc
+      let callee_attributes =
+        match get_proc_desc callee_pname with
+        | Some pdesc ->
+            Specs.pdesc_resolve_attributes pdesc
         | None -> assert false in
-      let callee_loc = Cfg.Procdesc.get_loc callee_pdesc in
+      let callee_loc = callee_attributes.ProcAttributes.loc in
 
-      let etl = drop_unchecked_params calls_this callee_pdesc callee_pname _etl in
+      let etl = drop_unchecked_params calls_this callee_attributes _etl in
       let call_params, typestate1 =
         let handle_et (e1, t1) (etl1, typestate1) =
           typecheck_expr_for_errors typestate e1 loc;
@@ -545,11 +548,10 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
           (((e1, e2), t1) :: etl1), typestate2 in
         list_fold_right handle_et etl ([], typestate) in
 
-      let annotated_signature = Models.get_annotated_signature callee_pdesc callee_pname in
-      let signature_params = drop_unchecked_signature_params
-          callee_pdesc
-          callee_pname
-          annotated_signature in
+      let annotated_signature =
+        Models.get_modelled_annotated_signature callee_attributes in
+      let signature_params =
+        drop_unchecked_signature_params callee_attributes annotated_signature in
 
       let is_anonymous_inner_class_constructor =
         Procname.java_is_anonymous_inner_class_constructor callee_pname in
@@ -559,7 +561,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
         | [] -> typestate'
         | [id] ->
             let (ia, ret_typ) = annotated_signature.Annotations.ret in
-            let is_library = Specs.proc_is_library callee_pname callee_pdesc in
+            let is_library = Specs.proc_is_library callee_attributes in
             let origin = TypeOrigin.Proc (callee_pname, loc', annotated_signature, is_library) in
             TypeState.add_id
               id
@@ -692,7 +694,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
               begin
                 let unique_id = Procname.to_unique_id callee_pname in
                 let classification =
-                  EradicateChecks.classify_procedure callee_pname callee_pdesc in
+                  EradicateChecks.classify_procedure callee_attributes in
                 L.stdout "  %s unique id: %s@." classification unique_id
               end;
             if cflags.Sil.cf_virtual && checks.eradicate then
@@ -714,8 +716,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
                 curr_pname
                 node
                 typestate1
-                callee_pname
-                callee_pdesc
+                callee_attributes
                 signature_params
                 call_params
                 loc
@@ -943,13 +944,14 @@ let typecheck_node
   let typestates_exn = ref [] in
   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
         (* check if the call might throw an exception *)
-        let exceptions =
-          match get_proc_desc callee_pname with
-          | Some callee_pdesc ->
-              (Specs.proc_get_attributes callee_pname callee_pdesc).ProcAttributes.exceptions
-          | None -> [] in
-        if exceptions <> [] then
+        let has_exceptions = match callee_attributes_opt with
+          | Some callee_attributes ->
+              callee_attributes.ProcAttributes.exceptions <> []
+          | None -> false in
+        if has_exceptions then
           typestates_exn := typestate :: !typestates_exn
     | Sil.Set (Sil.Lvar pv, _, _, _) when
         Sil.pvar_is_return pv &&