From 664978d65415df050c84ad26976f8ebdcb2b29df Mon Sep 17 00:00:00 2001 From: Martino Luca Date: Wed, 21 Nov 2018 05:35:28 -0800 Subject: [PATCH] Revert D12819709 to patch OOM events Reviewed By: mbouaziz, ddino Differential Revision: D13138398 fbshipit-source-id: c9a028c37 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- .../bufferOverrunProofObligations.ml | 66 ++++++++----------- .../bufferOverrunProofObligations.mli | 2 +- .../codetoanalyze/c/bufferoverrun/arith.c | 29 -------- .../c/bufferoverrun/issue_kinds.c | 21 ------ .../codetoanalyze/c/bufferoverrun/issues.exp | 10 +-- .../codetoanalyze/c/bufferoverrun/trivial.c | 8 +-- .../cpp/bufferoverrun/issues.exp | 2 - 8 files changed, 35 insertions(+), 105 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 8c33862c9..bc3a9f9b2 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 9ffeca001..b0d87b2de 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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) = - Option.value_map checked.report_issue_type ~default ~f:(fun issue_type -> + let check ~report cwt = + 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) - else default ) + if propagate then Some {cwt with reported= Some (Reported.make issue_type)} else None + | 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 - | _, None -> - `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 + if ConditionWithTrace.have_similar_bounds existing new_ then + match ConditionWithTrace.xcompare ~lhs:existing ~rhs:new_ with | `LeftSubsumesRight -> `DoNotAddAndStop | `RightSubsumesLeft -> `RemoveExistingAndContinue | `NotComparable -> - `KeepExistingAndContinue ) - | _, _ -> - `KeepExistingAndContinue + `KeepExistingAndContinue + else `KeepExistingAndContinue let join_one condset new_ = - let pp_cond fmt (cond, _) = ConditionWithTrace.pp fmt cond in - let rec aux acc ~same = function + let rec aux ~new_ 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 - new_ pp_cond existing ; + L.(debug BufferOverrun Verbose) + "[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 - existing pp_cond new_ ; - aux acc ~same:false rest + L.(debug BufferOverrun Verbose) + "[InferboPO] Removing condition %a (because of new %a)@." ConditionWithTrace.pp + 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 = - 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 check_all ~report condset = List.filter_map condset ~f:(ConditionWithTrace.check ~report) let pp_summary : F.formatter -> _ t0 -> unit = fun fmt condset -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 9c9812b0b..1f7b64611 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index c473b31ba..18e5a7d03 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index d7a410489..c9d4c606f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/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() { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 97bf94ce9..b420893e0 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/trivial.c, trivial, 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] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c index 3d7ac6c75..cb368f5b7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c +++ b/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); -} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 2192114a9..9bfe5484a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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,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,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]]