diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index b048fac34..f36c4590f 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -50,9 +50,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem
         else Dom.Mem.add_heap loc arr mem
       in
-      let loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in
       match typ.Typ.desc with
       | Typ.Tarray (typ, length, stride) ->
+          let loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in
           declare_array pname node location loc typ ~length
             ?stride:(Option.map ~f:IntLit.to_int stride)
             ~inst_num ~dimension:(dimension + 1) mem
@@ -147,7 +147,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc) |> fst
 
 
-  let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias loc =
+  let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias location =
     match ret with
     | Some (id, _) ->
         let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
@@ -155,7 +155,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let ret_var = Loc.of_var (Var.of_id id) in
         let add_ret_alias l = Dom.Mem.load_alias id l mem in
         let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in
-        Dom.Val.subst ret_val subst_map loc |> Dom.Val.add_trace_elem (Trace.Return loc)
+        Dom.Val.subst ret_val subst_map location |> Dom.Val.add_trace_elem (Trace.Return location)
         |> Fn.flip (Dom.Mem.add_stack ret_var) mem
     | None ->
         mem
@@ -163,7 +163,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem =
     let formals = Sem.get_formals pdesc in
-    let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem location) params in
+    let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in
     let f mem formal actual =
       match (snd formal).Typ.desc with
       | Typ.Tptr (typ, _) -> (
@@ -203,17 +203,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let instantiate_mem
       : Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t option -> Typ.Procname.t
         -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate =
-    fun tenv ret callee_pdesc callee_pname params caller_mem summary loc ->
+    fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
       let callee_entry_mem = Dom.Summary.get_input summary in
       let callee_exit_mem = Dom.Summary.get_output summary in
       let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
       match callee_pdesc with
       | Some pdesc ->
           let subst_map, ret_alias =
-            Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc
+            Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias
           in
-          instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias loc
-          |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc
+          instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias location
+          |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map
+               location
       | None ->
           caller_mem
 
@@ -234,8 +235,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       let pname = Procdesc.get_proc_name pdesc in
       let output_mem =
         match instr with
-        | Load (id, exp, _, loc) ->
-            let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in
+        | Load (id, exp, _, _) ->
+            let locs = Sem.eval exp mem |> Dom.Val.get_all_locs in
             let v = Dom.Mem.find_heap_set locs mem in
             if Ident.is_none id then mem
             else
@@ -243,9 +244,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               if PowLoc.is_singleton locs then
                 Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem
               else mem
-        | Store (exp1, _, exp2, loc) ->
-            let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in
-            let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in
+        | Store (exp1, _, exp2, location) ->
+            let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in
+            let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in
             let mem = Dom.Mem.update_mem locs v mem in
             if PowLoc.is_singleton locs then
               let loc_v = PowLoc.min_elt locs in
@@ -260,23 +261,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               | _ ->
                   Dom.Mem.store_simple_alias loc_v exp2 mem
             else mem
-        | Prune (exp, loc, _, _) ->
-            Sem.prune exp loc mem
-        | Call (ret, Const Cfun callee_pname, params, loc, _)
+        | Prune (exp, _, _, _) ->
+            Sem.prune exp mem
+        | Call (ret, Const Cfun callee_pname, params, location, _)
           -> (
             let quals = Typ.Procname.get_qualifiers callee_pname in
             match QualifiedCppName.Dispatch.dispatch_qualifiers Models.dispatcher quals with
             | Some model ->
-                model callee_pname ret params node loc mem
+                model callee_pname ret params node location mem
             | None ->
               match Summary.read_summary pdesc callee_pname with
               | Some summary ->
                   let callee = extras callee_pname in
-                  instantiate_mem tenv ret callee callee_pname params mem summary loc
+                  instantiate_mem tenv ret callee callee_pname params mem summary location
               | None ->
                   L.(debug BufferOverrun Verbose)
-                    "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp loc ;
-                  Models.model_by_value Dom.Val.unknown callee_pname ret params node loc mem
+                    "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
+                    location ;
+                  Models.model_by_value Dom.Val.unknown callee_pname ret params node location mem
                   |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown )
         | Declare_locals (locals, location) ->
             (* array allocation in stack e.g., int arr[10] *)
@@ -295,10 +297,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             in
             let mem, inst_num = List.fold ~f:(try_decl_arr location) ~init:(mem, 1) locals in
             declare_symbolic_parameter pdesc tenv node location inst_num mem
-        | Call (_, fun_exp, _, loc, _) ->
+        | Call (_, fun_exp, _, location, _) ->
             let () =
               L.(debug BufferOverrun Verbose)
-                "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp loc
+                "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location
             in
             mem
         | Remove_temps (temps, _) ->
@@ -321,28 +323,28 @@ module Report = struct
   let add_condition
       : Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
         -> PO.ConditionSet.t =
-    fun pname node exp loc mem cond_set ->
+    fun pname node exp location mem cond_set ->
       let array_access =
         match exp with
         | Exp.Var _ ->
-            let v = Sem.eval exp mem loc in
+            let v = Sem.eval exp mem in
             let arr = Dom.Val.get_array_blk v in
             let arr_traces = Dom.Val.get_traces v in
             Some (arr, arr_traces, Itv.zero, TraceSet.empty, true)
         | Exp.Lindex (e1, e2) ->
-            let locs = Sem.eval_locs e1 mem loc |> Dom.Val.get_all_locs in
+            let locs = Sem.eval_locs e1 mem |> Dom.Val.get_all_locs in
             let v_arr = Dom.Mem.find_set locs mem in
             let arr = Dom.Val.get_array_blk v_arr in
             let arr_traces = Dom.Val.get_traces v_arr in
-            let v_idx = Sem.eval e2 mem loc in
+            let v_idx = Sem.eval e2 mem in
             let idx = Dom.Val.get_itv v_idx in
             let idx_traces = Dom.Val.get_traces v_idx in
             Some (arr, arr_traces, idx, idx_traces, true)
         | Exp.BinOp ((Binop.PlusA as bop), e1, e2) | Exp.BinOp ((Binop.MinusA as bop), e1, e2) ->
-            let v_arr = Sem.eval e1 mem loc in
+            let v_arr = Sem.eval e1 mem in
             let arr = Dom.Val.get_array_blk v_arr in
             let arr_traces = Dom.Val.get_traces v_arr in
-            let v_idx = Sem.eval e2 mem loc in
+            let v_idx = Sem.eval e2 mem in
             let idx = Dom.Val.get_itv v_idx in
             let idx_traces = Dom.Val.get_traces v_idx in
             let is_plus = Binop.equal bop Binop.PlusA in
@@ -363,8 +365,8 @@ module Report = struct
           L.(debug BufferOverrun Verbose) "@]@." ;
           match (size, idx) with
           | NonBottom size, NonBottom idx ->
-              let traces = TraceSet.merge ~traces_arr ~traces_idx loc in
-              PO.ConditionSet.add_bo_safety pname loc site ~size ~idx traces cond_set
+              let traces = TraceSet.merge ~traces_arr ~traces_idx location in
+              PO.ConditionSet.add_bo_safety pname location site ~size ~idx traces cond_set
           | _ ->
               cond_set )
       | None ->
