[inferbo] Symbols for one value

Summary:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).

As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.

Reviewed By: skcho

Differential Revision: D13072084

fbshipit-source-id: 9bc0b9881

infer/src/bufferoverrun/bounds.ml

@@ -261,8 +261,8 @@ 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
+  let of_path path_of_partial make_symbol ~unsigned partial =
+    let s = make_symbol ~unsigned (path_of_partial partial) in
     of_sym (SymLinear.singleton_one s)
 
 
@@ -826,22 +826,25 @@ module Bound = struct
           NonBottom (f x y)
     in
     fun ~subst_pos x eval_sym ->
-      let get s =
-        match eval_sym s with
+      let get s bound_position =
+        match eval_sym s bound_position with
         | NonBottom x when Symb.Symbol.is_unsigned s ->
             NonBottom (approx_max subst_pos x zero)
         | x ->
             x
       in
       let get_mult_const s coeff =
-        if NonZeroInt.is_one coeff then get s
-        else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg
+        let bound_position =
+          if NonZeroInt.is_positive coeff then subst_pos else Symb.BoundEnd.neg subst_pos
+        in
+        if NonZeroInt.is_one coeff then get s bound_position
+        else if NonZeroInt.is_minus_one coeff then get s bound_position |> lift1 neg
         else
-          match eval_sym s with
+          match eval_sym s bound_position with
           | Bottom -> (
-            (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *)
-            match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
-            | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
+            (* For unsigned symbols, we can over/under-approximate with zero depending on [bound_position]. *)
+            match (Symb.Symbol.is_unsigned s, bound_position) with
+            | true, Symb.BoundEnd.LowerBound ->
                 NonBottom zero
             | _ ->
                 Bottom )
