From f9161b164fdf5823fd897ad2e8c5e1953c867e1e Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Sat, 8 Dec 2018 19:28:38 -0800
Subject: [PATCH] [inferbo] On-demand heap symbol using path

Summary:
It materializes symbolic values of function parameters on-demand. The on-demand materialization is triggered when finding a value from an abstract memory and joining/widening abstract memories.

Depends on D13294630

Main idea:

* Symbolic values are on-demand-ly generated by a symbol path and its type
* In order to avoid infinite generation of symbolic values, symbol paths are canonicalized by structure types and field names (which means they are abstracted to the same value). For example, in a linked list, a symbolic value `x->next->next` is canonicalized to `x->next` when the structures (`*x` and `*x->next`) have the same structure type and the same field name (`next`).

Changes from the previous code:

* `Symbol.t` does not include `id` and `pname` for distinguishing symbols. Now, all symbols are compared by `path:SymbolPath.partial` and `bound_end`.
* `SymbolTable` is no longer used, which was used for generating symbolic values with new `id`s.

Reviewed By: mbouaziz

Differential Revision: D13294635

fbshipit-source-id: fa422f084
---
 infer/src/bufferoverrun/absLoc.ml             |  38 +++
 infer/src/bufferoverrun/arrayBlk.ml           |  15 +-
 infer/src/bufferoverrun/bounds.ml             |  23 +-
 infer/src/bufferoverrun/bounds.mli            |  14 +-
 .../src/bufferoverrun/bufferOverrunChecker.ml | 235 +++-------------
 .../src/bufferoverrun/bufferOverrunDomain.ml  | 266 +++++++++++++++---
 .../src/bufferoverrun/bufferOverrunModels.ml  |  29 +-
 .../bufferoverrun/bufferOverrunSemantics.ml   |  41 +--
 infer/src/bufferoverrun/bufferOverrunUtils.ml |  56 +---
 .../src/bufferoverrun/bufferOverrunUtils.mli  |  24 +-
 infer/src/bufferoverrun/itv.ml                |  34 ++-
 infer/src/bufferoverrun/itv.mli               |  10 +-
 infer/src/bufferoverrun/symb.ml               | 114 ++------
 infer/src/bufferoverrun/symb.mli              |  21 +-
 .../codetoanalyze/c/bufferoverrun/get_field.c |   2 +-
 .../codetoanalyze/c/bufferoverrun/issues.exp  |  26 +-
 .../codetoanalyze/c/performance/issues.exp    |   6 +-
 .../codetoanalyze/cpp/bufferoverrun/class.cpp |   4 +-
 .../cpp/bufferoverrun/issues.exp              |  78 +++--
 .../cpp/bufferoverrun/repro1.cpp              |  12 +-
 .../java/performance/UnknownCallsTest.java    |   4 +-
 .../codetoanalyze/java/performance/issues.exp |  25 +-
 22 files changed, 539 insertions(+), 538 deletions(-)

diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index 7796abe88..bb102c161 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -73,6 +73,12 @@ module Allocsite = struct
   let unknown = Unknown
 
   let get_path = function Unknown -> None | Symbol path -> Some path | Known {path} -> path
+
+  let get_param_path = function
+    | Symbol path ->
+        Option.some_if (not (Symb.SymbolPath.represents_callsite_sound_partial path)) path
+    | Unknown | Known _ ->
+        None
 end
 
 module Loc = struct
@@ -128,6 +134,16 @@ module Loc = struct
 
   let of_id id = Var (Var.of_id id)
 
+  let rec of_path path =
+    match path with
+    | Symb.SymbolPath.Pvar pvar ->
+        of_pvar pvar
+    | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _ ->
+        Allocsite (Allocsite.make_symbol path)
+    | Symb.SymbolPath.Field (fn, path) ->
+        Field (of_path path, fn)
+
+
   let append_field l ~fn = Field (l, fn)
 
   let is_return = function
@@ -148,6 +164,21 @@ module Loc = struct
         Allocsite.get_path allocsite
     | Field (l, fn) ->
         Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
+
+
+  let rec get_param_path = function
+    | Var _ ->
+        None
+    | Allocsite allocsite ->
+        Allocsite.get_param_path allocsite
+    | Field (l, fn) ->
+        Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
+
+
+  let has_param_path formals x =
+    Option.value_map (get_path x) ~default:false ~f:(fun x ->
+        Option.value_map (Symb.SymbolPath.get_pvar x) ~default:false ~f:(fun x ->
+            List.exists formals ~f:(fun (formal, _) -> Pvar.equal x formal) ) )
 end
 
 module PowLoc = struct
@@ -173,6 +204,13 @@ module PowLoc = struct
 
 
   type eval_locpath = Symb.SymbolPath.partial -> t
+
+  let subst_loc l (eval_locpath : eval_locpath) =
+    match Loc.get_param_path l with None -> singleton l | Some path -> eval_locpath path
+
+
+  let subst x (eval_locpath : eval_locpath) =
+    fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
 end
 
 (** unsound but ok for bug catching *)
diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index 325c51506..19c0e7350 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -153,8 +153,19 @@ let get_pow_loc : t -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : t -> Bound.eval_sym -> t =
- fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
+let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
+ fun a eval_sym eval_locpath ->
+  let subst1 l info acc =
+    let info' = ArrInfo.subst info eval_sym in
+    match Allocsite.get_param_path l with
+    | None ->
+        add l info' acc
+    | Some path ->
+        let locs = eval_locpath path in
+        let add_allocsite l acc = match l with Loc.Allocsite a -> add a info' acc | _ -> acc in
+        PowLoc.fold add_allocsite locs acc
+  in
+  fold subst1 a empty
 
 
 let get_symbols : t -> Itv.SymbolSet.t =
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 68e4d8dd3..c3fd99b82 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -49,18 +49,6 @@ module SymLinear = struct
     M.for_all2 ~f:le_one_pair x y
 
 
-  let make :
-         unsigned:bool
-      -> Typ.Procname.t
-      -> Symb.SymbolTable.t
-      -> Symb.SymbolPath.t
-      -> Counter.t
-      -> t * t =
-   fun ~unsigned pname symbol_table path new_sym_num ->
-    let lb, ub = Symb.SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in
-    (singleton_one lb, singleton_one ub)
-
-
   let pp1 :
       markup:bool -> is_beginning:bool -> F.formatter -> Symb.Symbol.t -> NonZeroInt.t -> unit =
    fun ~markup ~is_beginning f s c ->
@@ -269,6 +257,17 @@ module Bound = struct
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
+  let of_path path_of_partial bound_end ~unsigned partial =
+    let s = Symb.Symbol.make ~unsigned (path_of_partial partial) bound_end in
+    of_sym (SymLinear.singleton_one s)
+
+
+  let of_normal_path = of_path Symb.SymbolPath.normal
+
+  let of_offset_path = of_path Symb.SymbolPath.offset ~unsigned:false
+
+  let of_length_path = of_path Symb.SymbolPath.length ~unsigned:true
+
   let is_symbolic : t -> bool = function
     | MInf | PInf ->
         false
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index 46b40bbcf..81b707a88 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -14,14 +14,6 @@ module SymLinear : sig
   module M = Symb.SymbolMap
 
   type t = Ints.NonZeroInt.t M.t
-
-  val make :
-       unsigned:bool
-    -> Typ.Procname.t
-    -> Symb.SymbolTable.t
-    -> Symb.SymbolPath.t
-    -> Counter.t
-    -> t * t
 end
 
 module Bound : sig
@@ -51,7 +43,11 @@ module Bound : sig
 
   val _255 : t
 
-  val of_sym : SymLinear.t -> t
+  val of_normal_path : Symb.BoundEnd.t -> unsigned:bool -> Symb.SymbolPath.partial -> t
+
+  val of_offset_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
+
+  val of_length_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
 
   val is_symbolic : t -> bool
 
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index da1615134..501748a04 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -26,121 +26,13 @@ module Payload = SummaryPayload.Make (struct
   let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun
 end)
 