@@ -374,17 +376,16 @@ module Report = struct
   let instantiate_cond
       : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate
         -> Summary.payload -> Location.t -> PO.ConditionSet.t =
-    fun tenv caller_pname callee_pdesc params caller_mem summary loc ->
+    fun tenv caller_pname callee_pdesc params caller_mem summary location ->
       let callee_entry_mem = Dom.Summary.get_input summary in
       let callee_cond = Dom.Summary.get_cond_set summary in
       match callee_pdesc with
       | Some pdesc ->
           let subst_map, _ =
             Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None
-              loc
           in
           let pname = Procdesc.get_proc_name pdesc in
-          PO.ConditionSet.subst callee_cond subst_map caller_pname pname loc
+          PO.ConditionSet.subst callee_cond subst_map caller_pname pname location
       | _ ->
           callee_cond
 
@@ -452,13 +453,13 @@ module Report = struct
           let pname = Procdesc.get_proc_name pdesc in
           let cond_set =
             match instr with
-            | Sil.Load (_, exp, _, loc) | Sil.Store (exp, _, _, loc) ->
-                add_condition pname node exp loc mem cond_set
-            | Sil.Call (_, Const Cfun callee_pname, params, loc, _) -> (
+            | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
+                add_condition pname node exp location mem cond_set
+            | Sil.Call (_, Const Cfun callee_pname, params, location, _) -> (
               match Summary.read_summary pdesc callee_pname with
               | Some summary ->
                   let callee = extras callee_pname in
-                  instantiate_cond tenv pname callee params mem summary loc
+                  instantiate_cond tenv pname callee params mem summary location
                   |> PO.ConditionSet.join cond_set
               | _ ->
                   cond_set )
@@ -472,13 +473,15 @@ module Report = struct
               match instr with
               | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) ->
                   ()
-              | Sil.Prune (cond, loc, true_branch, _) ->
+              | Sil.Prune (cond, location, true_branch, _) ->
                   let i = match cond with Exp.Const Const.Cint i -> i | _ -> IntLit.zero in
-                  let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
+                  let desc =
+                    Errdesc.explain_condition_always_true_false tenv i cond node location
+                  in
                   let exn =
                     Exceptions.Condition_always_true_false (desc, not true_branch, __POS__)
                   in
-                  Reporting.log_warning_deprecated pname ~loc exn
+                  Reporting.log_warning_deprecated pname ~loc:location exn
               (* special case for when we're at the end of a procedure *)
               | Sil.Call (_, Const Cfun pname, _, _, _)
                 when String.equal (Typ.Procname.get_method pname) "exit"
@@ -490,10 +493,10 @@ module Report = struct
                      && ExitStatement.has_multiple_sibling_nodes_and_one_successor node ->
                   ()
               | _ ->
-                  let loc = Sil.instr_get_loc instr in
-                  let desc = Errdesc.explain_unreachable_code_after loc in
+                  let location = Sil.instr_get_loc instr in
+                  let desc = Errdesc.explain_unreachable_code_after location in
                   let exn = Exceptions.Unreachable_code_after (desc, __POS__) in
-                  Reporting.log_error_deprecated pname ~loc exn )
+                  Reporting.log_error_deprecated pname ~loc:location exn )
             | _ ->
                 ()
           in
@@ -523,18 +526,18 @@ module Report = struct
     fun trace desc ->
       let f elem (trace, depth) =
         match elem with
-        | Trace.Assign loc ->
-            (Errlog.make_trace_element depth loc "Assignment" [] :: trace, depth)
-        | Trace.ArrDecl loc ->
-            (Errlog.make_trace_element depth loc "ArrayDeclaration" [] :: trace, depth)
-        | Trace.Call loc ->
-            (Errlog.make_trace_element depth loc "Call" [] :: trace, depth + 1)
-        | Trace.Return loc ->
-            (Errlog.make_trace_element (depth - 1) loc "Return" [] :: trace, depth - 1)
+        | Trace.Assign location ->
+            (Errlog.make_trace_element depth location "Assignment" [] :: trace, depth)
+        | Trace.ArrDecl location ->
+            (Errlog.make_trace_element depth location "ArrayDeclaration" [] :: trace, depth)
+        | Trace.Call location ->
+            (Errlog.make_trace_element depth location "Call" [] :: trace, depth + 1)
+        | Trace.Return location ->
+            (Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1)
         | Trace.SymAssign _ ->
             (trace, depth)
