diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml
index e8533ee17..909143795 100644
--- a/infer/src/backend/autounit.ml
+++ b/infer/src/backend/autounit.ml
@@ -490,7 +490,7 @@ let gen_init_equalities code pure =
 (** generate variable declarations *)
 let gen_var_decl code idmap parameters =
   let do_parameter (name, typ) =
-    let pp_name f () = Format.fprintf f "%s" name in
+    let pp_name f () = Mangled.pp f name in
     let pp f () = F.fprintf f "%a;" (Sil.pp_type_decl pe pp_name pp_exp_c) typ in
     Code.add_from_pp code pp in
   let do_vinfo id { typ = typ; alloc = alloc } =
@@ -579,9 +579,8 @@ let gen_hpara code proc_name spec_num env id hpara =
 let gen_hpara_dll code proc_name spec_num env id hpara_dll = assert false
 
 (** Generate epilog for the test case *)
-let gen_epilog code proc_name parameters =
-  let pp_parameter fmt (name, typ) =
-    F.fprintf fmt "%s" name in
+let gen_epilog code proc_name (parameters : (Mangled.t * Sil.typ) list) =
+  let pp_parameter fmt (name, _) = Mangled.pp fmt name in
   let pp f () = F.fprintf f "%a(%a);" Procname.pp proc_name (pp_comma_seq pp_parameter) parameters in
   let line1 = pp_to_string pp () in
   let line2 = "}" in
diff --git a/infer/src/backend/autounit.mli b/infer/src/backend/autounit.mli
index cf3184e8b..672be197e 100644
--- a/infer/src/backend/autounit.mli
+++ b/infer/src/backend/autounit.mli
@@ -17,7 +17,8 @@ type code
 val pp_code : Format.formatter -> code -> unit
 
 (** generate a unit test form a spec *)
-val genunit : string -> Procname.t -> int -> (string * Sil.typ) list -> Prop.normal Specs.spec -> code
+val genunit : string -> Procname.t -> int -> (Mangled.t * Sil.typ) list
+  -> Prop.normal Specs.spec -> code
 
 (** generate code for a main calling all the unit test functions passed as argument *)
 val genmain : (Procname.t * int) list -> code
diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index a2dca318f..d572b6a0d 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -51,7 +51,7 @@ let check_access access_opt de_opt =
     let find_formal_ids node = (* find ids obtained by a letref on a formal parameter *)
       let node_instrs = Cfg.Node.get_instrs node in
       let formals = Cfg.Procdesc.get_formals (Cfg.Node.get_proc_desc node) in
-      let formal_names = IList.map (fun (s, _) -> Mangled.from_string s) formals in
+      let formal_names = IList.map fst formals in
       let is_formal pvar =
         let name = Sil.pvar_get_name pvar in
         IList.exists (Mangled.equal name) formal_names in
diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml
index b9b925e29..beb37e94f 100644
--- a/infer/src/backend/cfg.ml
+++ b/infer/src/backend/cfg.ml
@@ -745,9 +745,6 @@ let add_abstraction_instructions cfg =
     if node_requires_abstraction node then Node.append_instrs_temps node [Sil.Abstract loc] [] in
   IList.iter do_node all_nodes
 
-let get_name_of_parameter (curr_f : Procdesc.t) (x, typ) =
-  Sil.mk_pvar (Mangled.from_string x) (Procdesc.get_proc_name curr_f)
-
 let get_name_of_local (curr_f : Procdesc.t) (x, typ) =
   Sil.mk_pvar x (Procdesc.get_proc_name curr_f)
 
@@ -849,8 +846,9 @@ let remove_locals (curr_f : Procdesc.t) p =
   (removed, if !Config.angelic_execution then remove_abducted_retvars p' else p')
 
 let remove_formals (curr_f : Procdesc.t) p =
-  let names_of_formals = IList.map (get_name_of_parameter curr_f) (Procdesc.get_formals curr_f) in
-  Prop.deallocate_stack_vars p names_of_formals
+  let pname = Procdesc.get_proc_name curr_f in
+  let formal_vars = IList.map (fun (n, _) -> Sil.mk_pvar n pname) (Procdesc.get_formals curr_f) in
+  Prop.deallocate_stack_vars p formal_vars
 
 (** remove the return variable from the prop *)
 let remove_ret (curr_f : Procdesc.t) (p: Prop.normal Prop.t) =
diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli
index 1be1da4a2..ec39e94c8 100644
--- a/infer/src/backend/cfg.mli
+++ b/infer/src/backend/cfg.mli
@@ -60,7 +60,7 @@ module Procdesc : sig
   val get_flags : t -> proc_flags
 
   (** Return name and type of formal parameters *)
-  val get_formals : t -> (string * Sil.typ) list
+  val get_formals : t -> (Mangled.t * Sil.typ) list
 
   (** Return loc information for the procedure *)
   val get_loc : t -> Location.t
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index f886540ee..cc71245d2 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -966,7 +966,7 @@ let pp_cfgnodename fmt (n : Cfg.Node.t) =
 
 let pp_etlist fmt etl =
   IList.iter (fun (id, ty) ->
-      Format.fprintf fmt " %s:%a" id (Sil.pp_typ_full pe_text) ty) etl
+      Format.fprintf fmt " %a:%a" Mangled.pp id (Sil.pp_typ_full pe_text) ty) etl
 
 let pp_local_list fmt etl =
   IList.iter (fun (id, ty) ->
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index a283cf25a..3c7fefe2b 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -803,7 +803,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
     as well as seed variables *)
 let initial_prop tenv (curr_f: Cfg.Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t =
   let construct_decl (x, typ) =
-    (Sil.mk_pvar (Mangled.from_string x) (Cfg.Procdesc.get_proc_name curr_f), typ) in
+    (Sil.mk_pvar x (Cfg.Procdesc.get_proc_name curr_f), typ) in
   let new_formals =
     if add_formals
     then IList.map construct_decl (Cfg.Procdesc.get_formals curr_f)
diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index 0251336a8..184ef8bd0 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -226,7 +226,7 @@ let compute_candidates procdesc : Vset.t * (Vset.t -> Vset.elt list) =
       candidates := Vset.add pv !candidates;
       if typ_is_struct_array typ then struct_array_cand := Vset.add pv !struct_array_cand
     ) in
-  IList.iter add_vi (IList.map (fun (var, typ) -> Mangled.from_string var, typ) (Cfg.Procdesc.get_formals procdesc));
+  IList.iter add_vi (Cfg.Procdesc.get_formals procdesc);
   IList.iter add_vi (Cfg.Procdesc.get_locals procdesc);
   let get_sorted_candidates vs =
     let priority, no_pri = IList.partition (fun pv -> Vset.mem pv !struct_array_cand) (Vset.elements vs) in
diff --git a/infer/src/backend/procAttributes.ml b/infer/src/backend/procAttributes.ml
index 2a35bfe16..196fe8211 100644
--- a/infer/src/backend/procAttributes.ml
+++ b/infer/src/backend/procAttributes.ml
@@ -24,7 +24,7 @@ type t =
     captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *)
     err_log: Errlog.t; (** Error log for the procedure *)
     exceptions : string list; (** exceptions thrown by the procedure *)
-    formals : (string * Sil.typ) list; (** name and type of formal parameters *)
+    formals : (Mangled.t * Sil.typ) list; (** name and type of formal parameters *)
     func_attributes : Sil.func_attribute list;
     is_abstract : bool; (** the procedure is abstract *)
     mutable is_bridge_method : bool; (** the procedure is a bridge method *)
diff --git a/infer/src/backend/procAttributes.mli b/infer/src/backend/procAttributes.mli
index 49ad56e2b..438a699eb 100644
--- a/infer/src/backend/procAttributes.mli
+++ b/infer/src/backend/procAttributes.mli
@@ -21,7 +21,7 @@ type t =
     captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *)
     err_log: Errlog.t; (** Error log for the procedure *)
     exceptions : string list; (** exceptions thrown by the procedure *)