-type extras = {symbol_table: Itv.SymbolTable.t; integer_type_widths: Typ.IntegerWidths.t}
+type extras = Dom.OndemandEnv.t
 
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 module Init = struct
-  let declare_symbolic_val :
-         Typ.Procname.t
-      -> Itv.SymbolTable.t
-      -> Itv.SymbolPath.partial
-      -> Tenv.t
-      -> Typ.IntegerWidths.t
-      -> node_hash:int
-      -> Location.t
-      -> Loc.t
-      -> Typ.typ
-      -> new_sym_num:Counter.t
-      -> Dom.Mem.t
-      -> Dom.Mem.t =
-   fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num
-       mem ->
-    let max_depth = 2 in
-    let rec decl_sym_val pname path tenv location ~depth ~may_last_field loc typ mem =
-      if depth > max_depth then mem
-      else
-        let depth = depth + 1 in
-        match typ.Typ.desc with
-        | Typ.Tint ikind ->
-            let unsigned = Typ.ikind_is_unsigned ikind in
-            let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
-            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
-        | Typ.Tfloat _ ->
-            let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
-            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
-        | Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
-          match typ with
-          | {desc= Typ.Tarray {elt}} ->
-              BoUtils.Exec.decl_sym_arr
-                ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc
-                elt ~new_sym_num mem
-          | _ ->
-              BoUtils.Exec.decl_sym_java_ptr
-                ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                pname path tenv location ~depth loc typ mem )
-        | Typ.Tptr (typ, _) ->
-            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
-              Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ
-              ~new_sym_num mem
-        | Typ.Tarray {elt; length; stride} ->
-            let size =
-              match length with
-              | Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
-                  None (* Will be made symbolic by [decl_sym_arr] *)
-              | _ ->
-                  Option.map ~f:Itv.of_int_lit length
-            in
-            let offset = Itv.zero in
-            let stride = Option.map ~f:IntLit.to_int_exn stride in
-            BoUtils.Exec.decl_sym_arr
-              ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt
-              ~offset ?size ?stride ~new_sym_num mem
-        | Typ.Tstruct typename -> (
-          match Models.TypName.dispatch tenv typename with
-          | Some {Models.declare_symbolic} ->
-              let model_env =
-                Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
-              in
-              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
-                loc ~new_sym_num mem
-          | None ->
-              let decl_fld ~may_last_field mem (fn, typ, _) =
-                let loc_fld = Loc.append_field loc ~fn in
-                let path = Itv.SymbolPath.field path fn in
-                decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field mem
-              in
-              let decl_flds str =
-                IList.fold_last ~f:(decl_fld ~may_last_field:false)
-                  ~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields
-              in
-              let opt_struct = Tenv.lookup tenv typename in
-              Option.value_map opt_struct ~default:mem ~f:decl_flds )
-        | _ ->
-            if Config.bo_debug >= 3 then
-              L.(debug BufferOverrun Verbose)
-                "/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp
-                location ;
-            mem
-    in
-    decl_sym_val pname path tenv location ~depth:0 ~may_last_field:true loc typ mem
-
-
-  let declare_symbolic_parameters :
-         Typ.Procname.t
-      -> Tenv.t
-      -> Typ.IntegerWidths.t
-      -> node_hash:int
-      -> Location.t
-      -> Itv.SymbolTable.t
-      -> (Pvar.t * Typ.t) list
-      -> Dom.Mem.t
-      -> Dom.Mem.t =
-   fun pname tenv integer_type_widths ~node_hash location symbol_table formals mem ->
-    let new_sym_num = Counter.make 0 in
-    let add_formal mem (pvar, typ) =
-      let loc = Loc.of_pvar pvar in
-      let path = Itv.SymbolPath.of_pvar pvar in
-      declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc
-        typ ~new_sym_num mem
-    in
-    List.fold ~f:add_formal ~init:mem formals
-
-
-  let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node
-      =
+  let initial_state {ProcData.pdesc; tenv; extras= {Dom.OndemandEnv.integer_type_widths} as oenv}
+      start_node =
     let node_hash = CFG.Node.hash start_node in
     let location = CFG.Node.loc start_node in
     let pname = Procdesc.get_proc_name pdesc in
@@ -155,7 +47,7 @@ module Init = struct
         match Models.TypName.dispatch tenv typname with
         | Some {Models.declare_local} ->
             let model_env =
-              Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
+              Models.mk_model_env pname node_hash location tenv integer_type_widths
             in
             declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
               ~dimension mem
@@ -170,11 +62,9 @@ module Init = struct
       decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
         ~dimension:1 mem
     in
-    let mem = Dom.Mem.init in
+    let mem = Dom.Mem.init oenv in
     let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
-    let formals = Dom.get_formals pdesc in
-    declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
-      formals mem
+    mem
 end
 
 module TransferFunctions = struct
@@ -183,21 +73,24 @@ module TransferFunctions = struct
 
   type nonrec extras = extras
 
-  let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace mem location =
-    let copy_reachable_new_locs_from locs mem =
+  let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem
+      ({Dom.eval_locpath} as eval_sym_trace) mem location =
+    let formals = Dom.get_formals callee_pdesc in
+    let copy_reachable_locs_from locs mem =
       let copy loc acc =
         Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
+            let locs = PowLoc.subst_loc loc eval_locpath in
             let v = Dom.Val.subst v eval_sym_trace location in
-            Dom.Mem.add_heap loc v acc )
+            PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc )
       in
-      let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
+      let reachable_locs = Dom.Mem.get_reachable_locs_from formals locs callee_exit_mem in
       PowLoc.fold copy reachable_locs mem
     in
     let instantiate_ret_alias mem =
       let subst_loc l =
         Option.find_map (Loc.get_path l) ~f:(fun partial ->
             try
-              let locs = eval_sym_trace.Dom.eval_locpath partial in
+              let locs = eval_locpath partial in
               match PowLoc.is_singleton_or_more locs with
               | IContainer.Singleton loc ->
                   Some loc
@@ -209,52 +102,18 @@ module TransferFunctions = struct
         Option.find_map (Dom.Mem.find_ret_alias callee_exit_mem) ~f:(fun alias_target ->
             Dom.AliasTarget.loc_map alias_target ~f:subst_loc )
       in
-      Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias id l mem)
+      Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias ret_id l mem)
     in
-    let ret_var = Loc.of_var (Var.of_id id) in
+    let ret_var = Loc.of_var (Var.of_id ret_id) in
     let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in
-    Dom.Val.subst ret_val eval_sym_trace location
-    |> Fn.flip (Dom.Mem.add_stack ret_var) mem
-    |> instantiate_ret_alias
-    |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
-
-
-  let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem =
-    let formals = Dom.get_formals pdesc in
-    let actuals_locs = List.map ~f:(fun (a, _) -> Sem.eval_locs a mem) params in
-    let f mem formal actual_locs =
-      match (snd formal).Typ.desc with
-      | Typ.Tptr (typ, _) -> (
-        match typ.Typ.desc with
-        | Typ.Tstruct typename -> (
-          match Tenv.lookup tenv typename with
-          | Some str ->
-              let formal_locs =
-                Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
-                |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
-              in
-              let instantiate_fld mem (fn, _, _) =
-                let formal_fields = PowLoc.append_field formal_locs ~fn in
-                let v = Dom.Mem.find_set formal_fields callee_exit_mem in
-                let actual_fields = PowLoc.append_field actual_locs ~fn in
-                Dom.Val.subst v eval_sym_trace location
-                |> Fn.flip (Dom.Mem.strong_update actual_fields) mem
-              in
-              List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields
-          | _ ->
-              mem )
-        | _ ->
-            let formal_locs =
-              Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
-              |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
-            in
-            let v = Dom.Mem.find_set formal_locs callee_exit_mem in
-            Dom.Val.subst v eval_sym_trace location
-            |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
-      | _ ->
-          mem
+    let formal_locs =
+      List.fold formals ~init:PowLoc.bot ~f:(fun acc (formal, _) ->
+          let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in
+          PowLoc.join acc (Dom.Val.get_all_locs v) )
     in
-    try List.fold2_exn formals actuals_locs ~init:mem ~f with Invalid_argument _ -> mem
+    Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
+    |> instantiate_ret_alias
+    |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val))
 
 
   let forget_ret_relation ret callee_pname mem =