-        | Trace.ArrAccess loc ->
-            (Errlog.make_trace_element depth loc ("ArrayAccess: " ^ desc) [] :: trace, depth)
+        | Trace.ArrAccess location ->
+            (Errlog.make_trace_element depth location ("ArrayAccess: " ^ desc) [] :: trace, depth)
       in
       List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
 
@@ -548,10 +551,10 @@ module Report = struct
         | None ->
             ()
         | Some issue_type ->
-            let caller_pname, loc =
+            let caller_pname, location =
               match PO.ConditionTrace.get_cond_trace trace with
-              | PO.ConditionTrace.Inter (caller_pname, _, loc) ->
-                  (caller_pname, loc)
+              | PO.ConditionTrace.Inter (caller_pname, _, location) ->
+                  (caller_pname, location)
               | PO.ConditionTrace.Intra pname ->
                   (pname, PO.ConditionTrace.get_location trace)
             in
@@ -564,9 +567,9 @@ module Report = struct
                 | trace ->
                     make_err_trace trace description
                 | exception _ ->
-                    [Errlog.make_trace_element 0 loc description []]
+                    [Errlog.make_trace_element 0 location description []]
               in
-              Reporting.log_error_deprecated pname ~loc ~ltr:trace exn
+              Reporting.log_error_deprecated pname ~loc:location ~ltr:trace exn
       in
       PO.ConditionSet.iter conds ~f:report1
 
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 017f45ef0..81dacf2f9 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -213,7 +213,7 @@ module Val = struct
   let subst
       : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Location.t
         -> t =
-    fun x (bound_map, trace_map) loc ->
+    fun x (bound_map, trace_map) location ->
       let symbols = get_symbols x in
       let traces_caller =
         List.fold symbols
@@ -221,7 +221,7 @@ module Val = struct
             try TraceSet.join (Itv.SubstMap.find symbol trace_map) traces with Not_found -> traces)
           ~init:TraceSet.empty
       in
-      let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces loc in
+      let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in
       {x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces}
       |> normalize
 
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 9674db57b..6afd40442 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -22,10 +22,10 @@ module Make (CFG : ProcCfg.S) = struct
     Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node -> Location.t
     -> Dom.Mem.astate -> Dom.Mem.astate
 
-  let set_uninitialized node (typ: Typ.t) loc mem =
+  let set_uninitialized node (typ: Typ.t) ploc mem =
     match typ.desc with
     | Tint _ | Tfloat _ ->
-        Dom.Mem.weak_update_heap loc Dom.Val.Itv.top mem
+        Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem
     | _ ->
         L.(debug BufferOverrun Verbose)
           "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp
@@ -48,7 +48,7 @@ module Make (CFG : ProcCfg.S) = struct
     match ret with
     | Some (id, _) ->
         let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in
-        let length = Sem.eval length0 mem (CFG.loc node) in
+        let length = Sem.eval length0 mem in
         let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
         let v =
           Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1
@@ -66,22 +66,22 @@ module Make (CFG : ProcCfg.S) = struct
     model_malloc pname ret (List.tl_exn params) node location mem
 
 
-  let model_min _pname ret params _node location mem =
+  let model_min _pname ret params _node _location mem =
     match (ret, params) with
     | Some (id, _), [(e1, _); (e2, _)] ->
-        let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in
-        let i2 = Sem.eval e2 mem location |> Dom.Val.get_itv in
+        let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in
+        let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in
         let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in
         mem |> Dom.Mem.add_stack (Loc.of_id id) v
     | _ ->
         mem
 
 
-  let model_set_size _pname _ret params _node location mem =
+  let model_set_size _pname _ret params _node _location mem =
     match params with
     | [(e1, _); (e2, _)] ->
-        let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in
-        let size = Sem.eval e2 mem location |> Dom.Val.get_itv in
+        let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in
+        let size = Sem.eval e2 mem |> Dom.Val.get_itv in
         let arr = Dom.Mem.find_heap_set locs mem in
         let arr = Dom.Val.set_array_size size arr in
         Dom.Mem.strong_update_heap locs arr mem
