Revert D12819709 to patch OOM events

Reviewed By: mbouaziz, ddino

Differential Revision: D13138398

fbshipit-source-id: c9a028c37

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -671,7 +671,7 @@ module Report = struct
                 let callee_pdesc = Summary.get_proc_desc callee_summary in
                 instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_payload
                   location
-                |> PO.ConditionSet.merge cond_set
+                |> PO.ConditionSet.join cond_set
             | None ->
                 (* no inferbo payload *) cond_set )
           | None ->

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -709,7 +709,7 @@ module ConditionWithTrace = struct
     else issue_type
 
 
-  let check cwt =
+  let check_aux cwt =
     let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond in
     match report_issue_type with
     | None ->
@@ -729,11 +729,14 @@ module ConditionWithTrace = struct
         {report_issue_type; propagate}
 
 
-  let report ~report ((cwt, checked) as default) =
+  let check ~report cwt =
-    Option.value_map checked.report_issue_type ~default ~f:(fun issue_type ->
+    let {report_issue_type; propagate} = check_aux cwt in
+    match report_issue_type with
+    | Some issue_type ->
         report cwt.cond cwt.trace issue_type ;
-        if checked.propagate then ({cwt with reported= Some (Reported.make issue_type)}, checked)
+        if propagate then Some {cwt with reported= Some (Reported.make issue_type)} else None
-        else default )
+    | None ->
+        Option.some_if propagate cwt
 
 
   let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
@@ -753,54 +756,48 @@ module ConditionSet = struct
 
   let empty = []
 