@@ -291,15 +150,15 @@ module TransferFunctions = struct
       Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem
     in
     let caller_mem =
-      instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location
-      |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location
+      instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace
+        caller_mem location
       |> forget_ret_relation ret callee_pname
     in
     Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
 
 
   let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-   fun mem {pdesc; tenv; extras= {symbol_table; integer_type_widths}} node instr ->
+   fun mem {pdesc; tenv; extras= {integer_type_widths}} node instr ->
     match instr with
     | Load (id, _, _, _) when Ident.is_none id ->
         mem
@@ -371,7 +230,6 @@ module TransferFunctions = struct
             let node_hash = CFG.Node.hash node in
             let model_env =
               Models.mk_model_env callee_pname node_hash location tenv integer_type_widths
-                symbol_table
             in
             exec model_env ~ret mem
         | None -> (
@@ -389,13 +247,13 @@ module TransferFunctions = struct
           | None ->
               L.d_printfln "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ;
               if is_external callee_pname then (
-                let node_hash = CFG.Node.hash node in
-                let path = Itv.SymbolPath.of_callsite (CallSite.make callee_pname location) in
                 L.(debug BufferOverrun Verbose)
                   "/!\\ External call to unknown  %a \n\n" Typ.Procname.pp callee_pname ;
-                Init.declare_symbolic_val callee_pname symbol_table path tenv integer_type_widths
-                  ~node_hash location (Loc.of_id id) ret_typ ~new_sym_num:(Counter.make node_hash)
-                  mem )
+                let callsite = CallSite.make callee_pname location in
+                let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in
+                let loc = Loc.of_allocsite (Allocsite.make_symbol path) in
+                let v = Dom.Mem.find loc mem in
+                Dom.Mem.add_stack (Loc.of_id id) v mem )
               else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) )
     | Call ((id, _), fun_exp, _, location, _) ->
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
@@ -619,13 +477,12 @@ module Report = struct
          Procdesc.t
       -> Tenv.t
       -> Typ.IntegerWidths.t
-      -> Itv.SymbolTable.t
       -> CFG.Node.t
       -> Sil.instr
       -> Dom.Mem.t
       -> PO.ConditionSet.checked_t
       -> PO.ConditionSet.checked_t =
-   fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set ->
+   fun pdesc tenv integer_type_widths node instr mem cond_set ->
     match instr with
     | Sil.Load (_, exp, _, location) ->
         cond_set
@@ -646,7 +503,7 @@ module Report = struct
             let node_hash = CFG.Node.hash node in
             let pname = Procdesc.get_proc_name pdesc in
             check
-              (Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table)
+              (Models.mk_model_env pname node_hash location tenv integer_type_widths)
               mem cond_set
         | None -> (
           match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
@@ -682,14 +539,13 @@ module Report = struct
       -> Procdesc.t
       -> Tenv.t
       -> Typ.IntegerWidths.t
-      -> Itv.SymbolTable.t
       -> CFG.t
       -> CFG.Node.t
       -> Instrs.not_reversed_t
       -> Dom.Mem.t AbstractInterpreter.State.t
       -> PO.ConditionSet.checked_t
       -> PO.ConditionSet.checked_t =
-   fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set ->
+   fun summary pdesc tenv integer_type_widths cfg node instrs state cond_set ->
     match state with
     | _ when Instrs.is_empty instrs ->
         cond_set
@@ -706,9 +562,7 @@ module Report = struct
           | NonBottom _ ->
               ()
         in
-        let cond_set =
-          check_instr pdesc tenv integer_type_widths symbol_table node instr pre cond_set
-        in
+        let cond_set = check_instr pdesc tenv integer_type_widths node instr pre cond_set in
         print_debug_info instr pre cond_set ;
         cond_set
 
@@ -718,18 +572,16 @@ module Report = struct
       -> Procdesc.t
       -> Tenv.t
       -> Typ.IntegerWidths.t
-      -> Itv.SymbolTable.t
       -> CFG.t
       -> Analyzer.invariant_map
       -> PO.ConditionSet.checked_t
       -> CFG.Node.t
       -> PO.ConditionSet.checked_t =
-   fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map cond_set node ->
+   fun summary pdesc tenv integer_type_widths cfg inv_map cond_set node ->
     match Analyzer.extract_state (CFG.Node.id node) inv_map with
     | Some state ->
         let instrs = CFG.instrs node in
-        check_instrs summary pdesc tenv integer_type_widths symbol_table cfg node instrs state
-          cond_set
+        check_instrs summary pdesc tenv integer_type_widths cfg node instrs state cond_set
     | _ ->
         cond_set
 
@@ -739,13 +591,12 @@ module Report = struct
       -> Procdesc.t
       -> Tenv.t
       -> Typ.IntegerWidths.t
-      -> Itv.SymbolTable.t
       -> CFG.t
       -> Analyzer.invariant_map
       -> PO.ConditionSet.checked_t =
-   fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map ->
+   fun summary pdesc tenv integer_type_widths cfg inv_map ->
     CFG.fold_nodes cfg
-      ~f:(check_node summary pdesc tenv integer_type_widths symbol_table cfg inv_map)
+      ~f:(check_node summary pdesc tenv integer_type_widths cfg inv_map)
       ~init:PO.ConditionSet.empty
 
 
@@ -786,8 +637,8 @@ let get_local_decls proc_desc =
 let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
  fun {proc_desc; tenv; integer_type_widths; summary} ->
   Preanal.do_preanalysis proc_desc tenv ;
-  let symbol_table = Itv.SymbolTable.empty () in
-  let pdata = ProcData.make proc_desc tenv {symbol_table; integer_type_widths} in
+  let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in
+  let pdata = ProcData.make proc_desc tenv oenv in
   let cfg = CFG.from_pdesc proc_desc in
   let initial = Init.initial_state pdata (CFG.start_node cfg) in
   let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in
@@ -797,13 +648,13 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
     |> Option.map ~f:(Dom.Mem.forget_locs locals)
   in
   let cond_set =
-    Report.check_proc summary proc_desc tenv integer_type_widths symbol_table cfg inv_map
+    Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map
     |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
   in
   let summary =
     match exit_mem with
     | Some exit_mem ->
-        let post = (exit_mem, cond_set) in
+        let post = (Dom.Mem.unset_oenv exit_mem, cond_set) in
         Payload.update_summary post summary
     | _ ->
         summary
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 92f2f0d55..9c79c2a93 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -13,6 +13,7 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module Relation = BufferOverrunDomainRelation
+module SPath = Symb.SymbolPath
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
@@ -27,6 +28,89 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
   Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
 
 
+module OndemandEnv = struct
+  type t =
+    { typ_of_param_path: SPath.partial -> Typ.t option
+    ; may_last_field: SPath.partial -> bool
+    ; entry_location: Location.t
+    ; integer_type_widths: Typ.IntegerWidths.t }
+
+  let mk pdesc =
+    let module FormalTyps = Caml.Map.Make (Pvar) in
+    let formal_typs =
+      List.fold (get_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) ->
+          FormalTyps.add formal typ acc )
+    in
+    fun tenv integer_type_widths ->
+      let rec typ_of_param_path = function
+        | SPath.Pvar x ->
+            FormalTyps.find_opt x formal_typs
+        | SPath.Deref (_, x) ->
+            Option.map (typ_of_param_path x) ~f:(fun typ ->
+                match typ.Typ.desc with
+                | Tptr (typ, _) ->
+                    typ
+                | Tarray {elt} ->
+                    elt
+                | Tvoid ->
+                    Typ.void
+                | _ ->
+                    L.(die InternalError) "Untyped expression is given." )
+        | SPath.Field (fn, x) ->
+            let lookup = Tenv.lookup tenv in
+            Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn)
+        | SPath.Callsite {ret_typ} ->
+            Some ret_typ
+      in
+      let is_last_field fn (fields : Typ.Struct.field list) =
+        Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) ->
+            Typ.Fieldname.equal fn last_fn )
+      in
+      let rec may_last_field = function
+        | SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
+            true
+        | SPath.Field (fn, x) ->
+            may_last_field x
+            && Option.value_map ~default:true (typ_of_param_path x) ~f:(fun parent_typ ->
+                   match parent_typ.Typ.desc with
+                   | Tstruct typename ->
+                       let opt_struct = Tenv.lookup tenv typename in
+                       Option.value_map opt_struct ~default:false ~f:(fun str ->
+                           is_last_field fn str.Typ.Struct.fields )
+                   | _ ->
+                       true )
+      in
+      let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
+      {typ_of_param_path; may_last_field; entry_location; integer_type_widths}
+
+
+  let canonical_path typ_of_param_path path =
+    let module KnownFields = Caml.Map.Make (struct
+      type t = Typ.t option * Typ.Fieldname.t [@@deriving compare]
+    end) in
+    let rec helper path =
+      match path with
+      | SPath.Pvar _ | SPath.Callsite _ ->
+          (None, KnownFields.empty)
+      | SPath.Deref (deref_kind, ptr) ->
+          let ptr_opt, known_fields = helper ptr in
+          (Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields)
+      | SPath.Field (fn, struct_path) -> (
+          let struct_path_opt, known_fields = helper struct_path in
+          let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in
+          match KnownFields.find_opt key known_fields with
+          | Some _ as canonicalized ->
+              (canonicalized, known_fields)
+          | None ->
+              let field_path =
+                Option.value_map struct_path_opt ~default:path ~f:(fun struct_path ->
+                    SPath.field struct_path fn )
+              in
+              (None, KnownFields.add key field_path known_fields) )
+    in
+    Option.value (helper path |> fst) ~default:path
+end
+
 module Val = struct
   type t =
     { itv: Itv.t
@@ -145,7 +229,7 @@ module Val = struct
 
   let of_big_int n = of_itv (Itv.of_big_int n)
 
-  let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x}
+  let of_loc ?(traces = TraceSet.empty) x = {bot with powloc= PowLoc.singleton x; traces}
 
   let of_pow_loc ~traces powloc = {bot with powloc; traces}
 