-    formals : (string * Sil.typ) list; (** name and type of formal parameters *)
+    formals : (Mangled.t * Sil.typ) list; (** name and type of formal parameters *)
     func_attributes : Sil.func_attribute list;
     is_abstract : bool; (** the procedure is abstract *)
     mutable is_bridge_method : bool; (** the procedure is a bridge method *)
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index e1a047b5d..6318e8541 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -407,11 +407,13 @@ let describe_phase summary =
 (** Return the signature of a procedure declaration as a string *)
 let get_signature summary =
   let s = ref "" in
-  IList.iter (fun (p, typ) ->
-      let pp_name f () = F.fprintf f "%s" p in
-      let pp f () = Sil.pp_type_decl pe_text pp_name Sil.pp_exp f typ in
-      let decl = pp_to_string pp () in
-      s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.ProcAttributes.formals;
+  IList.iter
+    (fun (p, typ) ->
+       let pp_name f () = F.fprintf f "%a" Mangled.pp p in
+       let pp f () = Sil.pp_type_decl pe_text pp_name Sil.pp_exp f typ in
+       let decl = pp_to_string pp () in
+       s := if !s = "" then decl else !s ^ ", " ^ decl)
+    summary.attributes.ProcAttributes.formals;
   let pp_procname f () = F.fprintf f "%a"
       Procname.pp summary.attributes.ProcAttributes.proc_name in
   let pp f () =
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 8f115a5d2..a9f68dfc5 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -169,7 +169,7 @@ val get_attributes : summary -> ProcAttributes.t
 val get_ret_type : summary -> Sil.typ
 
 (** Get the formal paramters of the procedure *)
-val get_formals : summary -> (string * Sil.typ) list
+val get_formals : summary -> (Mangled.t * Sil.typ) list
 
 (** Get the flag with the given key for the procedure, if any *)
 val get_flag : Procname.t -> string -> string option
@@ -190,7 +190,7 @@ val get_signature : summary -> string
 val get_specs : Procname.t -> Prop.normal spec list
 
 (** Return the specs and formal parameters for the proc in the spec table *)
-val get_specs_formals : Procname.t -> Prop.normal spec list * (string * Sil.typ) list
+val get_specs_formals : Procname.t -> Prop.normal spec list * (Mangled.t * Sil.typ) 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/tabulation.ml b/infer/src/backend/tabulation.ml
index 31bc00ee6..86eb4e342 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -112,7 +112,7 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S
         raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), try assert false with Assert_failure x -> x))
       end;
     let formal_parameters =
-      IList.map (fun (x, _) -> Sil.mk_pvar_callee (Mangled.from_string x) proc_name) formals in
+      IList.map (fun (x, _) -> Sil.mk_pvar_callee x proc_name) formals in
     IList.map f specs, formal_parameters
   with Not_found -> begin
       L.d_strln ("ERROR: found no entry for procedure " ^ Procname.to_string proc_name ^ ". Give up...");
@@ -774,7 +774,7 @@ let add_tainting_att_param_list prop param_nums formal_params att =
 (* Set Ataint attribute to list of parameteres in a prop *)
 let add_param_taint proc_name formal_params prop param_nums =
   let formal_params' = IList.map
-      (fun (p, _) -> Sil.mk_pvar (Mangled.from_string p) proc_name) formal_params in
+      (fun (p, _) -> Sil.mk_pvar p proc_name) formal_params in
   add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint proc_name)
 
 (* add Auntaint attribute to a callee_pname precondition *)
diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli
index 16b421373..17dec4d73 100644
--- a/infer/src/backend/tabulation.mli
+++ b/infer/src/backend/tabulation.mli
@@ -46,5 +46,5 @@ val exe_function_call:
 
 (* Set Ataint attribute to list of parameteres in a prop *)
 val add_param_taint :
-  Procname.t -> (string * Sil.typ) list -> Prop.normal Prop.t ->
+  Procname.t -> (Mangled.t * Sil.typ) list -> Prop.normal Prop.t ->
   int list -> Prop.normal Prop.t
diff --git a/infer/src/backend/type_prop.ml b/infer/src/backend/type_prop.ml
index 1733a048f..898376f99 100644
--- a/infer/src/backend/type_prop.ml
+++ b/infer/src/backend/type_prop.ml
@@ -77,8 +77,8 @@ let get_formals cfg procname =
   let pdesc = match Cfg.Procdesc.find_from_name cfg procname with
     | Some pdesc -> pdesc
     | None -> assert false in
