diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml
index 5e8cfd778..557e1fb4d 100644
--- a/infer/src/backend/cfg.ml
+++ b/infer/src/backend/cfg.ml
@@ -333,7 +333,8 @@ module Node = struct
   let replace_instrs node instrs =
     node.nd_instrs <- instrs
 
-  let proc_desc_get_ret_var pdesc = Sil.mk_pvar Ident.name_return pdesc.pd_name
+  let proc_desc_get_ret_var pdesc =
+    Sil.get_ret_pvar pdesc.pd_name
 
   (** Add declarations for local variables and return variable to the node *)
   let add_locals_ret_declaration node locals =
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 944227186..08d086349 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -246,11 +246,11 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
 (* =============== START of symbolic execution =============== *)
 
 (* propagate a set of results to the given node *)
-let propagate proc_desc is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
+let propagate pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
   let edgeset_todo =
     let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *)
       let exn_opt =
-        if is_exception then Some (Tabulation.prop_get_exn_name proc_desc prop)
+        if is_exception then Some (Tabulation.prop_get_exn_name pname prop)
         else None in
       Paths.PathSet.add_renamed_prop prop (Paths.Path.extend curr_node exn_opt (State.get_session ()) path) edgeset_curr in
     Paths.PathSet.fold f pset Paths.PathSet.empty in
@@ -263,7 +263,7 @@ let propagate_nodes_divergence
     (path: Paths.Path.t) (kind_curr_node : Cfg.Node.nodekind) (_succ_nodes: Cfg.node list)
     (exn_nodes: Cfg.node list) =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
-  let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pdesc) pset in
+  let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
   let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *)
     | Some node_id ->
         list_filter (fun n -> Cfg.Node.get_id n = node_id) _succ_nodes