@@ -162,24 +246,6 @@ module Val = struct
 
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
-  let make_sym :
-         ?unsigned:bool
-      -> Loc.t
-      -> Typ.Procname.t
-      -> Itv.SymbolTable.t
-      -> Itv.SymbolPath.partial
-      -> Counter.t
-      -> Location.t
-      -> t =
-   fun ?(unsigned = false) loc pname symbol_table path new_sym_num location ->
-    let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
-    { bot with
-      itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
-    ; sym= Relation.Sym.of_loc loc
-    ; traces= Trace.(Set.singleton location (Parameter loc))
-    ; represents_multiple_values }
-
-
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
 
   let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
@@ -323,7 +389,7 @@ module Val = struct
 
 
   let subst : t -> eval_sym_trace -> Location.t -> t =
-   fun x {eval_sym; trace_of_sym} location ->
+   fun x {eval_sym; trace_of_sym; eval_locpath} location ->
     let symbols = get_symbols x in
     let traces_caller =
       Itv.SymbolSet.fold
@@ -331,7 +397,11 @@ module Val = struct
         symbols TraceSet.empty
     in
     let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in
-    {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}
+    { x with
+      itv= Itv.subst x.itv eval_sym
+    ; powloc= PowLoc.subst x.powloc eval_locpath
+    ; arrayblk= ArrayBlk.subst x.arrayblk eval_sym eval_locpath
+    ; traces }
     (* normalize bottom *)
     |> normalize
 
@@ -359,6 +429,67 @@ module Val = struct
 
   let is_mone x = Itv.is_mone (get_itv x)
 
+  let of_path ~may_last_field integer_type_widths location typ path =
+    let is_java = Language.curr_language_is Java in
+    match typ.Typ.desc with
+    | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
+        let l = Loc.of_path path in
+        let traces = TraceSet.singleton location (Trace.Parameter l) in
+        let unsigned = Typ.is_unsigned_int typ in
+        of_itv ~traces (Itv.of_normal_path ~unsigned path)
+    | Tptr (elt, _) ->
+        if is_java then
+          let l = Loc.of_path path in
+          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          {bot with itv= Itv.of_length_path path; powloc= PowLoc.singleton l; traces}
+        else
+          let deref_kind = SPath.Deref_CPointer in
+          let deref_path = SPath.deref ~deref_kind path in
+          let l = Loc.of_path deref_path in
+          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let arrayblk =
+            let allocsite = Allocsite.make_symbol deref_path in
+            let stride =
+              match elt.Typ.desc with
+              | Typ.Tint ikind ->
+                  Itv.of_int (Typ.width_of_ikind integer_type_widths ikind)
+              | _ ->
+                  Itv.nat
+            in
+            let offset = Itv.of_offset_path path in
+            let size = Itv.of_length_path path in
+            ArrayBlk.make allocsite ~stride ~offset ~size
+          in
+          {bot with arrayblk; traces}
+    | Tstruct _ ->
+        let l = Loc.of_path path in
+        let traces = TraceSet.singleton location (Trace.Parameter l) in
+        of_loc ~traces l
+    | Tarray {length; stride} ->
+        let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
+        let l = Loc.of_path deref_path in
+        let traces = TraceSet.singleton location (Trace.Parameter l) in
+        let allocsite = Allocsite.make_symbol deref_path in
+        let stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in
+        let offset = Itv.zero in
+        let size =
+          Option.value_map length ~default:Itv.top ~f:(fun length ->
+              if may_last_field && (IntLit.iszero length || IntLit.isone length) then
+                Itv.of_length_path path
+              else Itv.of_big_int (IntLit.to_big_int length) )
+        in
+        of_array_alloc allocsite ~stride ~offset ~size ~traces
+
+
+  let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
+   fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
+    Option.value_map (Loc.get_path l) ~default ~f:(fun path ->
+        Option.value_map (typ_of_param_path path) ~default ~f:(fun typ ->
+            let may_last_field = may_last_field path in
+            let path = OndemandEnv.canonical_path typ_of_param_path path in
+            of_path ~may_last_field integer_type_widths entry_location typ path ) )
+
+
   module Itv = struct
     let m1_255 = of_itv Itv.m1_255
 
@@ -394,6 +525,41 @@ module MemPure = struct
           |> Polynomials.NonNegativePolynomial.mult acc
         else acc )
       mem Polynomials.NonNegativePolynomial.one
+
+
+  let join oenv astate1 astate2 =
+    if phys_equal astate1 astate2 then astate1
+    else
+      merge
+        (fun l v1_opt v2_opt ->
+          match (v1_opt, v2_opt) with
+          | Some v1, Some v2 ->
+              Some (Val.join v1 v2)
+          | Some v1, None | None, Some v1 ->
+              let v2 = Val.on_demand ~default:Val.bot oenv l in
+              Some (Val.join v1 v2)
+          | None, None ->
+              None )
+        astate1 astate2
+
+
+  let widen oenv ~prev ~next ~num_iters =
+    if phys_equal prev next then prev
+    else
+      merge
+        (fun l v1_opt v2_opt ->
+          match (v1_opt, v2_opt) with
+          | Some v1, Some v2 ->
+              Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
+          | Some v1, None ->
+              let v2 = Val.on_demand ~default:Val.bot oenv l in
+              Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
+          | None, Some v2 ->
+              let v1 = Val.on_demand ~default:Val.bot oenv l in
+              Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
+          | None, None ->
+              None )
+        prev next
 end
 
 module AliasTarget = struct