@@ -105,17 +105,16 @@ module Make (CFG : ProcCfg.S) = struct
     match params with
     | (e, _) :: _ ->
         L.(debug BufferOverrun Medium)
-          "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp
-          (Sem.eval e mem location) ;
+          "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ;
         mem
     | _ ->
         mem
 
 
-  let model_infer_set_array_length pname _ret params node location mem =
+  let model_infer_set_array_length pname _ret params node _location mem =
     match params with
     | [(Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)}); (length_exp, _)] ->
-        let length = Sem.eval length_exp mem location |> Dom.Val.get_itv in
+        let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
         let stride = Option.map ~f:IntLit.to_int stride0 in
         let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
         mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 2a65810d1..5c8d3b146 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -167,23 +167,23 @@ module ConditionTrace = struct
 
   type t =
     { proc_name: Typ.Procname.t
-    ; loc: Location.t
+    ; location: Location.t
     ; id: string
     ; cond_trace: cond_trace
     ; val_traces: ValTraceSet.t }
     [@@deriving compare]
 
-  let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.loc
+  let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.location
 
   let pp : F.formatter -> t -> unit =
     fun fmt ct ->
       if Config.bo_debug <= 1 then F.fprintf fmt "at %a" pp_location ct
       else
         match ct.cond_trace with
-        | Inter (_, pname, loc) ->
+        | Inter (_, pname, location) ->
             let pname = Typ.Procname.to_string pname in
             F.fprintf fmt "at %a by call %s() at %a (%a)" pp_location ct pname Location.pp_file_pos
-              loc ValTraceSet.pp ct.val_traces
+              location ValTraceSet.pp ct.val_traces
         | Intra _ ->
             F.fprintf fmt "%a (%a)" pp_location ct ValTraceSet.pp ct.val_traces
 
@@ -192,14 +192,14 @@ module ConditionTrace = struct
     fun fmt ct ->
       match ct.cond_trace with
       | Inter (_, pname, _)
-        when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.loc.Location.file) ->
+        when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.location.Location.file) ->
           F.fprintf fmt " %@ %a by call %a " pp_location ct MF.pp_monospaced
             (Typ.Procname.to_string pname ^ "()")
       | _ ->
           ()
 
 
-  let get_location : t -> Location.t = fun ct -> ct.loc
+  let get_location : t -> Location.t = fun ct -> ct.location
 
   let get_cond_trace : t -> cond_trace = fun ct -> ct.cond_trace
 
@@ -210,12 +210,15 @@ module ConditionTrace = struct
 
 
   let make : Typ.Procname.t -> Location.t -> string -> ValTraceSet.t -> t =
-    fun proc_name loc id val_traces -> {proc_name; loc; id; cond_trace= Intra proc_name; val_traces}
+    fun proc_name location id val_traces ->
+      {proc_name; location; id; cond_trace= Intra proc_name; val_traces}
 
 
-  let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc ct =
-    let val_traces = ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces loc in
-    {ct with cond_trace= Inter (caller_pname, callee_pname, loc); val_traces}
+  let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location ct =
+    let val_traces =
+      ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces location
+    in
+    {ct with cond_trace= Inter (caller_pname, callee_pname, location); val_traces}
 
 end
 
@@ -270,17 +273,17 @@ module ConditionSet = struct
 
   let join condset1 condset2 = List.fold_left ~f:add_one condset1 ~init:condset2
 
-  let add_bo_safety pname loc id ~idx ~size val_traces condset =
+  let add_bo_safety pname location id ~idx ~size val_traces condset =
     match Condition.make ~idx ~size with
     | None ->
         condset
     | Some cond ->
-        let trace = ConditionTrace.make pname loc id val_traces in
+        let trace = ConditionTrace.make pname location id val_traces in
         let cwt = {cond; trace} in
         join [cwt] condset
 
 