-  let formals = Cfg.Procdesc.get_formals pdesc in
-  formals
+  Cfg.Procdesc.get_formals pdesc
+  |> IList.map (fun (p, t) -> (Mangled.to_string p, t))
 
 (* Module for defining the map to be updated: in this case it is a map     *)
 (* from procedure names to a set of types for each of the procedure's      *)
@@ -104,7 +104,7 @@ struct
     | _ -> Sil.typ_to_string typ
 
   let string_typ_to_string (s, typ) =
-    if (s = "this") then None
+    if s = "this" then None
     else Some (s^" -> "^(type_to_string typ))
 
   let rec type_signature_to_string list =
@@ -561,7 +561,7 @@ struct
           if (Procname.Set.mem callee_pname !defined_methods) then
             let formals = Cfg.Procdesc.get_formals pdesc in
             let create_typ_bundle (exp, typ) (name, typ2) =
-              (name, (get_type tenv exp id_context context field_context)) in
+              (Mangled.to_string name, (get_type tenv exp id_context context field_context)) in
             let typ_bundle = IList.map2 create_typ_bundle actual_params formals in
             let set = Type_map.find_dyn_types callee_pname map in
             if Type_map.TypeSet.mem typ_bundle set
diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml
index 0e519cb98..06dd2a008 100644
--- a/infer/src/checkers/annotations.ml
+++ b/infer/src/checkers/annotations.ml
@@ -16,10 +16,10 @@ open Utils
 (** Method signature with annotations. *)
 type annotated_signature =
   { ret : Sil.item_annotation * Sil.typ; (** Annotated return type. *)
-    params: (string * Sil.item_annotation * Sil.typ) list } (** Annotated parameters. *)
+    params: (Mangled.t * Sil.item_annotation * Sil.typ) list } (** Annotated parameters. *)
 
 let param_equal (s1, ia1, t1) (s2, ia2, t2) =
-  string_equal s1 s2 &&
+  Mangled.equal s1 s2 &&
   Sil.item_annotation_compare ia1 ia2 = 0 &&
   Sil.typ_equal t1 t2
 
@@ -192,10 +192,11 @@ let annotated_signature_is_anonymous_inner_class_wrapper ann_sig proc_name =
     Sil.item_annotation_is_empty ia && PatternMatch.type_is_object t in
   let x_param_found = ref false in
   let name_is_x_number name =
-    let len = String.length name in
+    let name_str = Mangled.to_string name in
+    let len = String.length name_str in
     len >= 2 &&
-    String.sub name 0 1 = "x" &&
-    let s = String.sub name 1 (len - 1) in
+    String.sub name_str 0 1 = "x" &&
+    let s = String.sub name_str 1 (len - 1) in
     let is_int =
       try
         ignore (int_of_string s);
@@ -204,7 +205,7 @@ let annotated_signature_is_anonymous_inner_class_wrapper ann_sig proc_name =
       with Failure _ -> false in
     is_int in
   let check_param (name, ia, t) =
-    if name = "this" then true
+    if Mangled.to_string name = "this" then true
     else
       name_is_x_number name &&
       Sil.item_annotation_is_empty ia &&
@@ -216,16 +217,16 @@ let annotated_signature_is_anonymous_inner_class_wrapper ann_sig proc_name =
 
 (** Check if the given parameter has a Nullable annotation in the given signature *)
 let param_is_nullable pvar ann_sig =
-  let pvar_str = Mangled.to_string (Sil.pvar_get_name pvar) in
   IList.exists
-    (fun (param_str, annot, _) -> param_str = pvar_str && ia_is_nullable annot)
+    (fun (param, annot, _) ->
+       Mangled.equal param (Sil.pvar_get_name pvar) && ia_is_nullable annot)
     ann_sig.params
 
 (** Pretty print a method signature with annotations. *)
 let pp_annotated_signature proc_name fmt annotated_signature =
   let pp_ia fmt ia = if ia <> [] then F.fprintf fmt "%a " Sil.pp_item_annotation ia in