@@ -625,14 +791,17 @@ module MemReach = struct
     ; mem_pure: MemPure.t
     ; alias: Alias.t
     ; latest_prune: LatestPrune.t
-    ; relation: Relation.t }
+    ; relation: Relation.t
+    ; oenv: OndemandEnv.t option }
 
-  let init : t =
+  let init : OndemandEnv.t -> t =
+   fun oenv ->
     { stack_locs= StackLocs.bot
     ; mem_pure= MemPure.bot
     ; alias= Alias.bot
     ; latest_prune= LatestPrune.top
-    ; relation= Relation.empty }
+    ; relation= Relation.empty
+    ; oenv= Some oenv }
 
 
   let ( <= ) ~lhs ~rhs =
@@ -647,21 +816,27 @@ module MemReach = struct
 
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
-    else
+    else (
+      assert (phys_equal prev.oenv next.oenv) ;
+      let oenv = Option.value_exn prev.oenv in
       { stack_locs= StackLocs.widen ~prev:prev.stack_locs ~next:next.stack_locs ~num_iters
-      ; mem_pure= MemPure.widen ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
+      ; mem_pure= MemPure.widen oenv ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
       ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
       ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
-      ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters }
+      ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters
+      ; oenv= prev.oenv } )
 
 
   let join : t -> t -> t =
    fun x y ->
+    assert (phys_equal x.oenv y.oenv) ;
+    let oenv = Option.value_exn x.oenv in
     { stack_locs= StackLocs.join x.stack_locs y.stack_locs
-    ; mem_pure= MemPure.join x.mem_pure y.mem_pure
+    ; mem_pure= MemPure.join oenv x.mem_pure y.mem_pure
     ; alias= Alias.join x.alias y.alias
     ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune
-    ; relation= Relation.join x.relation y.relation }
+    ; relation= Relation.join x.relation y.relation
+    ; oenv= x.oenv }
 
 
   let pp : F.formatter -> t -> unit =
@@ -672,16 +847,22 @@ module MemReach = struct
       F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
 
 
+  let unset_oenv x = {x with oenv= None}
+
   let is_stack_loc : Loc.t -> t -> bool = fun l m -> StackLocs.mem l m.stack_locs
 
   let find_opt : Loc.t -> t -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure
 
   let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
 
-  let find_heap : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.Itv.top
+  let find_heap : default:Val.t -> Loc.t -> t -> Val.t =
+   fun ~default l m ->
+    IOption.value_default_f (find_opt l m) ~f:(fun () ->
+        Option.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) )
+
 
   let find : Loc.t -> t -> Val.t =
-   fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m
+   fun l m -> if is_stack_loc l m then find_stack l m else find_heap ~default:Val.Itv.top l m
 
 
   let find_set : PowLoc.t -> t -> Val.t =
@@ -756,7 +937,8 @@ module MemReach = struct
    fun ~f locs m ->
     let transform_mem1 l m =
       let add, find =
-        if is_stack_loc l m then (replace_stack, find_stack) else (add_heap, find_heap)
+        if is_stack_loc l m then (replace_stack, find_stack)
+        else (add_heap, find_heap ~default:Val.bot)
       in
       add l (f (find l m)) m
     in
@@ -815,7 +997,7 @@ module MemReach = struct
         {m with latest_prune= LatestPrune.Top}
 
 
-  let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
+  let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
     let add_reachable1 ~root loc v acc =
       if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
       else if Loc.is_field_of ~loc:root ~field_loc:loc then PowLoc.add loc acc
@@ -828,7 +1010,13 @@ module MemReach = struct
         let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in
         add_from_locs heap reachable_locs (PowLoc.add loc acc)
     in
-    fun locs m -> add_from_locs m.mem_pure locs PowLoc.empty
+    let add_param_locs formals mem acc =
+      let add_loc loc _ acc = if Loc.has_param_path formals loc then PowLoc.add loc acc else acc in
+      MemPure.fold add_loc mem acc
+    in
+    fun formals locs m ->
+      let locs = add_param_locs formals m.mem_pure locs in
+      add_from_locs m.mem_pure locs PowLoc.empty
 
 
   let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
@@ -877,7 +1065,7 @@ module Mem = struct
 
   let bot : t = Bottom
 
-  let init : t = NonBottom MemReach.init
+  let init : OndemandEnv.t -> t = fun oenv -> NonBottom (MemReach.init oenv)
 
   let f_lift_default : default:'a -> (MemReach.t -> 'a) -> t -> 'a =
    fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m'
@@ -952,8 +1140,9 @@ module Mem = struct
 
   let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v)
 
-  let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
-   fun locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from locs)
+  let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
+   fun formals locs ->
+    f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from formals locs)
 
 
   let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v)
@@ -1010,4 +1199,7 @@ module Mem = struct
         caller
     | NonBottom callee ->
         f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller
+
+
+  let unset_oenv = f_lift MemReach.unset_oenv
 end
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index fb8fbb8f2..ae363304b 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -21,11 +21,10 @@ type model_env =
   ; node_hash: int
   ; location: Location.t
   ; tenv: Tenv.t
-  ; integer_type_widths: Typ.IntegerWidths.t
-  ; symbol_table: Itv.SymbolTable.t }
+  ; integer_type_widths: Typ.IntegerWidths.t }
 
-let mk_model_env pname node_hash location tenv integer_type_widths symbol_table =
-  {pname; node_hash; location; tenv; integer_type_widths; symbol_table}
+let mk_model_env pname node_hash location tenv integer_type_widths =
+  {pname; node_hash; location; tenv; integer_type_widths}
 
 
 type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
@@ -50,7 +49,6 @@ type declare_symbolic_fun =
   -> model_env
   -> depth:int
   -> Loc.t
-  -> new_sym_num:Counter.t
   -> Dom.Mem.t
   -> Dom.Mem.t
 
@@ -238,9 +236,12 @@ let infer_print e =
 
 let get_array_length array_exp =
   let exec {integer_type_widths} ~ret mem =
-    let arr = Sem.eval_arr integer_type_widths array_exp mem in
+    let arr = Sem.eval integer_type_widths array_exp mem in
     let traces = Dom.Val.get_traces arr in
-    let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
+    let length =
+      if Language.curr_language_is Java then arr |> Dom.Val.get_itv
+      else arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof
+    in
     let result = Dom.Val.of_itv ~traces length in
     model_by_value result ret mem
   in
@@ -314,12 +315,11 @@ module StdArray = struct
       BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
         ~represents_multiple_values ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val path {pname; tenv; location; symbol_table} ~depth loc
-        ~new_sym_num mem =
+    let declare_symbolic ~decl_sym_val path {pname; tenv; location} ~depth loc mem =
       let offset = Itv.zero in
       let size = Itv.of_int64 length in
-      BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname symbol_table
-        path tenv location ~depth loc typ ~offset ~size ~new_sym_num mem
+      BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname path tenv
+        location ~depth loc typ ~offset ~size mem
     in
     {declare_local; declare_symbolic}
 
@@ -359,7 +359,7 @@ module StdArray = struct
         ~dimension:_ mem =
       (no_model "local" pname location mem, inst_num)
     in
-    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~new_sym_num:_ mem =
+    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc mem =
       no_model "symbolic" pname location mem
     in
     {declare_local; declare_symbolic}
@@ -376,9 +376,8 @@ module Collection = struct
       BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num
         ~represents_multiple_values ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
-        ~new_sym_num mem =
-      BoUtils.Exec.decl_sym_collection pname symbol_table path location loc ~new_sym_num mem
+    let declare_symbolic ~decl_sym_val:_ path {location} ~depth:_ loc mem =
+      BoUtils.Exec.decl_sym_collection path location loc mem
     in
     {declare_local; declare_symbolic}
 
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 0db7c551a..8686c127f 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -142,7 +142,7 @@ let set_array_stride integer_type_widths typ v =
 
 let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths exp mem ->