-  let subst condset (bound_map, trace_map) caller_pname callee_pname loc =
+  let subst condset (bound_map, trace_map) caller_pname callee_pname location =
     let subst_add_cwt condset cwt =
       match Condition.get_symbols cwt.cond with
       | [] ->
@@ -299,8 +302,8 @@ module ConditionSet = struct
                       val_traces )
             in
             let make_call_and_subst trace =
-              ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc
-                trace
+              ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname
+                location trace
             in
             let trace = make_call_and_subst cwt.trace in
             add_one condset {cond; trace}
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 580677c17..9492a9b75 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -186,8 +186,8 @@ module Make (CFG : ProcCfg.S) = struct
           false
 
 
-  let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t =
-    fun exp mem loc ->
+  let rec eval : Exp.t -> Mem.astate -> Val.t =
+    fun exp mem ->
       if must_alias_cmp exp mem then Val.of_int 0
       else
         match exp with
@@ -198,20 +198,19 @@ module Make (CFG : ProcCfg.S) = struct
             let arr = Mem.find_stack_set ploc mem in
             ploc |> Val.of_pow_loc |> Val.join arr
         | Exp.UnOp (uop, e, _) ->
-            eval_unop uop e mem loc
+            eval_unop uop e mem
         | Exp.BinOp (bop, e1, e2) ->
-            eval_binop bop e1 e2 mem loc
+            eval_binop bop e1 e2 mem
         | Exp.Const c ->
             eval_const c
         | Exp.Cast (_, e) ->
-            eval e mem loc
+            eval e mem
         | Exp.Lfield (e, fn, _) ->
-            eval e mem loc |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn
-            |> Val.of_pow_loc
+            eval e mem |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
         | Exp.Lindex (e1, _) ->
-            let arr = eval e1 mem loc |> Val.get_array_blk in
+            let arr = eval e1 mem |> Val.get_array_blk in
             (* must have array blk *)
-            (* let idx = eval e2 mem loc in *)
+            (* let idx = eval e2 mem in *)
             let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
             (* if nested array, add the array blk *)
             let arr = Mem.find_heap_set ploc mem in
@@ -224,9 +223,9 @@ module Make (CFG : ProcCfg.S) = struct
             Val.Itv.top
 
 
-  and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t =
-    fun unop e mem loc ->
-      let v = eval e mem loc in
+  and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t =
+    fun unop e mem ->
+      let v = eval e mem in
       match unop with
       | Unop.Neg ->
           Val.neg v
@@ -236,10 +235,10 @@ module Make (CFG : ProcCfg.S) = struct
           Val.lnot v
 
 
-  and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t =
-    fun binop e1 e2 mem loc ->
-      let v1 = eval e1 mem loc in
-      let v2 = eval e2 mem loc in
+  and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
+    fun binop e1 e2 mem ->
+      let v1 = eval e1 mem in
+      let v2 = eval e2 mem in
       match binop with
       | Binop.PlusA ->
           Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
@@ -281,8 +280,8 @@ module Make (CFG : ProcCfg.S) = struct
           Val.lor_sem v1 v2
 
 