@@ -281,17 +281,17 @@ let propagate_nodes_divergence
         Paths.PathSet.map mk_incons diverging_states in
       (L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
       Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln ();
-      propagate pdesc false prop_incons exit_node
+      propagate pname false prop_incons exit_node
     end;
-  list_iter (propagate pdesc false pset_ok) succ_nodes;
-  list_iter (propagate pdesc true pset_exn) exn_nodes
+  list_iter (propagate pname false pset_ok) succ_nodes;
+  list_iter (propagate pname true pset_exn) exn_nodes
 
 (* ===================== END of symbolic execution ===================== *)
 
 (* =============== START of forward_tabulate =============== *)
 
 (** Symbolic execution for a Join node *)
-let do_symexec_join proc_desc tenv curr_node (edgeset_todo : Paths.PathSet.t) =
+let do_symexec_join pname tenv curr_node (edgeset_todo : Paths.PathSet.t) =
   let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
   let curr_id = Cfg.Node.get_id curr_node in
@@ -303,7 +303,7 @@ let do_symexec_join proc_desc tenv curr_node (edgeset_todo : Paths.PathSet.t) =
   list_iter (fun node ->
           Paths.PathSet.iter (fun prop path ->
                   State.set_path path None;
-                  propagate proc_desc false (Paths.PathSet.from_renamed_list [(prop, path)]) node)
+                  propagate pname false (Paths.PathSet.from_renamed_list [(prop, path)]) node)
             new_dset') succ_nodes
 
 let prop_max_size = ref (0, Prop.prop_emp)
@@ -549,7 +549,7 @@ let forward_tabulate cfg tenv =
       L.d_ln (); L.d_ln ();
 
       match kind_curr_node with
-      | Cfg.Node.Join_node -> do_symexec_join proc_desc tenv curr_node pathset_todo
+      | Cfg.Node.Join_node -> do_symexec_join proc_name tenv curr_node pathset_todo
       | Cfg.Node.Stmt_node _
       | Cfg.Node.Prune_node _
       | Cfg.Node.Exit_node _
@@ -940,10 +940,10 @@ let reset_global_counters cfg proc_name proc_desc =
   set_current_language cfg proc_desc
 
 (* Collect all pairs of the kind (precondition, exception) from a summary *)
-let exception_preconditions tenv pdesc summary =
+let exception_preconditions tenv pname summary =
   let collect_exceptions pre exns (prop, path) =
-    if Tabulation.prop_is_exn pdesc prop then
-      let exn_name = Tabulation.prop_get_exn_name pdesc prop in
+    if Tabulation.prop_is_exn pname prop then
+      let exn_name = Tabulation.prop_get_exn_name pname prop in
       if AndroidFramework.is_runtime_exception tenv exn_name then
         (pre, exn_name):: exns
       else exns
@@ -984,19 +984,19 @@ let remove_this_not_null prop =
 (** Detects if there are specs of the form {precondition} proc {runtime exception} and report
 an error in that case, generating the trace that lead to the runtime exception if the method is
 called in the context { precondition } *)
-let report_runtime_exceptions tenv cfg proc_desc summary =
-  let proc_name = Specs.get_proc_name summary in
+let report_runtime_exceptions tenv cfg pdesc summary =
+  let pname = Specs.get_proc_name summary in
   let is_public_method =
     (Specs.get_attributes summary).Sil.access = Sil.Public in
   let is_main =
     is_public_method
     (* TODO (#4559939): add check for static method *)
-    && Procname.is_java proc_name
-    && (Procname.java_get_method proc_name) = "main" in
+    && Procname.is_java pname
+    && (Procname.java_get_method pname) = "main" in
   let is_annotated =
     let annotated_signature =
       Annotations.get_annotated_signature
-        Specs.proc_get_method_annotation proc_desc proc_name in
+        Specs.proc_get_method_annotation pdesc pname in
     let ret_annotation, _ = annotated_signature.Annotations.ret in
     Annotations.ia_is_verify ret_annotation in
   let is_unavoidable pre =
@@ -1011,10 +1011,10 @@ let report_runtime_exceptions tenv cfg proc_desc summary =
     if should_report pre then
       let pre_str =
         Utils.pp_to_string (Prop.pp_prop pe_text) (Specs.Jprop.to_prop pre) in
-      let exn_desc = Localise.java_unchecked_exn_desc proc_name runtime_exception pre_str in
+      let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in
       let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in
-      Reporting.log_error proc_name ~pre: (Some (Specs.Jprop.to_prop pre)) exn in
-  list_iter report (exception_preconditions tenv proc_desc summary)
+      Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in
+  list_iter report (exception_preconditions tenv pname summary)
 
 
 (** update a summary after analysing a procedure *)
diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml
index d5aaf920e..ee62e6301 100644
--- a/infer/src/backend/sil.ml
+++ b/infer/src/backend/sil.ml
@@ -3776,7 +3776,8 @@ let pp_tenv f (tenv : tenv) =
 let mk_pvar (name: Mangled.t) (proc_name: Procname.t) : pvar =
   { pv_name = name; pv_kind = Local_var proc_name }
 
-let mk_ret_var pname =
+
+let get_ret_pvar pname =
   mk_pvar Ident.name_return pname
 
 (** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *)
diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli
index 01ab436d3..36c147861 100644
--- a/infer/src/backend/sil.mli
+++ b/infer/src/backend/sil.mli
@@ -1318,8 +1318,8 @@ val loc_none : location
 (** [mk_pvar name proc_name suffix] creates a program var with the given function name and suffix *)
 val mk_pvar : Mangled.t -> Procname.t -> pvar
 
-(** [mk_ret_var proc_name] creates the retun pvar based on the procedure name *)
-val mk_ret_var : Procname.t -> pvar
+(** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name *)
+val get_ret_pvar : Procname.t -> pvar
 
 (** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *)
 val mk_pvar_callee : Mangled.t -> Procname.t -> pvar
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 110dc9abc..826504bbd 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1342,10 +1342,11 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
 
 let lifted_sym_exec
     handle_exn cfg tenv pdesc (pset : Paths.PathSet.t) node (instrs : Sil.instr list)
-: Paths.PathSet.t =
+    : Paths.PathSet.t =
+  let pname = Cfg.Procdesc.get_proc_name pdesc in
   let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
     let pset2 =
-      if Tabulation.prop_is_exn pdesc p && not (Sil.instr_is_auxiliary instr)
+      if Tabulation.prop_is_exn pname p && not (Sil.instr_is_auxiliary instr)
       && Cfg.Node.get_kind node <> Cfg.Node.exn_handler_kind
       (* skip normal instructions if an exception was thrown, unless this is an exception handler node *)
       then
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 51beafec7..1f664cf49 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -537,8 +537,8 @@ let exp_is_exn = function
   | _ -> false
 
 (** check if a prop is an exception *)
-let prop_is_exn pdesc prop =
-  let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in
+let prop_is_exn pname prop =
+  let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in
   let is_exn = function
     | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Sil.exp_equal e1 ret_pvar ->
         exp_is_exn e2
@@ -546,8 +546,8 @@ let prop_is_exn pdesc prop =
   list_exists is_exn (Prop.get_sigma prop)
 
 (** when prop is an exception, return the exception name *)
-let prop_get_exn_name pdesc prop =
-  let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in
+let prop_get_exn_name pname prop =
+  let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in
   let exn_name = ref (Mangled.from_string "") in
   let find_exn_name e =
     let do_hpred = function
@@ -574,8 +574,8 @@ let lookup_global_errors prop =
   search_error (Prop.get_sigma prop)
 
 (** set a prop to an exception sexp *)
-let prop_set_exn pdesc prop se_exn =
-  let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in
+let prop_set_exn pname prop se_exn =
+  let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in
   let map_hpred = function
     | Sil.Hpointsto (e, _, t) when Sil.exp_equal e ret_pvar ->
         Sil.Hpointsto(e, se_exn, t)
@@ -673,7 +673,7 @@ let combine
 
     let post_p3 = (** replace [result|callee] with an aux variable dedicated to this proc *)
       let callee_ret_pvar =
-        Sil.Lvar (Sil.pvar_to_callee callee_pname (Sil.mk_ret_var callee_pname)) in
+        Sil.Lvar (Sil.pvar_to_callee callee_pname (Sil.get_ret_pvar callee_pname)) in
       match Prop.prop_iter_create post_p2 with
       | None -> post_p2
       | Some iter ->
@@ -686,7 +686,7 @@ let combine
               match fst (Prop.prop_iter_current iter') with
               | Sil.Hpointsto (e, Sil.Eexp (e', inst), t) when exp_is_exn e' -> (* resuls is an exception: set in caller *)
                   let p = Prop.prop_iter_remove_curr_then_to_prop iter' in
-                  prop_set_exn caller_pdesc p (Sil.Eexp (e', inst))
+                  prop_set_exn caller_pname p (Sil.Eexp (e', inst))
               | Sil.Hpointsto (e, Sil.Eexp (e', inst), t) when list_length ret_ids = 1 ->
                   let p = Prop.prop_iter_remove_curr_then_to_prop iter' in
                   Prop.conjoin_eq e' (Sil.Var (list_hd ret_ids)) p
diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli
index 21df001e6..d3f17eb0d 100644
--- a/infer/src/backend/tabulation.mli
+++ b/infer/src/backend/tabulation.mli
@@ -23,10 +23,10 @@ val raise_cast_exception :
 Utils.ml_location -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a
 
 (** check if a prop is an exception *)
-val prop_is_exn : Cfg.Procdesc.t -> 'a Prop.t -> bool
+val prop_is_exn : Procname.t -> 'a Prop.t -> bool
 
 (** when prop is an exception, return the exception name *)
-val prop_get_exn_name : Cfg.Procdesc.t -> 'a Prop.t -> Mangled.t
+val prop_get_exn_name : Procname.t -> 'a Prop.t -> Mangled.t
 
 (** search in prop contains an error state *)
 val lookup_global_errors : 'a Prop.t -> Mangled.t option
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 7e4c6b988..1e093d8bb 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -831,13 +831,15 @@ let rec instruction context pc instr : translation =
   let cn = JContext.get_cn context in
   let program = JContext.get_program context in
   let meth_kind = JContext.get_meth_kind context in
+  let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in
+  let ret_var = Sil.get_ret_pvar proc_name in
+  let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
   let loc = get_location (JContext.get_impl context) pc meth_kind cn in
   let match_never_null = JContext.get_never_null_matcher context in
   let create_node node_kind temps sil_instrs =
     Cfg.Node.create
       cfg (get_location (JContext.get_impl context) pc meth_kind cn) node_kind sil_instrs (JContext.get_procdesc context) temps in
   let return_not_null () =
-    let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in
     (match_never_null loc.Sil.file proc_name
       || list_exists (fun p -> Procname.equal p proc_name) JTransType.never_returning_null) in
   try
@@ -858,8 +860,6 @@ let rec instruction context pc instr : translation =
               create_node node_kind [] []
           | Some expr ->
               let (idl, stml, sil_expr) = expression context pc expr in
-              let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
-              let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
               let sil_instrs =
                 let return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in
                 if return_not_null () then
@@ -938,8 +938,6 @@ let rec instruction context pc instr : translation =
     | JBir.Throw expr ->
         let node_kind = Cfg.Node.Stmt_node "throw" in
         let (ids, instrs, sil_expr) = expression context pc expr in
-        let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
-        let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
         let sil_exn = Sil.Const (Sil.Cexn sil_expr) in
         let sil_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
         let node = create_node node_kind ids (instrs @ [sil_instr]) in
@@ -1076,8 +1074,6 @@ let rec instruction context pc instr : translation =
             let ret_opt = Some (Sil.Var ret_id, class_type) in
             method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
-          let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
-          let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
           let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
           let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in
           create_node npe_kind (ids @ call_ids) npe_instrs in
@@ -1133,8 +1129,6 @@ let rec instruction context pc instr : translation =
               context loc pc None out_of_bound_cn constr_ms
               (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
-          let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
-          let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
           let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
           let out_of_bound_instrs =
             instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in
@@ -1173,8 +1167,6 @@ let rec instruction context pc instr : translation =
             method_invocation context loc pc None cce_cn constr_ms
               (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
-          let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
-          let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
           let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
           let cce_instrs =
             instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in