-  if must_alias_cmp exp mem then Val.Itv.zero
+  if (not (Language.curr_language_is Java)) && must_alias_cmp exp mem then Val.Itv.zero
   else
     match exp with
     | Exp.Var id ->
@@ -346,29 +346,33 @@ let rec eval_sympath_partial params p mem =
       L.(debug BufferOverrun Verbose)
         "Symbol %a is not found in parameters.@\n" (Pvar.pp Pp.text) x ;
       Val.Itv.top )
-  | Symb.SymbolPath.Callsite cs ->
+  | Symb.SymbolPath.Callsite {cs} ->
       L.(debug BufferOverrun Verbose)
         "Symbol for %a is not expected to be in parameters.@\n" Typ.Procname.pp (CallSite.pname cs) ;
-      Val.Itv.top
+      Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
   | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
       let locs = eval_locpath params p mem in
       Mem.find_set locs mem
 
 
 and eval_locpath params p mem =
-  match p with
-  | Symb.SymbolPath.Pvar _ ->
-      let v = eval_sympath_partial params p mem in
-      Val.get_all_locs v
-  | Symb.SymbolPath.Deref (_, p) ->
-      let v = eval_sympath_partial params p mem in
-      Val.get_all_locs v
-  | Symb.SymbolPath.Callsite _ ->
-      let v = eval_sympath_partial params p mem in
-      Val.get_all_locs v
-  | Symb.SymbolPath.Field (fn, p) ->
-      let locs = eval_locpath params p mem in
-      PowLoc.append_field ~fn locs
+  let res =
+    match p with
+    | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
+        let v = eval_sympath_partial params p mem in
+        Val.get_all_locs v
+    | Symb.SymbolPath.Deref (_, p) ->
+        let v = eval_sympath_partial params p mem in
+        Val.get_all_locs v
+    | Symb.SymbolPath.Field (fn, p) ->
+        let locs = eval_locpath params p mem in
+        PowLoc.append_field ~fn locs
+  in
+  if PowLoc.is_empty res then (
+    L.(debug BufferOverrun Verbose)
+      "Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ;
+    PowLoc.unknown )
+  else res
 
 
 let eval_sympath params sympath mem =
@@ -381,7 +385,10 @@ let eval_sympath params sympath mem =
       (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
   | Symb.SymbolPath.Length p ->
       let v = eval_sympath_partial params p mem in
-      (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
+      let traces = Val.get_traces v in
+      let itv = ArrayBlk.sizeof (Val.get_array_blk v) in
+      let itv = if Language.curr_language_is Java then Itv.join itv (Val.get_itv v) else itv in
+      (itv, traces)
 
 
 let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index 955ea90ac..8c738efee 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -128,7 +128,6 @@ module Exec = struct
          decl_sym_val:decl_sym_val
       -> Symb.SymbolPath.deref_kind
       -> Typ.Procname.t
-      -> Itv.SymbolTable.t
       -> Itv.SymbolPath.partial
       -> Tenv.t
       -> Location.t
@@ -138,20 +137,11 @@ module Exec = struct
       -> ?offset:Itv.t
       -> ?size:Itv.t
       -> ?stride:int
-      -> new_sym_num:Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun ~decl_sym_val deref_kind pname symbol_table path tenv location ~depth loc typ ?offset ?size
-       ?stride ~new_sym_num mem ->
-    let offset =
-      IOption.value_default_f offset ~f:(fun () ->
-          Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num )
-    in
-    let size =
-      IOption.value_default_f size ~f:(fun () ->
-          Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
-      )
-    in
+   fun ~decl_sym_val deref_kind pname path tenv location ~depth loc typ ?offset ?size ?stride mem ->
+    let offset = IOption.value_default_f offset ~f:(fun () -> Itv.of_offset_path path) in
+    let size = IOption.value_default_f size ~f:(fun () -> Itv.of_length_path path) in
     let deref_path = Itv.SymbolPath.deref ~deref_kind path in
     let allocsite = Allocsite.make_symbol deref_path in
     let mem =
@@ -168,45 +158,13 @@ module Exec = struct
     decl_sym_val pname deref_path tenv location ~depth deref_loc typ mem
 
 
-  let decl_sym_java_ptr :
-         decl_sym_val:decl_sym_val
-      -> Typ.Procname.t
-      -> Itv.SymbolPath.partial
-      -> Tenv.t
-      -> Location.t
-      -> depth:int
-      -> Loc.t
-      -> Typ.t
-      -> Dom.Mem.t
-      -> Dom.Mem.t =
-   fun ~decl_sym_val pname path tenv location ~depth loc typ mem ->
-    let allocsite = Allocsite.make_symbol path in
-    let alloc_loc = Loc.of_allocsite allocsite in
-    let v =
-      let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
-      let traces = Trace.(Set.singleton location (Trace.Parameter loc)) in
-      Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces
-      |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
-    in
-    let mem = Dom.Mem.add_heap loc v mem in
-    decl_sym_val pname path tenv location ~depth alloc_loc typ mem
-
-
-  let decl_sym_collection :
-         Typ.Procname.t
-      -> Itv.SymbolTable.t
-      -> Itv.SymbolPath.partial
-      -> Location.t
-      -> Loc.t
-      -> new_sym_num:Counter.t
-      -> Dom.Mem.t
-      -> Dom.Mem.t =
-   fun pname symbol_table path location loc ~new_sym_num mem ->
+  let decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
+      =
+   fun path location loc mem ->
     let size =
       let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
       let traces = Trace.(Set.singleton location (Parameter loc)) in
-      Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
-      |> Dom.Val.of_itv ~traces
+      Itv.of_length_path path |> Dom.Val.of_itv ~traces
       |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
     in
     Dom.Mem.add_heap loc size mem
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli
index b421302d7..977fde459 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.mli
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli
@@ -71,7 +71,6 @@ module Exec : sig
        decl_sym_val:decl_sym_val
     -> Symb.SymbolPath.deref_kind
     -> Typ.Procname.t
-    -> Itv.SymbolTable.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
     -> Location.t
@@ -81,31 +80,10 @@ module Exec : sig
     -> ?offset:Itv.t
     -> ?size:Itv.t
     -> ?stride:int
-    -> new_sym_num:Counter.t
     -> Dom.Mem.t
     -> Dom.Mem.t
 
-  val decl_sym_java_ptr :
-       decl_sym_val:decl_sym_val
-    -> Typ.Procname.t
-    -> Itv.SymbolPath.partial
-    -> Tenv.t
-    -> Location.t
-    -> depth:int
-    -> Loc.t
-    -> Typ.t
-    -> Dom.Mem.t
-    -> Dom.Mem.t
-
-  val decl_sym_collection :
-       Typ.Procname.t
-    -> Itv.SymbolTable.t
-    -> Itv.SymbolPath.partial
-    -> Location.t
-    -> Loc.t
-    -> new_sym_num:Counter.t
-    -> Dom.Mem.t
-    -> Dom.Mem.t
+  val decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
 
   val init_array_fields :
        Tenv.t
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 2133404ff..49d36a8f2 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -14,7 +14,6 @@ module L = Logging
 module Bound = Bounds.Bound
 open Ints
 module SymbolPath = Symb.SymbolPath
-module SymbolTable = Symb.SymbolTable
 module SymbolSet = Symb.SymbolSet
 
 module ItvRange = struct
@@ -113,13 +112,6 @@ module ItvPure = struct
 
   let of_big_int n = of_bound (Bound.of_big_int n)
 
-  let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
-      =
-   fun ~unsigned pname symbol_table path new_sym_num ->
-    let lb, ub = Bounds.SymLinear.make ~unsigned pname symbol_table path new_sym_num in
-    (Bound.of_sym lb, Bound.of_sym ub)
-
-
   let mone = of_bound Bound.mone
 
   let m1_255 = (Bound.minus_one, Bound._255)
@@ -417,6 +409,19 @@ module ItvPure = struct
   let max_of_ikind integer_type_widths ikind =
     let _, max = Typ.range_of_ikind integer_type_widths ikind in
     of_big_int max
+
+
+  let of_path bound_of_path path =
+    let lb = bound_of_path Symb.BoundEnd.LowerBound path in
+    let ub = bound_of_path Symb.BoundEnd.UpperBound path in
+    (lb, ub)
+
+
+  let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)
+
+  let of_offset_path = of_path Bound.of_offset_path
+
+  let of_length_path = of_path Bound.of_length_path
 end
 
 include AbstractDomain.BottomLifted (ItvPure)
@@ -552,12 +557,6 @@ let minus : t -> t -> t = lift2 ItvPure.minus
 
 let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv
 
-let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
-    =
- fun ?(unsigned = false) pname symbol_table path new_sym_num ->
-  NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
-
-
 let is_const : t -> Z.t option = bind1zo ItvPure.is_const
 
 let is_mone = bind1bool ItvPure.is_mone
@@ -627,3 +626,10 @@ let normalize : t -> t = bind1 ItvPure.normalize
 
 let max_of_ikind integer_type_widths ikind =
   NonBottom (ItvPure.max_of_ikind integer_type_widths ikind)
+
+
+let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned path)
+
+let of_offset_path path = NonBottom (ItvPure.of_offset_path path)
+
+let of_length_path path = NonBottom (ItvPure.of_length_path path)
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index c0430da08..b228e6dbd 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -10,7 +10,6 @@ open! AbstractDomain.Types
 module F = Format
 module Bound = Bounds.Bound
 module SymbolPath = Symb.SymbolPath