-  let pp_annotated_param fmt (s, ia, t) =
-    F.fprintf fmt " %a%a %s" pp_ia ia (Sil.pp_typ_full pe_text) t s in
+  let pp_annotated_param fmt (p, ia, t) =
+    F.fprintf fmt " %a%a %a" pp_ia ia (Sil.pp_typ_full pe_text) t Mangled.pp p in
   let ia, ret_type = annotated_signature.ret in
   F.fprintf fmt "%a%a %s (%a )"
     pp_ia ia
@@ -264,8 +265,8 @@ let annotated_signature_mark proc_name ann asig (b, bs) =
       L.stdout "  ANNOTATED SIGNATURE: %a@." (pp_annotated_signature proc_name) asig;
       assert false in
     let rec combine l1 l2 = match l1, l2 with
-      | ("this", ia, t):: l1', l2' ->
-          ("this", ia, t) :: combine l1' l2'
+      | (p, ia, t):: l1', l2' when Mangled.to_string p = "this" ->
+          (p, ia, t) :: combine l1' l2'
       | (s, ia, t):: l1', x:: l2' ->
           mark_param (s, ia, t) x :: combine l1' l2'
       | [], _:: _ -> fail ()
diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli
index a972bd5e4..aba7c6693 100644
--- a/infer/src/checkers/annotations.mli
+++ b/infer/src/checkers/annotations.mli
@@ -21,7 +21,7 @@ type annotation =
 (** Method signature with annotations. *)
 type annotated_signature =
   { ret : Sil.item_annotation * Sil.typ; (** Annotated return type. *)
-    params: (string * Sil.item_annotation * Sil.typ) list } (** Annotated parameters. *)
+    params: (Mangled.t * Sil.item_annotation * Sil.typ) list } (** Annotated parameters. *)
 
 (** 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
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 011d60005..0ed3eace3 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -278,12 +278,13 @@ let callback_monitor_nullcheck all_procs get_proc_desc idenv tenv proc_name proc
     let formals = Cfg.Procdesc.get_formals proc_desc in
     let class_formals =
       let is_class_type = function
-        | "this", Sil.Tptr _ -> false (* no need to null check 'this' *)
+        | p, Sil.Tptr _ when Mangled.to_string p = "this" ->
+            false (* no need to null check 'this' *)
         | _, Sil.Tstruct _ -> true
         | _, Sil.Tptr (Sil.Tstruct _, _) -> true
         | _ -> false in
       IList.filter is_class_type formals in
-    IList.map (fun (s, _) -> Mangled.from_string s) class_formals) in
+    IList.map fst class_formals) in
   let equal_formal_param exp formal_name = match exp with
     | Sil.Lvar pvar ->
         let name = Sil.pvar_get_name pvar in
diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml
index d130193a2..f0c67aa26 100644
--- a/infer/src/checkers/eradicate.ml
+++ b/infer/src/checkers/eradicate.ml
@@ -76,7 +76,7 @@ struct
       find_canonical_duplicate calls_this checks get_proc_desc idenv tenv curr_pname
       curr_pdesc annotated_signature linereader proc_loc
     : bool * Extension.extension TypeState.t option =
-    let mk_pvar s = Sil.mk_pvar (Mangled.from_string s) curr_pname in
+    let mk_pvar s = Sil.mk_pvar s curr_pname in
     let add_formal typestate (s, ia, typ) =
       let pvar = mk_pvar s in
       let ta =
diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml
index 5b8c08061..60f59dc8d 100644
--- a/infer/src/checkers/eradicateChecks.ml
+++ b/infer/src/checkers/eradicateChecks.ml
@@ -68,7 +68,7 @@ let classify_procedure proc_attributes =
 
 
 let is_virtual = function
-  | ("this", _, _):: _ -> true
+  | (p, _, _):: _ when Mangled.to_string p = "this" -> true
   | _ -> false
 
 
@@ -431,7 +431,7 @@ let check_call_parameters
   let tot_param_num = IList.length sig_params - (if has_this then 1 else 0) in
   let rec check sparams cparams = match sparams, cparams with
     | (s1, ia1, t1) :: sparams', ((orig_e2, e2), t2) :: cparams' ->