-  let rec eval_locs : Exp.t -> Mem.astate -> Location.t -> Val.t =
-    fun exp mem loc ->
+  let rec eval_locs : Exp.t -> Mem.astate -> Val.t =
+    fun exp mem ->
       match exp with
       | Exp.Var id -> (
         match Mem.find_alias id mem with
@@ -293,14 +292,14 @@ module Make (CFG : ProcCfg.S) = struct
       | Exp.Lvar pvar ->
           pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc
       | Exp.BinOp (bop, e1, e2) ->
-          eval_binop bop e1 e2 mem loc
+          eval_binop bop e1 e2 mem
       | Exp.Cast (_, e) ->
-          eval_locs e mem loc
+          eval_locs e mem
       | Exp.Lfield (e, fn, _) ->
-          eval e mem loc |> Val.get_all_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
+          eval e mem |> Val.get_all_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
       | Exp.Lindex (e1, e2) ->
-          let arr = eval e1 mem loc in
-          let idx = eval e2 mem loc in
+          let arr = eval e1 mem in
+          let idx = eval e2 mem in
           Val.plus_pi arr idx
       | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
           Val.bot
@@ -358,8 +357,8 @@ module Make (CFG : ProcCfg.S) = struct
           mem
 
 
-  let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
-    fun e loc mem ->
+  let prune_binop_left : Exp.t -> Mem.astate -> Mem.astate =
+    fun e mem ->
       match e with
       | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
       | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e')
@@ -368,7 +367,7 @@ module Make (CFG : ProcCfg.S) = struct
         match Mem.find_simple_alias x mem with
         | Some lv ->
             let v = Mem.find_heap lv mem in
-            let v' = Val.prune_comp comp v (eval e' mem loc) in
+            let v' = Val.prune_comp comp v (eval e' mem) in
             Mem.update_mem (PowLoc.singleton lv) v' mem
         | None ->
             mem )
@@ -376,7 +375,7 @@ module Make (CFG : ProcCfg.S) = struct
         match Mem.find_simple_alias x mem with
         | Some lv ->
             let v = Mem.find_heap lv mem in
-            let v' = Val.prune_eq v (eval e' mem loc) in
+            let v' = Val.prune_eq v (eval e' mem) in
             Mem.update_mem (PowLoc.singleton lv) v' mem
         | None ->
             mem )
@@ -384,7 +383,7 @@ module Make (CFG : ProcCfg.S) = struct
         match Mem.find_simple_alias x mem with
         | Some lv ->
             let v = Mem.find_heap lv mem in
-            let v' = Val.prune_ne v (eval e' mem loc) in
+            let v' = Val.prune_ne v (eval e' mem) in
             Mem.update_mem (PowLoc.singleton lv) v' mem
         | None ->
             mem )
@@ -392,8 +391,8 @@ module Make (CFG : ProcCfg.S) = struct
           mem
 
 
-  let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
-    fun e loc mem ->
+  let prune_binop_right : Exp.t -> Mem.astate -> Mem.astate =
+    fun e mem ->
       match e with
       | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x)
@@ -401,43 +400,42 @@ module Make (CFG : ProcCfg.S) = struct
       | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x)
       | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) ->
-          prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
+          prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem
       | _ ->
           mem
 
 
-  let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool =
-    fun e loc m -> Val.( <= ) ~lhs:(eval e m loc) ~rhs:(Val.of_int 0)
+  let is_unreachable_constant : Exp.t -> Mem.astate -> bool =
+    fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0)
 
 
-  let prune_unreachable : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
-    fun e loc mem -> if is_unreachable_constant e loc mem then Mem.bot else mem
+  let prune_unreachable : Exp.t -> Mem.astate -> Mem.astate =
+    fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem
 
 
-  let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
-    fun e loc mem ->
+  let rec prune : Exp.t -> Mem.astate -> Mem.astate =
+    fun e mem ->
       let mem =
-        mem |> prune_unreachable e loc |> prune_unop e |> prune_binop_left e loc
-        |> prune_binop_right e loc
+        mem |> prune_unreachable e |> prune_unop e |> prune_binop_left e |> prune_binop_right e
       in
       match e with
       | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
-          prune e loc mem
+          prune e mem
       | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
-          prune (Exp.UnOp (Unop.LNot, e, None)) loc mem
+          prune (Exp.UnOp (Unop.LNot, e, None)) mem
       | Exp.UnOp (Unop.Neg, Exp.Var x, _) ->
-          prune (Exp.Var x) loc mem
+          prune (Exp.Var x) mem
       | Exp.BinOp (Binop.LAnd, e1, e2) ->
-          mem |> prune e1 loc |> prune e2 loc
+          mem |> prune e1 |> prune e2
       | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