-  let try_merge ~existing:(existing_cwt, existing_checked) ~new_:(new_cwt, new_checked) =
+  let try_merge ~existing ~new_ =
     (* we don't want to remove issues that would end up in a higher bucket,
      e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
-    match (existing_checked.report_issue_type, new_checked.report_issue_type) with
+    if ConditionWithTrace.have_similar_bounds existing new_ then
-    | _, None ->
+      match ConditionWithTrace.xcompare ~lhs:existing ~rhs:new_ with
-        `AddAndStop
-    | Some existing_issue_type, Some new_issue_type
-      when IssueType.equal existing_issue_type new_issue_type
-           && ConditionWithTrace.have_similar_bounds existing_cwt new_cwt -> (
-      match ConditionWithTrace.xcompare ~lhs:existing_cwt ~rhs:new_cwt with
       | `LeftSubsumesRight ->
           `DoNotAddAndStop
       | `RightSubsumesLeft ->
           `RemoveExistingAndContinue
       | `NotComparable ->
-          `KeepExistingAndContinue )
-    | _, _ ->
           `KeepExistingAndContinue
+    else `KeepExistingAndContinue
 
 
   let join_one condset new_ =
-    let pp_cond fmt (cond, _) = ConditionWithTrace.pp fmt cond in
+    let rec aux ~new_ acc ~same = function
-    let rec aux acc ~same = function
       | [] ->
           if Config.bo_debug >= 3 then
-            L.d_printfln "[InferboPO] Adding new condition %a@." pp_cond new_ ;
+            L.(debug BufferOverrun Verbose)
+              "[InferboPO] Adding new condition %a@." ConditionWithTrace.pp new_ ;
           if same then new_ :: condset else new_ :: acc
       | existing :: rest as existings -> (
         match try_merge ~existing ~new_ with
-        | `AddAndStop ->
-            new_ :: (if same then condset else List.rev_append acc existings)
         | `DoNotAddAndStop ->
             if Config.bo_debug >= 3 then
-              L.d_printfln "[InferboPO] Not adding condition %a (because of existing %a)@." pp_cond
+              L.(debug BufferOverrun Verbose)
-                new_ pp_cond existing ;
+                "[InferboPO] Not adding condition %a (because of existing %a)@."
+                ConditionWithTrace.pp new_ ConditionWithTrace.pp existing ;
             if same then condset else List.rev_append acc existings
         | `RemoveExistingAndContinue ->
             if Config.bo_debug >= 3 then
-              L.d_printfln "[InferboPO] Removing condition %a (because of new %a)@." pp_cond
+              L.(debug BufferOverrun Verbose)
-                existing pp_cond new_ ;
+                "[InferboPO] Removing condition %a (because of new %a)@." ConditionWithTrace.pp
-            aux acc ~same:false rest
+                existing ConditionWithTrace.pp new_ ;
+            aux ~new_ acc ~same:false rest
         | `KeepExistingAndContinue ->
-            aux (existing :: acc) ~same rest )
+            aux ~new_ (existing :: acc) ~same rest )
     in
-    aux [] ~same:true condset
+    aux ~new_ [] ~same:true condset
 
 
-  let merge condset1 condset2 = List.rev_append condset1 condset2
+  let join condset1 condset2 = List.fold_left ~f:join_one condset1 ~init:condset2
 
   let add_opt location val_traces condset = function
     | None ->
@@ -808,7 +805,7 @@ module ConditionSet = struct
     | Some cond ->
         let trace = ConditionTrace.make location val_traces in
         let cwt = ConditionWithTrace.make cond trace in
-        cwt :: condset
+        join [cwt] condset
 
 
   let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp
@@ -839,17 +836,12 @@ module ConditionSet = struct
       | None ->
           condset
       | Some cwt ->
-          cwt :: condset
+          join_one condset cwt
     in
     List.fold condset ~f:subst_add_cwt ~init:[]
 
 
-  let check_all ~report condset =
+  let check_all ~report condset = List.filter_map condset ~f:(ConditionWithTrace.check ~report)
-    List.map condset ~f:(fun cwt -> (cwt, ConditionWithTrace.check cwt))
-    |> List.fold ~init:[] ~f:join_one
-    |> List.map ~f:(ConditionWithTrace.report ~report)
-    |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt)
-
 
   let pp_summary : F.formatter -> _ t0 -> unit =
    fun fmt condset ->

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -59,7 +59,7 @@ module ConditionSet : sig
     -> t
     -> t
 
-  val merge : t -> t -> t
+  val join : t -> t -> t
 
   val subst :
        summary_t

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -335,35 +335,6 @@ void minmax_div_const2_Bad_FN() {
   div_const2(-2);
 }
 
-uint32_t unknown_nat() {
-  uint32_t x = unknown_function();
-  if (x >= 0) {
-    return x;
-  } else {
-    return 0;
-  }
-}
-
-void two_safety_conditions2_Bad(uint32_t s) {
-  uint32_t x = unknown_nat();
-  uint32_t y, z;
-
-  if (unknown_function()) {
-    y = 0;
-  } else {
-    y = 80;
-  }
-  z = x + y; // integer overflow L5: [0, +oo] + [0, 80]
-
-  if (s >= 10 && s <= 20) {
-    z = x + s; // [0, +oo] + [max(10, s.lb), min(20, s.ub)]
-  }
-}
-
-void call_two_safety_conditions2_Bad() {
-  two_safety_conditions2_Bad(15); // integer overflow L5: [0, +oo] + 15
-}
-
 void band_positive_constant_Good() {
   char a[3];
   int x = 6 & 2; // y is 2

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

@@ -242,27 +242,6 @@ void False_Issue_Type_l3_unknown_function_Bad() {
   }
 }
 
-int mone_to_one() {
-  int x = unknown_function();
-  if (x >= -1 && x <= 1) {
-    return x;
-  } else {
-    return 0;
-  }
-}
-
-void two_safety_conditions(int n) {
-  char a[10];
-  int y = mone_to_one();
-  if (unknown_function()) {
-    a[n] = 0; // should be L1 when n=10
-  } else {
-    a[n + y] = 0; // should be L2 when n=10
-  }
-}
-
-void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); }
-
 /* issue1 and issue2 are deduplicated since the offset of issue2
    ([10,+oo]) subsumes that of issue1 ([10,10]). */
 void deduplicate_issues_Bad() {

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

@@ -1,9 +1,9 @@
 codetoanalyze/c/bufferoverrun/arith.c, band_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,Assignment,Assignment,ArrayAccess: Offset: [0, 2] Size: 2]
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
-codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 8] Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_nat,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, band_positive_Good, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_nat,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 9]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
-codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
@@ -26,7 +26,6 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binop: (85 * 4294967295):unsigned32]
-codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 80]):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@@ -95,8 +94,6 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Binop: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: 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,ArrayDeclaration,Parameter: n,ArrayAccess: 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, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: 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, [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,Parameter: n,Assignment,Binop: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
@@ -194,8 +191,7 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0]
-codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0]
+codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
-codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/trivial.c

@@ -7,13 +7,7 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-void trivial_Bad() {
+void trivial() {
   int a[10];
   a[10] = 0; /* BUG */
 }
-
-void malloc_zero_Bad() {
-  char* x;
-  x = malloc(0);
-  x = malloc(1);
-}

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

@@ -44,7 +44,6 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFE
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,Assignment,Return,Assignment,ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: [0, 6]]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 12]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params2` ]
@@ -79,7 +78,6 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([3, +oo] + 42):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [45, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]]