-        let param_is_this = s1 = "this" in
+        let param_is_this = Mangled.to_string s1 = "this" in
         let formal_is_nullable = Annotations.ia_is_nullable ia1 in
         let formal_is_present = Annotations.ia_is_present ia1 in
         let (_, ta2, _) =
@@ -457,7 +457,7 @@ let check_call_parameters
             let description =
               match explain_expr node orig_e2 with
               | Some descr -> descr
-              | None -> "formal parameter " ^ s1 in
+              | None -> "formal parameter " ^ (Mangled.to_string s1) in
             let origin_descr = TypeAnnotation.descr_origin ta2 in
 
             let param_num = IList.length sparams' + (if has_this then 0 else 1) in
@@ -523,7 +523,7 @@ let check_overridden_annotations
             find_canonical_duplicate
             start_node
             (TypeErr.Inconsistent_subclass_parameter_annotation
-               (current_name, pos, proc_name, overriden_proc_name))
+               (Mangled.to_string current_name, pos, proc_name, overriden_proc_name))
             None
             loc proc_name in
       (pos + 1) in
diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml
index 8c4ca2aa7..cde066772 100644
--- a/infer/src/checkers/typeCheck.ml
+++ b/infer/src/checkers/typeCheck.ml
@@ -263,7 +263,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
           begin
             match pvar_get_origin pvar with
             | Some (TypeOrigin.Formal s) ->
