From 9e9deb93bef8ba473180c0154dfe5c6663685ade Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 1 Nov 2018 20:07:56 -0700 Subject: [PATCH] [inferbo] Use set instead of list on get_symbols Reviewed By: mbouaziz Differential Revision: D12855522 fbshipit-source-id: 4e916654c --- infer/src/bufferoverrun/arrayBlk.ml | 9 +++---- infer/src/bufferoverrun/bounds.ml | 10 ++++---- infer/src/bufferoverrun/bounds.mli | 2 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 10 ++++---- .../bufferOverrunProofObligations.ml | 12 ++++++---- infer/src/bufferoverrun/itv.ml | 10 ++++---- infer/src/bufferoverrun/itv.mli | 6 ++--- infer/src/bufferoverrun/symb.ml | 6 +++++ infer/src/bufferoverrun/symb.mli | 6 +++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 +- .../cpp/bufferoverrun/issues.exp | 24 +++++++++---------- 11 files changed, 56 insertions(+), 41 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 55e57ec10..deeb79db5 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -65,12 +65,12 @@ module ArrInfo = struct fun fmt arr -> Format.fprintf fmt "offset : %a, size : %a" Itv.pp arr.offset Itv.pp arr.size - let get_symbols : t -> Itv.Symbol.t list = + let get_symbols : t -> Itv.SymbolSet.t = fun arr -> let s1 = Itv.get_symbols arr.offset in let s2 = Itv.get_symbols arr.size in let s3 = Itv.get_symbols arr.stride in - List.concat [s1; s2; s3] + Itv.SymbolSet.union3 s1 s2 s3 let normalize : t -> t = @@ -145,8 +145,9 @@ let subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate = fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a -let get_symbols : astate -> Itv.Symbol.t list = - fun a -> List.concat_map ~f:(fun (_, ai) -> ArrInfo.get_symbols ai) (bindings a) +let get_symbols : astate -> Itv.SymbolSet.t = + fun a -> + fold (fun _ ai acc -> Itv.SymbolSet.union acc (ArrInfo.get_symbols ai)) a Itv.SymbolSet.empty let normalize : astate -> astate = fun a -> map ArrInfo.normalize a diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index e5bdfd71f..92f2747d2 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -139,8 +139,8 @@ module SymLinear = struct Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s') - let get_symbols : t -> Symb.Symbol.t list = - fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x [] + let get_symbols : t -> Symb.SymbolSet.t = + fun x -> M.fold (fun symbol _coeff acc -> Symb.SymbolSet.add symbol acc) x Symb.SymbolSet.empty (* we can give integer bounds (obviously 0) only when all symbols are unsigned *) @@ -773,13 +773,13 @@ module Bound = struct let div_const_u = div_const Symb.BoundEnd.UpperBound - let get_symbols : t -> Symb.Symbol.t list = function + let get_symbols : t -> Symb.SymbolSet.t = function | MInf | PInf -> - [] + Symb.SymbolSet.empty | Linear (_, se) -> SymLinear.get_symbols se | MinMax (_, _, _, _, s) -> - [s] + Symb.SymbolSet.singleton s let are_similar b1 b2 = diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 497709503..610973af3 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -103,7 +103,7 @@ module Bound : sig val div_const_u : t -> Ints.NonZeroInt.t -> t sexp_option - val get_symbols : t -> Symb.Symbol.t list + val get_symbols : t -> Symb.SymbolSet.t val are_similar : t -> t -> bool diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 99102b9f3..1b3aa42ba 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -285,8 +285,8 @@ module Val = struct {bot with itv; traces= TraceSet.join x.traces y.traces} - let get_symbols : t -> Itv.Symbol.t list = - fun x -> List.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk) + let get_symbols : t -> Itv.SymbolSet.t = + fun x -> Itv.SymbolSet.union (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk) let normalize : t -> t = @@ -301,9 +301,9 @@ module Val = struct fun x (eval_sym, trace_of_sym) location -> let symbols = get_symbols x in let traces_caller = - List.fold symbols - ~f:(fun traces symbol -> TraceSet.join (trace_of_sym symbol) traces) - ~init:TraceSet.empty + Itv.SymbolSet.fold + (fun symbol traces -> TraceSet.join (trace_of_sym symbol) traces) + symbols TraceSet.empty in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 61d1b5b51..77b27eb04 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -108,7 +108,8 @@ module ArrayAccessCondition = struct [@@deriving compare] let get_symbols c = - ItvPure.get_symbols c.offset @ ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size + Symb.SymbolSet.union3 (ItvPure.get_symbols c.offset) (ItvPure.get_symbols c.idx) + (ItvPure.get_symbols c.size) let pp : F.formatter -> t -> unit = @@ -325,7 +326,7 @@ module BinaryOperationCondition = struct ; lhs: ItvPure.astate ; rhs: ItvPure.astate } - let get_symbols c = ItvPure.get_symbols c.lhs @ ItvPure.get_symbols c.rhs + let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs) let subst eval_sym c = match (ItvPure.subst c.lhs eval_sym, ItvPure.subst c.rhs eval_sym) with @@ -675,7 +676,7 @@ module ConditionWithTrace = struct let subst (eval_sym, trace_of_sym) rel_map caller_relation callee_pname call_site cwt = let symbols = Condition.get_symbols cwt.cond in - if List.is_empty symbols then + if Symb.SymbolSet.is_empty symbols then L.(die InternalError) "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \ the first place?" @@ -685,8 +686,9 @@ module ConditionWithTrace = struct None | Some cond -> let traces_caller = - List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> - ValTraceSet.join (trace_of_sym symbol) val_traces ) + Symb.SymbolSet.fold + (fun symbol val_traces -> ValTraceSet.join (trace_of_sym symbol) val_traces) + symbols ValTraceSet.empty in let trace = ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index d738ace87..3a3fa7cdd 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -29,9 +29,9 @@ module Boolean = struct end open Ints -module Symbol = Symb.Symbol module SymbolPath = Symb.SymbolPath module SymbolTable = Symb.SymbolTable +module SymbolSet = Symb.SymbolSet (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) module NonNegativeBound = struct @@ -797,8 +797,8 @@ module ItvPure = struct if is_invalid (l, u) then NonBottom x else if Bound.eq l u then prune_diff x l else NonBottom x - let get_symbols : t -> Symbol.t list = - fun (l, u) -> List.append (Bound.get_symbols l) (Bound.get_symbols u) + let get_symbols : t -> SymbolSet.t = + fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u) let make_positive : t -> t = @@ -978,9 +978,9 @@ let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t = fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x -let get_symbols : t -> Symbol.t list = function +let get_symbols : t -> SymbolSet.t = function | Bottom -> - [] + SymbolSet.empty | NonBottom x -> ItvPure.get_symbols x diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index ecb697e3e..a0227dcca 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -25,9 +25,9 @@ module Boolean : sig val is_true : t -> bool end -module Symbol = Symb.Symbol module SymbolPath = Symb.SymbolPath module SymbolTable = Symb.SymbolTable +module SymbolSet = Symb.SymbolSet module NonNegativePolynomial : sig include AbstractDomain.WithTop @@ -134,7 +134,7 @@ module ItvPure : sig | `LeftSubsumesRight | `RightSubsumesLeft ] - val get_symbols : t -> Symbol.t list + val get_symbols : t -> SymbolSet.t val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted @@ -197,7 +197,7 @@ val neg : t -> t val normalize : t -> t -val get_symbols : t -> Symbol.t list +val get_symbols : t -> SymbolSet.t val eq : t -> t -> bool diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 444e7450c..291c2f50a 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -106,6 +106,12 @@ module SymbolTable = struct s end +module SymbolSet = struct + include PrettyPrintable.MakePPSet (Symbol) + + let union3 x y z = union (union x y) z +end + module SymbolMap = struct include PrettyPrintable.MakePPMap (Symbol) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 64201dac6..1b9bb9a1d 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -53,6 +53,12 @@ module Symbol : sig val bound_end : t -> BoundEnd.t end +module SymbolSet : sig + include PrettyPrintable.PPSet with type elt = Symbol.t + + val union3 : t -> t -> t -> t +end + module SymbolMap : sig include PrettyPrintable.PPMap with type key = Symbol.t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b21746e62..3a6b12075 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -57,7 +57,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: 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,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ] codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 16db13400..174ca3722 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -20,7 +20,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] @@ -43,12 +43,12 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Binop: ([-oo, +oo] - 1):signed32] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903] @@ -61,10 +61,10 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERR codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64] 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,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned64] @@ -74,11 +74,11 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVER codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,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,Call,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,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0] +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,Call,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Parameter: count,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Parameter: count,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []