diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 2688a122c..4ff29c96b 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -667,19 +667,13 @@ let get_flag summary key =
     Some (Hashtbl.find proc_flags key)
   with Not_found -> None
 
-(** Return the specs and parameters for the proc in the spec table *)
-let get_specs_formals proc_name =
+(** Return the specs for the proc in the spec table *)
+let get_specs proc_name =
   match get_summary proc_name with
   | None ->
-      raise (Failure ("Specs.get_specs_formals: " ^ (Typ.Procname.to_string proc_name) ^ "Not_found"))
+      failwithf "Specs.get_specs: %a not found" Typ.Procname.pp proc_name
   | Some summary ->
-      let specs = get_specs_from_payload summary in
-      let formals = get_formals summary in
-      (specs, formals)
-
-(** Return the specs for the proc in the spec table *)
-let get_specs proc_name =
-  fst (get_specs_formals proc_name)
+      get_specs_from_payload summary
 
 (** Return the current phase for the proc *)
 let get_phase summary =
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 62ee22394..e668400df 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -194,9 +194,6 @@ val get_signature : summary -> string
 (** Return the specs for the proc in the spec table *)
 val get_specs : Typ.Procname.t -> Prop.normal spec list
 
-(** Return the specs and formal parameters for the proc in the spec table *)
-val get_specs_formals : Typ.Procname.t -> Prop.normal spec list * (Mangled.t * Typ.t) list
-
 (** Get the specs from the payload of the summary. *)
 val get_specs_from_payload : summary -> Prop.normal spec list
 
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index e06e447ca..5ad930af9 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1567,10 +1567,11 @@ and sym_exec_objc_accessor property_accesor ret_typ tenv ret_id pdesc _ loc args
   |> List.map ~f:(fun p -> (p, path))
 
 (** Perform symbolic execution for a function call *)
-and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc; } =
+and proc_call
+    callee_summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc; } =
   let caller_pname = Procdesc.get_proc_name pdesc in
-  let callee_pname = Specs.get_proc_name summary in
-  let ret_typ = Specs.get_ret_type summary in
+  let callee_pname = Specs.get_proc_name callee_summary in
+  let ret_typ = Specs.get_ret_type callee_summary in
   let check_return_value_ignored () =
     (* check if the return value of the call is ignored, and issue a warning *)
     let is_ignored = match ret_typ.Typ.desc, ret_id with
@@ -1578,13 +1579,13 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
       | _, None -> true
       | _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in
     if is_ignored
-    && is_none (Specs.get_flag summary ProcAttributes.proc_flag_ignore_return) then
+    && is_none (Specs.get_flag callee_summary ProcAttributes.proc_flag_ignore_return) then
       let err_desc = Localise.desc_return_value_ignored callee_pname loc in
       let exn = (Exceptions.Return_value_ignored (err_desc, __POS__)) in
       Reporting.log_warning caller_pname exn in
   check_inherently_dangerous_function caller_pname callee_pname;
   begin
-    let formal_types = List.map ~f:(fun (_, typ) -> typ) (Specs.get_formals summary) in
+    let formal_types = List.map ~f:snd (Specs.get_formals callee_summary) in
     let rec comb actual_pars formal_types =
       match actual_pars, formal_types with
       | [], [] -> actual_pars
@@ -1614,14 +1615,14 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
     check_return_value_ignored ();
     (* In case we call an objc instance method we add and extra spec *)
     (* were the receiver is null and the semantics of the call is nop*)
-    let callee_attrs = Specs.get_attributes summary in
+    (* let callee_attrs = Specs.get_attributes callee_summary in *)
     if (!Config.curr_language <> Config.Java)  &&
-       (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then
+       (Specs.get_attributes callee_summary).ProcAttributes.is_objc_instance_method then
       handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc
-        callee_pname loc path (Tabulation.exe_function_call callee_attrs)
+        callee_pname loc path (Tabulation.exe_function_call callee_summary)
     else  (* non-objective-c method call. Standard tabulation *)
       Tabulation.exe_function_call
-        callee_attrs tenv ret_id pdesc callee_pname loc actual_params pre path
+        callee_summary tenv ret_id pdesc callee_pname loc actual_params pre path
   end
 
 (** perform symbolic execution for a single prop, and check for junk *)
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 148960118..51a2a6789 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -116,13 +116,15 @@ let spec_rename_vars pname spec =
 
 (** Find and number the specs for [proc_name],
     after renaming their vars, and also return the parameters *)
-let spec_find_rename trace_call (proc_name : Typ.Procname.t)
+let spec_find_rename trace_call summary
   : (int * Prop.exposed Specs.spec) list * Pvar.t list =
+  let proc_name = Specs.get_proc_name summary in
   try
     let count = ref 0 in
     let f spec =
       incr count; (!count, spec_rename_vars proc_name spec) in
-    let specs, formals = Specs.get_specs_formals proc_name in
+    let specs = Specs.get_specs proc_name in
+    let formals = Specs.get_formals summary in
     if List.is_empty specs then
       begin
         trace_call Specs.CallStats.CR_not_found;
@@ -1286,15 +1288,14 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
 
 (** Execute the function call and return the list of results with return value *)
 let exe_function_call
-    callee_attrs tenv ret_id caller_pdesc callee_pname loc actual_params prop path =
+    callee_summary tenv ret_id caller_pdesc callee_pname loc actual_params prop path =
+  let callee_attrs = Specs.get_attributes callee_summary in
   let caller_pname = Procdesc.get_proc_name caller_pdesc in
+  let caller_summary = Specs.get_summary_unsafe "exe_function_call" caller_pname in
   let trace_call res =
-    match Specs.get_summary caller_pname with
-    | None -> ()
-    | Some summary ->
-        Specs.CallStats.trace
-          summary.Specs.stats.Specs.call_stats callee_pname loc res !Config.footprint in
-  let spec_list, formal_params = spec_find_rename trace_call callee_pname in
+    Specs.CallStats.trace
+      caller_summary.Specs.stats.Specs.call_stats callee_pname loc res !Config.footprint in
+  let spec_list, formal_params = spec_find_rename trace_call callee_summary in
   let nspecs = List.length spec_list in
   L.d_strln
     ("Found " ^
diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli
index 9b3e76fd4..a1f7ae13d 100644
--- a/infer/src/backend/tabulation.mli
+++ b/infer/src/backend/tabulation.mli
@@ -44,6 +44,6 @@ val d_splitting : splitting -> unit
 
 (** Execute the function call and return the list of results with return value *)
 val exe_function_call:
-  ProcAttributes.t -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Typ.Procname.t ->
+  Specs.summary -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Typ.Procname.t ->
   Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t ->
   (Prop.normal Prop.t * Paths.Path.t) list