-module SymbolTable = Symb.SymbolTable
 module SymbolSet = Symb.SymbolSet
 
 module ItvRange : sig
@@ -142,9 +141,6 @@ val is_mone : t -> bool
 
 val eq_const : Z.t -> t -> bool
 
-val make_sym :
-  ?unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t -> t
-
 val lb : t -> Bound.t
 
 val ub : t -> Bound.t
@@ -218,3 +214,9 @@ val prune_ne : t -> t -> t
 val subst : t -> Bound.eval_sym -> t
 
 val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t
+
+val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t
+
+val of_offset_path : Symb.SymbolPath.partial -> t
+
+val of_length_path : Symb.SymbolPath.partial -> t
diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml
index aa10ffca0..a44bc8d7b 100644
--- a/infer/src/bufferoverrun/symb.ml
+++ b/infer/src/bufferoverrun/symb.ml
@@ -8,7 +8,7 @@ open! IStd
 module F = Format
 
 module BoundEnd = struct
-  type t = LowerBound | UpperBound
+  type t = LowerBound | UpperBound [@@deriving compare]
 
   let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
 
@@ -22,7 +22,7 @@ module SymbolPath = struct
     | Pvar of Pvar.t
     | Deref of deref_kind * partial
     | Field of Typ.Fieldname.t * partial
-    | Callsite of CallSite.t
+    | Callsite of {ret_typ: Typ.t; cs: CallSite.t}
   [@@deriving compare]
 
   type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare]
@@ -33,7 +33,7 @@ module SymbolPath = struct
 
   let of_pvar pvar = Pvar pvar
 
-  let of_callsite cs = Callsite cs
+  let of_callsite ~ret_typ cs = Callsite {ret_typ; cs}
 
   let field p fn = Field (fn, p)
 
@@ -45,6 +45,15 @@ module SymbolPath = struct
 
   let length p = Length p
 
+  let rec get_pvar = function
+    | Pvar pvar ->
+        Some pvar
+    | Deref (_, partial) | Field (_, partial) ->
+        get_pvar partial
+    | Callsite _ ->
+        None
+
+
   let rec pp_partial_paren ~paren fmt = function
     | Pvar pvar ->
         Pvar.pp_value fmt pvar
@@ -58,7 +67,7 @@ module SymbolPath = struct
         F.fprintf fmt "%a->%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
     | Field (fn, p) ->
         F.fprintf fmt "%a.%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
-    | Callsite cs ->
+    | Callsite {cs} ->
         F.fprintf fmt "%a" Typ.Procname.pp (CallSite.pname cs)
 
 
@@ -94,107 +103,46 @@ module SymbolPath = struct
         represents_callsite_sound_partial p
 
 
-  let represents_partial_sound ~f = function Normal p | Offset p | Length p -> f p
-
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 end
 
 module Symbol = struct
-  type t =
-    | IntraProc of
-        { id: int
-        ; pname: Typ.Procname.t
-        ; unsigned: bool
-        ; path: SymbolPath.t
-        ; bound_end: BoundEnd.t }
-    (* symbols for unknown calls *)
-    | Call of
-        { id: int
-        ; pname: Typ.Procname.t
-        ; unsigned: bool
-        ; path: SymbolPath.t
-        ; bound_end: BoundEnd.t }
+  type extra_bool = bool
 
-  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+  let compare_extra_bool _ _ = 0
 
-  let compare s1 s2 =
-    match (s1, s2) with
-    | IntraProc s1, IntraProc s2 ->
-        (* Parameter symbols only make sense within a given function, so shouldn't be compared across function boundaries. *)
-        assert (phys_equal s1.pname s2.pname) ;
-        Int.compare s1.id s2.id
-    | Call s1, Call s2 ->
-        Int.compare s1.id s2.id
-    | Call _, IntraProc _ ->
-        -1
-    | IntraProc _, Call _ ->
-        1
+  type t = {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t} [@@deriving compare]
 
+  let compare x y =
+    let r = compare x y in
+    if Int.equal r 0 then assert (Bool.equal x.unsigned y.unsigned) ;
+    r
 
-  let equal = [%compare.equal: t]
-
-  let paths_equal s1 s2 =
-    match (s1, s2) with
-    | IntraProc _, Call _ | Call _, IntraProc _ ->
-        false
-    | IntraProc {path= path1}, IntraProc {path= path2} | Call {path= path1}, Call {path= path2} ->
-        SymbolPath.equal path1 path2
 
+  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
 
-  let make_intraproc : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
-   fun ~unsigned pname path bound_end id -> IntraProc {id; pname; unsigned; path; bound_end}
+  let equal = [%compare.equal: t]
 
+  let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
 
-  let make_call : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
-   fun ~unsigned pname path bound_end id -> Call {id; pname; unsigned; path; bound_end}
+  let make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t =
+   fun ~unsigned path bound_end -> {unsigned; path; bound_end}
 
 
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
-    match s with
-    | Call {id; pname; unsigned; path; bound_end} | IntraProc {id; pname; unsigned; path; bound_end}
-      ->
-        SymbolPath.pp fmt path ;
-        if Config.developer_mode then Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end) ;
-        if Config.bo_debug > 1 then
-          let symbol_name = if unsigned then 'u' else 's' in
-          F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id
+    SymbolPath.pp fmt s.path ;
+    if Config.developer_mode then Format.fprintf fmt ".%s" (BoundEnd.to_string s.bound_end) ;
+    if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if s.unsigned then 'u' else 's')
 
 
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
-  let is_unsigned : t -> bool = function IntraProc {unsigned} | Call {unsigned} -> unsigned
-
-  let path = function IntraProc {path} | Call {path} -> path
+  let is_unsigned {unsigned} = unsigned
 
-  let bound_end = function IntraProc {bound_end} | Call {bound_end} -> bound_end
-end
+  let path {path} = path
 