-                let pvar' = Sil.mk_pvar (Mangled.from_string s) curr_pname in
+                let pvar' = Sil.mk_pvar s curr_pname in
                 Some (Sil.Lvar pvar')
             | _ -> None
           end
@@ -350,8 +350,8 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
         let exp' = Idenv.expand_expr_temps idenv node _exp in
 
         let is_parameter_field pvar = (* parameter.field *)
-          let name = Sil.pvar_to_string pvar in
-          let filter (s, ia, typ) = string_equal s name in
+          let name = Sil.pvar_get_name pvar in
+          let filter (s, ia, typ) = Mangled.equal s name in
           IList.exists filter annotated_signature.Annotations.params in
 
         let is_static_field pvar = (* static field *)
@@ -404,8 +404,9 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
 
             (* Drop reference parameters to this and outer objects. *)
             let is_hidden_parameter (n, t) =
-              string_equal n "this" ||
-              Str.string_match (Str.regexp "$bcvar[0-9]+") n 0 in
+              let n_str = Mangled.to_string n in
+              n_str = "this" ||
+              Str.string_match (Str.regexp "$bcvar[0-9]+") n_str 0 in
             let rec drop_n_args ntl = match ntl with
               | fp:: tail when is_hidden_parameter fp -> 1 + drop_n_args tail
               | _ -> 0 in
diff --git a/infer/src/checkers/typeErr.ml b/infer/src/checkers/typeErr.ml
index 1c34d7a6b..531871fd4 100644
--- a/infer/src/checkers/typeErr.ml
+++ b/infer/src/checkers/typeErr.ml
@@ -254,11 +254,12 @@ module Strict = struct
 
   let this_type_get_strict signature =
     match signature.Annotations.params with
-    | ("this", _, this_type):: _ -> begin
-        match PatternMatch.type_get_annotation this_type with
-        | Some ia -> Annotations.ia_get_strict ia
-        | None -> None
-      end
+    | (p, _, this_type):: _ when Mangled.to_string p = "this" ->
+        begin
+          match PatternMatch.type_get_annotation this_type with
+          | Some ia -> Annotations.ia_get_strict ia
+          | None -> None
+        end
     | _ -> None
 
   let signature_get_strict signature =
diff --git a/infer/src/checkers/typeOrigin.ml b/infer/src/checkers/typeOrigin.ml
index b3bab199e..cc6814e1c 100644
--- a/infer/src/checkers/typeOrigin.ml
+++ b/infer/src/checkers/typeOrigin.ml
@@ -26,7 +26,7 @@ type proc_origin =
 type t =
   | Const of Location.t
   | Field of Ident.fieldname * Location.t
-  | Formal of string
+  | Formal of Mangled.t
   | Proc of proc_origin
   | New
   | ONone
@@ -49,7 +49,7 @@ let equal o1 o2 = match o1, o2 with
   | Field _, _
   | _, Field _ -> false
   | Formal s1, Formal s2 ->
-      string_equal s1 s2
+      Mangled.equal s1 s2
   | Formal _, _
   | _, Formal _ -> false
   | Proc po1 , Proc po2 ->
@@ -67,7 +67,7 @@ let equal o1 o2 = match o1, o2 with
 let to_string = function
   | Const loc -> "Const"
   | Field (fn, loc) -> "Field " ^ Ident.fieldname_to_simplified_string fn
-  | Formal s -> "Formal " ^ s
+  | Formal s -> "Formal " ^ Mangled.to_string s
   | Proc po ->
       Printf.sprintf
         "Fun %s"
@@ -85,7 +85,7 @@ let get_description origin =
   | Field (fn, loc) ->
       Some ("field " ^ Ident.fieldname_to_simplified_string fn ^ atline loc, Some loc, None)
   | Formal s ->
-      Some ("method parameter " ^ s, None, None)
+      Some ("method parameter " ^ Mangled.to_string s, None, None)
   | Proc po ->
       let strict = match TypeErr.Strict.signature_get_strict po.annotated_signature with
         | Some ann ->
diff --git a/infer/src/checkers/typeOrigin.mli b/infer/src/checkers/typeOrigin.mli
index 8052f3de5..2f5186598 100644
--- a/infer/src/checkers/typeOrigin.mli
+++ b/infer/src/checkers/typeOrigin.mli
@@ -19,7 +19,7 @@ type proc_origin =
 type t =
   | Const of Location.t (** A constant in the source *)
   | Field of Ident.fieldname * Location.t (** A field access *)
-  | Formal of string (** A formal parameter *)
+  | Formal of Mangled.t (** A formal parameter *)
   | Proc of proc_origin (** A procedure call *)
   | New (** A new object creation *)
   | ONone (** No origin is known *)
diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml
index 3579de410..dc4675f99 100644
--- a/infer/src/clang/cMethod_trans.ml
+++ b/infer/src/clang/cMethod_trans.ml
@@ -270,7 +270,7 @@ let get_formal_parameters tenv ms =
             (Ast_expressions.create_pointer_type raw_type)
           else raw_type in
         let typ = CTypes_decl.type_ptr_to_sil_type tenv tp in
-        (name, typ):: defined_parameters pl' in
+        (Mangled.from_string name, typ):: defined_parameters pl' in
   defined_parameters (CMethod_signature.ms_get_args ms)
 
 let get_return_type tenv ms =
@@ -325,11 +325,10 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
                            && CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in
   let create_new_procdesc () =
     let formals = get_formal_parameters tenv ms in
-    let captured_str = IList.map (
-        fun (var, t) -> (Mangled.to_string (Sil.pvar_get_name var), t)
-      ) captured in
+    let captured_str =
+      IList.map (fun (var, t) -> (Mangled.from_string (Sil.pvar_to_string var), t)) captured in
     (* Captured variables for blocks are treated as parameters *)
-    let formals = captured_str @formals in
+    let formals = captured_str @ formals in
     let source_range = CMethod_signature.ms_get_loc ms in
     Printing.log_out "\nCreating a new procdesc for function: '%s'\n@." pname;
     let loc_start = CLocation.get_sil_location_from_range source_range true in
@@ -375,7 +374,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
       let ret_type, formals =
         (match type_opt with
          | Some (ret_type, arg_types) ->
-             ret_type, IList.map (fun typ -> ("x", typ)) arg_types
+             ret_type, IList.map (fun typ -> (Mangled.from_string "x", typ)) arg_types
          | None -> Sil.Tvoid, []) in
       let loc = Location.dummy in
       let _ =
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index a2ae7b043..7c7417866 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -275,7 +275,9 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv =
     let ret_type = lookup_typ (Procname.java_get_return_type proc_name) in
     let formals =
       let param_strs = Procname.java_get_parameters_as_strings proc_name in
-      IList.fold_right (fun typ_str params -> ("", lookup_typ typ_str) :: params) param_strs [] in
+      IList.fold_right
+        (fun typ_str params -> (Mangled.from_string "", lookup_typ typ_str) :: params)
+        param_strs [] in
     let proc_attributes =
       { (ProcAttributes.default proc_name Config.Java) with
         ProcAttributes.formals;
diff --git a/infer/src/java/jConfig.ml b/infer/src/java/jConfig.ml
index 9f3d4cc42..4d4c55fb3 100644
--- a/infer/src/java/jConfig.ml
+++ b/infer/src/java/jConfig.ml
@@ -63,13 +63,13 @@ let run_method = "run"
 
 (** {2 Names of special variables, constants and method names} *)
 
-let this = "this"
+let this = Mangled.from_string "this"
 
 let constructor_name = "<init>"
 
 let clone_name = "clone"
 
-let field_st = "field"
+let field_st = Mangled.from_string "field"
 
 let field_cst = "<field>"
 
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index e1663ae47..c348325e6 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -127,7 +127,7 @@ let formals_from_signature program tenv cn ms kind =
   let get_arg_name () =
     let arg = method_name^"_arg_"^(string_of_int !counter) in
     incr counter;
-    arg in
+    Mangled.from_string arg in
   let collect l vt =
     let arg_name = get_arg_name () in
     let arg_type = JTransType.value_type program tenv vt in
@@ -139,7 +139,7 @@ let formals_from_signature program tenv cn ms kind =
 
 let formals program tenv cn impl =
   let collect l (vt, var) =
-    let name = JBir.var_name_g var in
+    let name = Mangled.from_string (JBir.var_name_g var) in
     let typ = JTransType.param_type program tenv cn var vt in
     (name, typ):: l in
   IList.rev (IList.fold_left collect [] (JBir.params impl))
@@ -153,9 +153,8 @@ let locals_formals program tenv cn impl meth_kind =
       let string_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in
       [(JConfig.field_st, string_type) ]
     else formals program tenv cn impl in
-  let is_formal v =
-    let v = Mangled.to_string v in
-    IList.exists (fun (v', _) -> Utils.string_equal v v') form_list in
+  let is_formal p =
+    IList.exists (fun (p', _) -> Mangled.equal p p') form_list in
   let collect l var =
     let vname = Mangled.from_string (JBir.var_name_g var) in
     let names = (fst (IList.split l)) in
@@ -440,7 +439,7 @@ let rec expression context pc expr =
       begin
         match c with (* We use the constant <field> internally to mean a variable. *)
         | `String s when (JBasics.jstr_pp s) = JConfig.field_cst ->
-            let varname = Mangled.from_string JConfig.field_st in
+            let varname = JConfig.field_st in
             let string_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in
             let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
             let pvar = Sil.mk_pvar varname procname in
@@ -781,7 +780,12 @@ let instruction_thread_start context cn ms obj args var_opt =
 
 let is_this expr =
   match expr with
-  | JBir.Var (_, var) -> JBir.var_name_debug var = Some JConfig.this
+  | JBir.Var (_, var) ->
+      begin
+        match JBir.var_name_debug var with
+        | None -> false
+        | Some name_opt -> Mangled.to_string JConfig.this = name_opt
+      end
   | _ -> false
 
 
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index 6b97591e5..30a92e006 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -396,7 +396,7 @@ let sizeof_of_object_type program tenv ot subtypes =
 
 (** return the name and type of a formal parameter, looking up the class name in case of "this" *)
 let param_type program tenv cn name vt =
-  if (JBir.var_name_g name) = JConfig.this
+  if (JBir.var_name_g name) = Mangled.to_string JConfig.this
   then get_class_type program tenv cn
   else value_type program tenv vt
 
diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml
index 78365dcb6..e8f632907 100644
--- a/infer/src/llvm/lTrans.ml
+++ b/infer/src/llvm/lTrans.ml
@@ -128,7 +128,8 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
       let (proc_attrs : ProcAttributes.t) =
         let open Sil in
         { (ProcAttributes.default proc_name Config.C_CPP) with
-          ProcAttributes.formals = IList.map (fun (tp, name) -> (name, trans_typ tp)) params;
+          ProcAttributes.formals =
+            IList.map (fun (tp, name) -> (Mangled.from_string name, trans_typ tp)) params;
           is_defined = true; (** is defined and not just declared *)
           loc = source_only_location ();
           locals = []; (* TODO *)