-          mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc
+          mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) |> prune (Exp.UnOp (Unop.LNot, e2, t))
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _)
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _)
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _)
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _)
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _)
       | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) ->
-          prune (Exp.BinOp (comp_not c, e1, e2)) loc mem
+          prune (Exp.BinOp (comp_not c, e1, e2)) mem
       | _ ->
           mem
 
@@ -553,10 +551,10 @@ module Make (CFG : ProcCfg.S) = struct
 
   let get_subst_map
       : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
-        -> callee_ret_alias:AliasTarget.t option -> Location.t
+        -> callee_ret_alias:AliasTarget.t option
         -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t)
            * AliasTarget.t option =
-    fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc ->
+    fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias ->
       let add_pair (formal, typ) actual (l, ret_alias) =
         let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
         let new_matching, ret_alias' =
@@ -565,7 +563,7 @@ module Make (CFG : ProcCfg.S) = struct
         (List.rev_append new_matching l, Option.first_some ret_alias ret_alias')
       in
       let formals = get_formals callee_pdesc in
-      let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in
+      let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in
       let pairs, ret_alias =
         list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None)
       in
diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml
index 5a1e21803..f66906ff8 100644
--- a/infer/src/bufferoverrun/bufferOverrunTrace.ml
+++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml
@@ -35,18 +35,18 @@ module BoTrace = struct
   let pp_elem : F.formatter -> elem -> unit =
     fun fmt elem ->
       match elem with
-      | Assign loc ->
-          F.fprintf fmt "Assign (%a)" Location.pp_file_pos loc
-      | ArrDecl loc ->
-          F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos loc
-      | Call loc ->
-          F.fprintf fmt "Call (%a)" Location.pp_file_pos loc
-      | Return loc ->
-          F.fprintf fmt "Return (%a)" Location.pp_file_pos loc
-      | SymAssign loc ->
-          F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos loc
-      | ArrAccess loc ->
-          F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos loc
+      | Assign location ->
+          F.fprintf fmt "Assign (%a)" Location.pp_file_pos location
+      | ArrDecl location ->
+          F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos location
+      | Call location ->
+          F.fprintf fmt "Call (%a)" Location.pp_file_pos location
+      | Return location ->
+          F.fprintf fmt "Return (%a)" Location.pp_file_pos location
+      | SymAssign location ->
+          F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos location
+      | ArrAccess location ->
+          F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos location
 
 
   let pp : F.formatter -> t -> unit =
@@ -78,30 +78,32 @@ module Set = struct
     if is_empty t then singleton (BoTrace.singleton elem) else map (BoTrace.add_elem_last elem) t
 
 
-  let instantiate ~traces_caller ~traces_callee loc =
+  let instantiate ~traces_caller ~traces_callee location =
     if is_empty traces_caller then
-      map (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call loc) trace_callee) traces_callee
+      map
+        (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call location) trace_callee)
+        traces_callee
     else
       fold
         (fun trace_callee traces ->
           fold
             (fun trace_caller traces ->
-              let new_trace_caller = BoTrace.add_elem (BoTrace.Call loc) trace_caller in
+              let new_trace_caller = BoTrace.add_elem (BoTrace.Call location) trace_caller in
               let new_trace = BoTrace.append trace_callee new_trace_caller in
               add new_trace traces)
             traces_caller traces)
         traces_callee empty
 
 
-  let merge ~traces_arr ~traces_idx loc =
+  let merge ~traces_arr ~traces_idx location =
     if is_empty traces_idx then
-      map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess loc) trace_arr) traces_arr
+      map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess location) trace_arr) traces_arr
     else
       fold
         (fun trace_idx traces ->
           fold
             (fun trace_arr traces ->
-              let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess loc) trace_idx in
+              let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess location) trace_idx in
               let new_trace = BoTrace.append new_trace_idx trace_arr in
               add new_trace traces)
             traces_arr traces)