-module SymbolTable = struct
-  module M = PrettyPrintable.MakePPMap (SymbolPath)
-
-  type t = (Symbol.t * Symbol.t) M.t ref
-
-  let empty () = ref M.empty
-
-  let lookup ~unsigned pname path symbol_table new_sym_num =
-    match M.find_opt path !symbol_table with
-    | Some s ->
-        s
-    | None ->
-        let s =
-          if
-            SymbolPath.represents_partial_sound ~f:SymbolPath.represents_callsite_sound_partial
-              path
-          then
-            ( Symbol.make_call ~unsigned pname path LowerBound (Counter.next new_sym_num)
-            , Symbol.make_call ~unsigned pname path UpperBound (Counter.next new_sym_num) )
-          else
-            ( Symbol.make_intraproc ~unsigned pname path LowerBound (Counter.next new_sym_num)
-            , Symbol.make_intraproc ~unsigned pname path UpperBound (Counter.next new_sym_num) )
-        in
-        symbol_table := M.add path s !symbol_table ;
-        s
+  let bound_end {bound_end} = bound_end
 end
 
 module SymbolSet = struct
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index 0d923b9b1..11a9789e9 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/infer/src/bufferoverrun/symb.mli
@@ -21,7 +21,7 @@ module SymbolPath : sig
     | Pvar of Pvar.t
     | Deref of deref_kind * partial
     | Field of Typ.Fieldname.t * partial
-    | Callsite of CallSite.t
+    | Callsite of {ret_typ: Typ.t; cs: CallSite.t}
   [@@deriving compare]
 
   type t = private Normal of partial | Offset of partial | Length of partial
@@ -30,11 +30,15 @@ module SymbolPath : sig
 
   val pp_mark : markup:bool -> F.formatter -> t -> unit
 
+  val pp_partial : F.formatter -> partial -> unit
+
   val pp_partial_paren : paren:bool -> F.formatter -> partial -> unit
 
   val of_pvar : Pvar.t -> partial
 
-  val of_callsite : CallSite.t -> partial
+  val of_callsite : ret_typ:Typ.t -> CallSite.t -> partial
+
+  val get_pvar : partial -> Pvar.t option
 
   val deref : deref_kind:deref_kind -> partial -> partial
 
@@ -47,6 +51,8 @@ module SymbolPath : sig
   val length : partial -> t
 
   val represents_multiple_values : partial -> bool
+
+  val represents_callsite_sound_partial : partial -> bool
 end
 
 module Symbol : sig
@@ -67,6 +73,8 @@ module Symbol : sig
   val path : t -> SymbolPath.t
 
   val bound_end : t -> BoundEnd.t
+
+  val make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t
 end
 
 module SymbolSet : sig
@@ -80,12 +88,3 @@ module SymbolMap : sig
 
   val for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool
 end
-
-module SymbolTable : sig
-  type t
-
-  val empty : unit -> t
-
-  val lookup :
-    unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> t -> Counter.t -> Symbol.t * Symbol.t
-end
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c
index 94fd79bbb..94551507a 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c
@@ -23,7 +23,7 @@ void call_get_field_cond_Bad() {
   }
 }
 
-void FP_call_get_field_Good() {
+void call_get_field_Good() {
   int a[5];
   t x = {0};
   a[get_field_wrapper(&x)] = 0;
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index 04bb92c36..e5b9f1cde 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -3,7 +3,9 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
@@ -46,7 +48,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, COND
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 20 Size: 10]
-codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
+codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f[*]`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 6 Size: 6]
@@ -66,14 +68,14 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVE
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,<Offset trace>,Assignment,<Length trace>,Parameter `a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ]
-codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ]
+codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ]
+codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
-codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
+codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
@@ -82,10 +84,10 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
-codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
+codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
@@ -125,7 +127,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2,
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,Assignment,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: n Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]]
@@ -177,14 +179,14 @@ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label,
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `x`,<Length trace>,Parameter `p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `x`,<Length trace>,Parameter `*p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
-codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
-codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
+codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index f19a41f97..b164d38a7 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -185,6 +185,6 @@ codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_E
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
index d9d1d2f3c..a45c2d5ee 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
@@ -296,7 +296,7 @@ class my_class6 {
 
   void dummy_function() {}
 
-  void set_x_two_Good_FP() {
+  void set_x_two_Good() {
     int arr[5];
     *x = 0;
     dummy_function();
@@ -312,7 +312,7 @@ class my_class6 {
 
   void set_x_three() { *x = 3; }
 
-  void call_set_x_three_Good_FP() {
+  void call_set_x_three_Good() {
     int arr[5];
     set_x_three();
     arr[*x] = 0;
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index ee1914aaa..06328027b 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -9,33 +9,31 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVER
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
-codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this->arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
+codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
 codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this->children`,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this->children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ]
+codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this->children[*]`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
-codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x->b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 3]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x->b[*]`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
-codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
@@ -44,29 +42,29 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 7 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 8 Size: 5 by call to `minus_params_Ok` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params2` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Assignment,Array declaration,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params2` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral` ]
-codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,Parameter `this->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, t->bI.lb), -1+max(1, t->bI.ub)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64]
@@ -74,25 +72,25 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
-codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h`,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `*v->a`,Call,Parameter `*this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `*v->a`,Call,Parameter `*this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp
index f75edb447..b9d984a2e 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp
@@ -78,7 +78,7 @@ struct LM {
     if (t.bI == kBN) {
       return;
     }
-    uI_FP(t.bI, o);
+    uI(t.bI, o);
     t.bI = kBN;
   }
 
@@ -93,7 +93,7 @@ struct LM {
     }
     t.bI = bi;
   }
-  void uI_FP(BI bi, const lo& o) { b[bi - 1]->u(o); }
+  void uI(BI bi, const lo& o) { b[bi - 1]->u(o); }
   std::vector<std::unique_ptr<B>> b;
 };
 
@@ -103,13 +103,13 @@ typedef TFM LMDM;
 
 static LM<LMDM>* al;
 
-static inline void ral(lt* t, ai a) {
+static inline void ral_FP(lt* t, ai a) {
   ASSERT(t);
   lo o = alo(a);
   al->u(*t, o);
 }
 
-static inline void gal(lt* t, ai a) {
+static inline void gal_FP(lt* t, ai a) {
   ASSERT(t);
   lo o = alo(a);
   if (__infer_nondet_int()) {
@@ -137,6 +137,6 @@ static void am_Good_FP(im* it) {
   const arh* ch = (const arh*)it->gKPC();
   const ai a = aft(ch->i1);
   lt at;
-  gal(&at, a);
-  ral(&at, a);
+  gal_FP(&at, a);
+  ral_FP(&at, a);
 }
diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java
index c734a1cbd..639603e60 100644
--- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java
+++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java
@@ -52,9 +52,7 @@ class UnknownCallsTest {
     for (Character c : input.toCharArray()) {}
   }
 
-  // We can't instantiate loop_over_charArray properly because I don't
-  // know what to do with the symbol for the call to "toCharArray()"
-  private static void call_loop_over_charArray_FN(StringBuilder out, String in) {
+  private static void call_loop_over_charArray(StringBuilder out, String in) {
     loop_over_charArray(out, in);
   }
 }
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 2a2e376fb..70dbbd166 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -122,12 +122,30 @@ codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):
 codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
 codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
 codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
+codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 87 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 91 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 50 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 44 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 38 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 22 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
@@ -138,7 +156,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a`,<RHS trace>,Parameter `b`,Binary operation: (a.length × b.length):signed64]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
@@ -153,6 +171,7 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 13 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ (int JSONArray.length().ub), degree = 1]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ (int JSONArray.length().ub), degree = 1]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_quadratic(org.json.JSONArray):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ (int JSONArray.length().ub)² + 4 ⋅ (1+max(0, int JSONArray.length().ub)), degree = 2]
@@ -161,5 +180,5 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 13 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (int InputStream.read(byte[],int,int).ub + int Math.min(int,int).ub), degree = 1]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (int InputStream.read(byte[],int,int).ub + int Math.min(int,int).ub), degree = 1]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (int Math.min(int,int).ub + int InputStream.read(byte[],int,int).ub), degree = 1]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (int Math.min(int,int).ub + int InputStream.read(byte[],int,int).ub), degree = 1]