@@ -860,62 +863,65 @@ module Bound = struct
               ~init:(NonBottom (of_big_int c))
               ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
       | MinMax (c, sign, min_max, d, s) -> (
-        match get s with
-        | Bottom ->
-            Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
-                NonBottom (of_big_int i) )
-        | NonBottom x' ->
-            let res =
-              match (sign, min_max, x') with
-              | Plus, Min, MInf | Minus, Max, PInf ->
-                  MInf
-              | Plus, Max, PInf | Minus, Min, MInf ->
-                  PInf
-              | sign, Min, PInf | sign, Max, MInf ->
-                  of_big_int (Sign.eval_big_int sign c d)
-              | _, _, Linear (c2, se) -> (
-                  if SymLinear.is_zero se then
-                    of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
-                  else if SymLinear.is_one_symbol se then
-                    mk_MinMax
-                      ( Sign.eval_big_int sign c c2
-                      , sign
-                      , min_max
-                      , Z.(d - c2)
-                      , SymLinear.get_one_symbol se )
-                  else if SymLinear.is_mone_symbol se then
-                    mk_MinMax
-                      ( Sign.eval_big_int sign c c2
-                      , Sign.neg sign
-                      , MinMax.neg min_max
-                      , Z.(c2 - d)
-                      , SymLinear.get_mone_symbol se )
-                  else
-                    match big_int_of_minmax subst_pos x with
-                    | Some i ->
-                        of_big_int i
-                    | None ->
-                        of_bound_end subst_pos )
-              | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
-                match (min_max, sign2, min_max2) with
-                | Min, Plus, Min | Max, Plus, Max ->
-                    let c' = Sign.eval_big_int sign c c2 in
-                    let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
-                    mk_MinMax (c', sign, min_max, d', s2)
-                | Min, Minus, Max | Max, Minus, Min ->
-                    let c' = Sign.eval_big_int sign c c2 in
-                    let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
-                    mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
-                | _ ->
-                    let bound_end =
-                      match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
-                    in
-                    of_big_int
-                      (Sign.eval_big_int sign c
-                         (MinMax.eval_big_int min_max d
-                            (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
-            in
-            NonBottom res )
+          let bound_position =
+            match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
+          in
+          match get s bound_position with
+          | Bottom ->
+              Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
+                  NonBottom (of_big_int i) )
+          | NonBottom x' ->
+              let res =
+                match (sign, min_max, x') with
+                | Plus, Min, MInf | Minus, Max, PInf ->
+                    MInf
+                | Plus, Max, PInf | Minus, Min, MInf ->
+                    PInf
+                | sign, Min, PInf | sign, Max, MInf ->
+                    of_big_int (Sign.eval_big_int sign c d)
+                | _, _, Linear (c2, se) -> (
+                    if SymLinear.is_zero se then
+                      of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
+                    else if SymLinear.is_one_symbol se then
+                      mk_MinMax
+                        ( Sign.eval_big_int sign c c2
+                        , sign
+                        , min_max
+                        , Z.(d - c2)
+                        , SymLinear.get_one_symbol se )
+                    else if SymLinear.is_mone_symbol se then
+                      mk_MinMax
+                        ( Sign.eval_big_int sign c c2
+                        , Sign.neg sign
+                        , MinMax.neg min_max
+                        , Z.(c2 - d)
+                        , SymLinear.get_mone_symbol se )
+                    else
+                      match big_int_of_minmax subst_pos x with
+                      | Some i ->
+                          of_big_int i
+                      | None ->
+                          of_bound_end subst_pos )
+                | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
+                  match (min_max, sign2, min_max2) with
+                  | Min, Plus, Min | Max, Plus, Max ->
+                      let c' = Sign.eval_big_int sign c c2 in
+                      let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
+                      mk_MinMax (c', sign, min_max, d', s2)
+                  | Min, Minus, Max | Max, Minus, Min ->
+                      let c' = Sign.eval_big_int sign c c2 in
+                      let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
+                      mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
+                  | _ ->
+                      let bound_end =
+                        match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
+                      in
+                      of_big_int
+                        (Sign.eval_big_int sign c
+                           (MinMax.eval_big_int min_max d
+                              (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
+              in
+              NonBottom res )
 
 
   let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym

infer/src/bufferoverrun/bounds.mli

@@ -43,11 +43,17 @@ module Bound : sig
 
   val _255 : t
 
-  val of_normal_path : Symb.BoundEnd.t -> unsigned:bool -> Symb.SymbolPath.partial -> t
+  val of_normal_path :
+       (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t)
+    -> unsigned:bool
+    -> Symb.SymbolPath.partial
+    -> t
 
-  val of_offset_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
+  val of_offset_path :
+    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
-  val of_length_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
+  val of_length_path :
+    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
   val is_symbolic : t -> bool
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -392,10 +392,11 @@ let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
     let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in
     ParamBindings.make formals actuals
   in
-  let eval_sym s =
+  let eval_sym s bound_end =
     let sympath = Symb.Symbol.path s in
     let itv, _ = eval_sympath params sympath caller_mem in
-    Itv.get_bound itv (Symb.Symbol.bound_end s)
+    Symb.Symbol.assert_bound_end s bound_end ;
+    Itv.get_bound itv bound_end
   in
   let trace_of_sym s =
     let sympath = Symb.Symbol.path s in

infer/src/bufferoverrun/itv.ml

@@ -411,9 +411,13 @@ module ItvPure = struct
 
 
   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)
+    if Symb.SymbolPath.represents_multiple_values_sound path then
+      let lb = bound_of_path (Symb.Symbol.make_boundend Symb.BoundEnd.LowerBound) path in
+      let ub = bound_of_path (Symb.Symbol.make_boundend Symb.BoundEnd.UpperBound) path in
+      (lb, ub)
+    else
+      let b = bound_of_path Symb.Symbol.make_onevalue path in
+      (b, b)
 
 
   let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)

infer/src/bufferoverrun/symb.ml

@@ -10,6 +10,8 @@ module F = Format
 module BoundEnd = struct
   type t = LowerBound | UpperBound [@@deriving compare]
 
+  let equal = [%compare.equal: t]
+
   let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
 
   let to_string = function LowerBound -> "lb" | UpperBound -> "ub"
@@ -92,6 +94,8 @@ module SymbolPath = struct
         F.fprintf fmt "%a.length" pp_partial p
 
 
+  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
+
   let rec represents_multiple_values = function
     (* TODO depending on the result, the call might represent multiple values *)
     | Callsite _ | Pvar _ ->
@@ -105,6 +109,17 @@ module SymbolPath = struct
         represents_multiple_values p
 
 
+  let rec represents_multiple_values_sound = function
+    | Callsite _ ->
+        true
+    | Pvar _ ->
+        false
+    | Deref ((Deref_ArrayIndex | Deref_CPointer), _) ->
+        true
+    | Deref (Deref_JavaPointer, p) | Field (_, p) ->
+        represents_multiple_values_sound p
+
+
   let rec represents_callsite_sound_partial = function
     | Callsite _ ->
         true
@@ -112,9 +127,6 @@ module SymbolPath = struct
         false
     | Deref (_, p) | Field (_, p) ->
         represents_callsite_sound_partial p
-
-
-  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 end
 
 module Symbol = struct
@@ -122,38 +134,67 @@ module Symbol = struct
 
   let compare_extra_bool _ _ = 0
 
-  type t = {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t} [@@deriving compare]
+  type t =
+    | OneValue of {unsigned: extra_bool; path: SymbolPath.t}
+    | BoundEnd of {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 compare s1 s2 =
+    match (s1, s2) with
+    | OneValue _, BoundEnd _ ->
+        -1
+    | BoundEnd _, OneValue _ ->
+        1
+    | OneValue {unsigned= unsigned1}, OneValue {unsigned= unsigned2}
+    | BoundEnd {unsigned= unsigned1}, BoundEnd {unsigned= unsigned2} ->
+        let r = compare s1 s2 in
+        if Int.equal r 0 then assert (Bool.equal unsigned1 unsigned2) ;
+        r
 
 
-  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+  type 'res eval = t -> BoundEnd.t -> 'res AbstractDomain.Types.bottom_lifted
 
   let equal = [%compare.equal: t]
 
-  let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
+  let paths_equal s1 s2 =
+    match (s1, s2) with
+    | OneValue _, BoundEnd _ | BoundEnd _, OneValue _ ->
+        false
+    | OneValue {path= path1}, OneValue {path= path2}
+    | BoundEnd {path= path1}, BoundEnd {path= path2} ->
+        SymbolPath.equal path1 path2
+
+
+  let make_onevalue : unsigned:bool -> SymbolPath.t -> t =
+   fun ~unsigned path -> OneValue {unsigned; path}
+
 
-  let make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t =
-   fun ~unsigned path bound_end -> {unsigned; path; bound_end}
+  let make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t =
+   fun bound_end ~unsigned path -> BoundEnd {unsigned; path; bound_end}
 
 
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
-    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')
+    match s with
+    | OneValue {unsigned; path} | BoundEnd {unsigned; path} ->
+        SymbolPath.pp fmt path ;
+        ( if Config.developer_mode then
+          match s with
+          | BoundEnd {bound_end} ->
+              Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end)
+          | OneValue _ ->
+              () ) ;
+        if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if unsigned then 'u' else 's')
 
 
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
-  let is_unsigned {unsigned} = unsigned
+  let is_unsigned : t -> bool = function OneValue {unsigned} | BoundEnd {unsigned} -> unsigned
 
-  let path {path} = path
+  let path = function OneValue {path} | BoundEnd {path} -> path
 
-  let bound_end {bound_end} = bound_end
+  let assert_bound_end s be =
+    match s with OneValue _ -> () | BoundEnd {bound_end} -> assert (BoundEnd.equal be bound_end)
 end
 
 module SymbolSet = struct

infer/src/bufferoverrun/symb.mli

@@ -54,13 +54,15 @@ module SymbolPath : sig
 
   val represents_multiple_values : partial -> bool
 
+  val represents_multiple_values_sound : partial -> bool
+
   val represents_callsite_sound_partial : partial -> bool
 end
 
 module Symbol : sig
   type t
 
-  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+  type 'res eval = t -> BoundEnd.t -> 'res AbstractDomain.Types.bottom_lifted
 
   val compare : t -> t -> int
 
@@ -74,9 +76,11 @@ module Symbol : sig
 
   val path : t -> SymbolPath.t
 
-  val bound_end : t -> BoundEnd.t
+  val assert_bound_end : t -> BoundEnd.t -> unit
+
+  val make_onevalue : unsigned:bool -> SymbolPath.t -> t
 
-  val make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t
+  val make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t
 end
 
 module SymbolSet : sig

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -38,6 +38,11 @@ void l1_symbolic_overrun_Bad(int i) {
   }
 }
 
+void l1_symbolic_overrun2_Bad(int n) {
+  int a[n];
+  a[n] = 0;
+}
+
 void l1_symbolic_underrun_Bad(int i) {
   int a[10];
   if (i < 0) {
@@ -45,6 +50,22 @@ void l1_symbolic_underrun_Bad(int i) {
   }
 }
 
+int less_than(int i, int n) { return i < n; }
+
+void l1_symbolic_widened_Bad(int n) {
+  int a[n];
+  for (int i = n; less_than(i, 2 * n); i++) {
+    a[i] = 0;
+  }
+}
+
+void l1_symbolic_widened_Good_FP(int n) {
+  int a[n];
+  for (int i = n; less_than(i, n); i++) {
+    a[i] = 0;
+  }
+}
+
 void l2_concrete_overrun_Bad() {
   int a[10];
   a[zero_or_ten(1)] = 0;
@@ -65,9 +86,9 @@ void l2_concrete_no_underrun_Good_FP() {
   a[zero_or_ten(1) - 1] = 0;
 }
 
-void l2_symbolic_overrun_Bad(int n) {
-  int a[n];
-  a[n] = 0;
+void l2_symbolic_overrun_Bad(int* n) {
+  int a[*n];
+  a[*n] = 0;
 }
 
 void l2_symbolic_no_overrun_Good(int n) {
@@ -97,8 +118,6 @@ void l3_concrete_no_underrun_Good_FP() {
   a[zero_or_ten(1) - 1] = 0;
 }
 
-int less_than(int i, int n) { return i < n; }
-
 void l4_widened_overrun_Bad() {
   int a[10];
   for (int i = 0; less_than(i, 11); i++) {
@@ -120,25 +139,30 @@ void l5_external_Warn_Bad() {
   a[unknown_function()] = 0;
 }
 
-void s2_symbolic_widened_Bad(int n) {
-  int a[n];
-  for (int i = n; less_than(i, 2 * n); i++) {
+void s2_symbolic_widened_Bad(int* n) {
+  int a[*n];
+  for (int i = *n; less_than(i, 2 * *n); i++) {
     a[i] = 0;
   }
 }
 
-void s2_symbolic_widened_Good_FP(int n) {
-  int a[n];
-  for (int i = n; less_than(i, n); i++) {
+void s2_symbolic_widened_Good_FP(int* n) {
+  int a[*n];
+  for (int i = *n; less_than(i, *n); i++) {
     a[i] = 0;
   }
 }
 
 // Do not report as it was already reported in the callee with the same issue
 // type
-void call_s2_symbolic_widened_Silenced(int m) { s2_symbolic_widened_Bad(m); }
+void FP_call_s2_symbolic_widened_Silenced(int* m) {
+  s2_symbolic_widened_Bad(m);
+}
 
-void l1_call_to_s2_symbolic_widened_Bad() { s2_symbolic_widened_Bad(1); }
+void l1_call_to_s2_symbolic_widened_Bad() {
+  int x = 1;
+  s2_symbolic_widened_Bad(&x);
+}
 
 void may_underrun_symbolic_Nowarn_Good(int n) {
   int a[n];

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -57,7 +57,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Bad, 3, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 15] Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Good_FP, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
-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_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: 3⋅len + 1 Size: 3⋅len + 1]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `y.f[*]`,<Length trace>,Array declaration,Array access: Offset: [min(20, y.f[*]), max(20, y.f[*])] 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_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
@@ -100,7 +100,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_call_access_index_4_on_S3_Ba
 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, [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/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, 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]
@@ -132,21 +132,24 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Ba
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `*n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun2_Bad, 2, BUFFER_OVERRUN_L1, 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, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [max(10, i), i] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 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_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: [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, 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]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 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]]
@@ -156,13 +159,12 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, B
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-19+min(0, x), -1] Size: 1]
 codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: unknown,Assignment,Call,<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset added: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 255] Size: 255]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 256] Size: 256]
@@ -197,19 +199,22 @@ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label,
 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_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, call_pointer_arith4_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,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_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5]
 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_call_prune_arrblk_eq_Ok, 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_eq_CAF` ]
 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_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ]
-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, 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_CAT` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-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, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [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]
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_exp2_CAF, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_exp_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_ge_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_gt_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -97,19 +97,19 @@ void memcpy_good4() {
   memcpy(dst, src, sizeof(dst));
 }
 
-void memcpy_len(size_t len) {
+void memcpy_len_Good(size_t len) {
   char dst[len];
   char src[len];
   memcpy(dst, src, len);
 }
 
-void call_memcpy_len1_Good() { memcpy_len(40); }
+void call_memcpy_len1_Good() { memcpy_len_Good(40); }
 
 extern size_t unknown_uint();
 
-void call_memcpy_len2_Good_FP() {
+void call_memcpy_len2_Good() {
   size_t x = unknown();
-  memcpy_len(x);
+  memcpy_len_Good(x);
 }
 
 void memmove_bad1() {

infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c

@@ -36,17 +36,26 @@ void call_pointer_arith3_Bad() {
   pointer_arith3(p, 100);
 }
 
+void pointer_arith4_Bad(int x) {
+  int len = 5;
+  char p[5];
+  (p + x)[10 - x] = 0;
+}
+
 /* It is better to raise an alarm here, rather than returning a safety
    condition, since the buffer overrun occurs always without regard to
    the input x.  Using symbols for variables, not only for bounds,
    would help in this case. */
-void FN_pointer_arith4_Bad(int x) {
+void FN_pointer_arith4_Bad(int* x) {
   int len = 5;
   char p[5];
-  (p + x)[10 - x] = 0;
+  (p + *x)[10 - *x] = 0;
 }
 
-void call_pointer_arith4_Bad() { FN_pointer_arith4_Bad(100); }
+void call_pointer_arith4_Bad() {
+  int x = 100;
+  FN_pointer_arith4_Bad(&x);
+}
 
 #include <stdio.h>
 #include <stdlib.h>

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -98,45 +98,53 @@ void prune_alias_exp_Ok(int x) {
   }
 }
 
-void FP_prune_alias_exp_Ok(int x) {
+void prune_alias_exp2_CAF(int x) {
   int a[1];
 
-  if (x + 1 != 1 + x) {
+  if (x + 1 != 1 + x) { // Condition always false
+    a[1] = 0;
+  }
+}
+
+void FP_prune_alias_exp_Ok(int* x) {
+  int a[1];
+
+  if (*x + 1 != 1 + *x) {
     a[1] = 0;
   }
 }
 
 #include <stdlib.h>
 
-void prune_arrblk_ne(int* x) {
+void prune_arrblk_ne_CAT(int* x) {
   int* y = x + 10;
 
-  if (x != y) {
+  if (x != y) { // always true
     x[5] = 1;
   }
 }
 
 void call_prune_arrblk_ne_Ok() {
   int* x = (int*)malloc(sizeof(int) * 10);
-  prune_arrblk_ne(x);
+  prune_arrblk_ne_CAT(x);
 }
 
 void call_prune_arrblk_ne_Bad() {
   int* x = (int*)malloc(sizeof(int) * 5);
-  prune_arrblk_ne(x);
+  prune_arrblk_ne_CAT(x);
 }
 
-void prune_arrblk_eq(int* x) {
+void prune_arrblk_eq_CAF(int* x) {
   int* y = x + 10;
 
-  if (x == y) {
+  if (x == y) { // always false
     x[5] = 1; /* unreachable */
   }
 }
 
-void call_prune_arrblk_eq_Ok() {
+void FP_call_prune_arrblk_eq_Ok() {
   int* x = (int*)malloc(sizeof(int) * 5);
-  prune_arrblk_eq(x);
+  prune_arrblk_eq_CAF(x);
 }
 
 void prune_minmax1_Ok(unsigned int x, unsigned int y) {

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -1,17 +1,17 @@
-codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
+codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -32,10 +32,10 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3532, degree = 0]
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
@@ -47,13 +47,13 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1209, degree = 0]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), degree = 1]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m.lb + 20), degree = 1]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m.lb + 20), degree = 1]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 ⋅ (-m.lb + 20), degree = 1]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 ⋅ (-m + 20), degree = 1]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
@@ -115,26 +115,26 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 551, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 553, degree = 0]
 codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16007, degree = 0]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m - 1) × m + 8 ⋅ m + 2 ⋅ m × (max(1, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m - 1) × m + 8 ⋅ m + 2 ⋅ m × (max(1, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m + 6 ⋅ m² + 2 ⋅ m × (1+max(0, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m + 6 ⋅ m² + 2 ⋅ m × (1+max(0, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
 codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004, degree = 0]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004, degree = 0]
@@ -160,9 +160,9 @@ codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIM
 codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
 codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
 codetoanalyze/c/performance/loops.c, larger_state_FN, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
-codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 4 ⋅ x.ub + 2 ⋅ (1+max(0, x.ub)), degree = 1]
-codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x.ub + 2 ⋅ (1+max(0, x.ub)), degree = 1]
-codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x.ub + 2 ⋅ (1+max(0, x.ub)), degree = 1]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1]
 codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
 codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
 codetoanalyze/c/performance/purity.c, loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
@@ -176,15 +176,15 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUT
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 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, 4, 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, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, 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, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-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 ⋅ 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]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+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 + 2 ⋅ (1+max(0, m)), 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 + 2 ⋅ (1+max(0, m)), 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 + 2 ⋅ (1+max(0, m)), 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 + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), 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 + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), 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 + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), degree = 1]

infer/tests/codetoanalyze/java/bufferoverrun/issues.exp

@@ -1,2 +1,2 @@
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
-codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy.ub - 1] × d.cci[*].s):signed32]
+codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -1,9 +1,9 @@
 codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [2, 8] Size: 8]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 ⋅ length.ub, degree = 1]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length.ub, degree = 1]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ mag.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ mag.length.ub, degree = 1]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length, degree = 1]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 ⋅ length, degree = 1]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length, degree = 1]
+codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ mag.length, degree = 1]
+codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ mag.length, degree = 1]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
@@ -25,49 +25,49 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length.ub × log(list.length.ub), degree = 1 + 1⋅log]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 ⋅ (list1.length.ub - 1) + 4 ⋅ list1.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 13 ⋅ (list1.length.ub - 1) + 4 ⋅ list1.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length.ub × log(list.length.ub), degree = 1 + 1⋅log]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p.ub, degree = 1]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 ⋅ p.ub, degree = 1]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p.ub, degree = 1]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.ensure_call(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (list.length.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (list.length.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size.ub + 5 ⋅ size.ub × list.length.ub, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 17 ⋅ size.ub + 5 ⋅ size.ub × list.length.ub, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 ⋅ (list1.length - 1) + 4 ⋅ list1.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 13 ⋅ (list1.length - 1) + 4 ⋅ list1.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, degree = 1]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 ⋅ p, degree = 1]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), degree = 2]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), degree = 2]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), degree = 2]
+codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), degree = 2]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.ensure_call(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (list.length - 1) + 5 ⋅ (list.length - 1) × list.length + 4 ⋅ list.length, degree = 2]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (list.length - 1) + 5 ⋅ (list.length - 1) × list.length + 4 ⋅ list.length, degree = 2]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 17 ⋅ size + 5 ⋅ size × list.length, degree = 2]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size + 5 ⋅ size × list.length, degree = 2]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 10 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 10 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 10 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 10 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
+codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -79,8 +79,8 @@ codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Con
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
-codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k.ub, degree = 1]
-codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 13 ⋅ k.ub, degree = 1]
+codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 13 ⋅ k, degree = 1]
+codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, degree = 1]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202, degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1203, degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0]
@@ -115,24 +115,24 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0]
 codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ test.a.ub, degree = 1]
-codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a.ub, degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1]
+codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, degree = 1]
+codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ test.a, degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `size`,<RHS trace>,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ (size.ub + 20), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size.ub + 20), degree = 1]
-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/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 4 ⋅ (items.length + 1), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ items.length + 4 ⋅ (items.length + 1), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2]
+codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2]
+codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2]
+codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ (size + 20), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size + 20), 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 - 1) + 4 ⋅ parts.length, degree = 1]
+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 - 1) + 4 ⋅ parts.length, 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 - 1) + 4 ⋅ parts.length, 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 ⋅ 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 ⋅ 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 ⋅ String.toCharArray().length.ub, degree = 1]
@@ -160,22 +160,22 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 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]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 ⋅ (length.ub - 1), degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length.ub - 1), degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length.ub - 1), degree = 1]
-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 4 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-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, 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]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 ⋅ (length - 1), degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length - 1), degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length - 1), degree = 1]
+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 4 + 71 ⋅ (length - 1)² + 8 ⋅ length, degree = 2]
+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 - 1)² + 8 ⋅ length, 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 - 1)² + 8 ⋅ length, 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 - 1)² + 8 ⋅ length, degree = 2]
+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 - 1)² + 8 ⋅ length, 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 - 1)² + 8 ⋅ length, 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 - 1)² + 8 ⋅ length, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length, degree = 1]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, 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, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]