diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index fb347a6d4..f7370bf65 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -92,7 +92,7 @@ module ArrInfo = struct fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset} - let set_size : Itv.t -> t -> t = fun size arr -> {arr with size} + let set_length : Itv.t -> t -> t = fun size arr -> {arr with size} (* Set new stride only when the previous stride is a constant interval. *) let set_stride : Z.t -> t -> t = @@ -181,6 +181,6 @@ let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2 -let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a +let set_length : Itv.t -> astate -> astate = fun length a -> map (ArrInfo.set_length length) a let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index c75f7b99c..0a1b4c27f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -184,9 +184,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct BoUtils.Exec.load_val id (Sem.eval integer_type_widths exp mem) mem | Store (exp1, _, exp2, location) -> let locs = Sem.eval integer_type_widths exp1 mem |> Dom.Val.get_all_locs in - let v = - Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) - in + let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location in let mem = let sym_exps = Dom.Relation.SymExp.of_exps diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9bcf3de17..216659b5e 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -130,8 +130,6 @@ module Val = struct let get_traces : t -> TraceSet.t = fun x -> x.traces - let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces} - let of_itv ?(traces = TraceSet.empty) itv = {bot with itv; traces} let of_int n = of_itv (Itv.of_int n) @@ -140,15 +138,17 @@ module Val = struct let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x} - let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} + let of_pow_loc ~traces powloc = {bot with powloc; traces} - let of_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> t = - fun allocsite ~stride ~offset ~size -> + let of_array_alloc : + Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> traces:TraceSet.t -> t = + fun allocsite ~stride ~offset ~size ~traces -> let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in { bot with arrayblk= ArrayBlk.make allocsite ~offset ~size ~stride ; offset_sym= Relation.Sym.of_allocsite_offset allocsite - ; size_sym= Relation.Sym.of_allocsite_size allocsite } + ; size_sym= Relation.Sym.of_allocsite_size allocsite + ; traces } let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} @@ -177,8 +177,9 @@ module Val = struct let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top} - let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = - fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces} + let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = + fun f ?(f_trace = TraceSet.join) x y -> + {bot with itv= f x.itv y.itv; traces= f_trace x.traces y.traces} let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk) @@ -190,23 +191,23 @@ module Val = struct {bot with itv; traces= TraceSet.join x.traces y.traces} - let plus_a : t -> t -> t = lift_itv Itv.plus + let plus_a = lift_itv Itv.plus - let minus_a : t -> t -> t = lift_itv Itv.minus + let minus_a = lift_itv Itv.minus let get_iterator_itv : t -> t = fun i -> {bot with itv= Itv.get_iterator_itv i.itv} - let mult : t -> t -> t = lift_itv Itv.mult + let mult = lift_itv Itv.mult - let div : t -> t -> t = lift_itv Itv.div + let div = lift_itv Itv.div - let mod_sem : t -> t -> t = lift_itv Itv.mod_sem + let mod_sem = lift_itv Itv.mod_sem - let shiftlt : t -> t -> t = lift_itv Itv.shiftlt + let shiftlt = lift_itv Itv.shiftlt - let shiftrt : t -> t -> t = lift_itv Itv.shiftrt + let shiftrt = lift_itv Itv.shiftrt - let band_sem : t -> t -> t = lift_itv Itv.band_sem + let band_sem = lift_itv Itv.band_sem let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem @@ -302,7 +303,7 @@ module Val = struct (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 + let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} (* normalize bottom *) |> normalize @@ -314,8 +315,13 @@ module Val = struct {x with traces} - let set_array_size : Itv.t -> t -> t = - fun size v -> {v with arrayblk= ArrayBlk.set_size size v.arrayblk} + let add_assign_trace_elem location x = add_trace_elem (Trace.Assign location) x + + let set_array_length : Location.t -> length:t -> t -> t = + fun location ~length v -> + { v with + arrayblk= ArrayBlk.set_length length.itv v.arrayblk + ; traces= TraceSet.add_elem (Trace.ArrDecl location) length.traces } let set_array_stride : Z.t -> t -> t = @@ -332,6 +338,8 @@ module Val = struct let one = of_itv Itv.one + let pos = of_itv Itv.pos + let top = of_itv Itv.top let zero = of_itv Itv.zero diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 0ed5680fd..2e755aa16 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -118,7 +118,7 @@ let malloc size_exp = let size_exp = Option.value dyn_length ~default:length0 in Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp in - let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in + let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt @@ -159,16 +159,13 @@ let realloc src_exp size_exp = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, _, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval integer_type_widths length0 mem in - let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let v = - Sem.eval integer_type_widths src_exp mem - |> Dom.Val.set_array_size (Dom.Val.get_itv length) - |> Dom.Val.set_traces traces + Sem.eval integer_type_widths src_exp mem |> Dom.Val.set_array_length location ~length in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in - BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) + BoUtils.Exec.set_dyn_length location tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) and check = check_alloc_size size_exp in {exec; check} @@ -211,10 +208,10 @@ let inferbo_min e1 e2 = let inferbo_set_size e1 e2 = - let exec {integer_type_widths} ~ret:_ mem = + let exec {integer_type_widths; location} ~ret:_ mem = let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in - let size = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in - Dom.Mem.transform_mem ~f:(Dom.Val.set_array_size size) locs mem + let length = Sem.eval integer_type_widths e2 mem in + Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem and check = check_alloc_size e2 in {exec; check} @@ -256,11 +253,13 @@ let set_array_length array length_exp = let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = match array with | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> - let length = Sem.eval integer_type_widths length_exp mem |> Dom.Val.get_itv in + let length = Sem.eval integer_type_widths length_exp mem in let stride = Option.map ~f:IntLit.to_int_exn stride in let path = Some (Symb.SymbolPath.of_pvar array_pvar) in let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in - let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size:length in + let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let size = Dom.Val.get_itv length in + let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v |> set_uninitialized location elt (Dom.Val.get_array_locs v) @@ -272,9 +271,7 @@ let set_array_length array length_exp = module Split = struct let std_vector integer_type_widths ~adds_at_least_one (vector_exp, vector_typ) location mem = - let traces = BufferOverrunTrace.(Set.singleton (Call location)) in - let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in - let increment = Dom.Val.of_itv ~traces increment_itv in + let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in let vector_size_locs = @@ -282,7 +279,8 @@ module Split = struct |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field in - Dom.Mem.transform_mem ~f:(Dom.Val.plus_a increment) vector_size_locs mem + let f_trace _ traces = TraceSet.add_elem (Trace.Return location) traces in + Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem end module Boost = struct @@ -402,7 +400,7 @@ module Collection = struct let alloc_loc = Loc.of_allocsite allocsite in let init_size = Dom.Val.of_int 0 in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces init_size) in - let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.set_traces traces in + let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces in mem |> Dom.Mem.add_stack loc v |> Dom.Mem.add_heap alloc_loc init_size in {exec; check= no_check} diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index b0d87b2de..1458da44f 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -625,9 +625,7 @@ module ConditionTrace = struct let make_call_and_subst ~traces_caller ~callee_pname call_site ct = - let val_traces = - ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces call_site - in + let val_traces = ValTraceSet.call call_site ~traces_caller ~traces_callee:ct.val_traces in {ct with cond_trace= Inter {callee_pname; call_site}; val_traces} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 4b4f80168..050175578 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -160,8 +160,9 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = let v = eval integer_type_widths e mem in set_array_stride integer_type_widths t v | Exp.Lfield (e, fn, _) -> - eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn - |> Val.of_pow_loc + let v = eval integer_type_widths e mem in + let locs = Val.get_all_locs v |> PowLoc.append_field ~fn in + Val.of_pow_loc locs ~traces:(Val.get_traces v) | Exp.Lindex (e1, e2) -> eval_lindex integer_type_widths e1 e2 mem | Exp.Sizeof {nbytes= Some size} -> @@ -187,7 +188,7 @@ and eval_lindex integer_type_widths array_exp index_exp mem = x.f[n] in the concrete semantics. *) Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v | _ -> - Val.of_pow_loc PowLoc.unknown + Val.of_pow_loc PowLoc.unknown ~traces:TraceSet.empty else match array_exp with | Exp.Lindex _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index eab083e27..cd65e9ced 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -91,7 +91,7 @@ module Set = struct let add_elem elem t = if is_empty t then singleton elem else map (BoTrace.add_elem elem) t - let instantiate ~traces_caller ~traces_callee location = + let call location ~traces_caller ~traces_callee = if is_empty traces_caller then map (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call location) trace_callee) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 335256a08..a67f92c57 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -69,8 +69,8 @@ module Exec = struct let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in let mem = let arr = - Dom.Val.of_array_alloc allocsite ~stride ~offset ~size - |> Dom.Val.add_trace_elem (Trace.ArrDecl location) + let traces = TraceSet.singleton (Trace.ArrDecl location) in + Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem @@ -98,15 +98,15 @@ module Exec = struct let path = Loc.get_path loc in let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in let alloc_loc = Loc.of_allocsite allocsite in + let traces = TraceSet.singleton (Trace.ArrDecl location) in let mem = let alist = - Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) - |> Dom.Val.add_trace_elem (Trace.ArrDecl location) + Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in if Int.equal dimension 1 then Dom.Mem.add_stack loc alist mem else - let size = Dom.Val.Itv.zero in + let size = Dom.Val.of_itv ~traces Itv.zero in Dom.Mem.add_heap loc alist mem |> Dom.Mem.add_heap alloc_loc size in (mem, inst_num + 1) @@ -163,10 +163,9 @@ module Exec = struct in let mem = let arr = - let elem = Trace.SymAssign (loc, location) in + let traces = TraceSet.singleton (Trace.SymAssign (loc, location)) in let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in - Dom.Val.of_array_alloc allocsite ~stride ~offset ~size - |> Dom.Val.add_trace_elem elem + Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc @@ -193,15 +192,14 @@ module Exec = struct fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem -> let alloc_num = Counter.next new_alloc_num in - let elem = Trace.SymAssign (loc, location) in let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path) in let alloc_loc = Loc.of_allocsite allocsite in let v = let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in - Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) - |> Dom.Val.add_trace_elem elem + let traces = TraceSet.singleton (Trace.SymAssign (loc, location)) in + Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in let mem = Dom.Mem.add_heap loc v mem in @@ -218,11 +216,11 @@ module Exec = struct -> Dom.Mem.astate -> Dom.Mem.astate = fun pname symbol_table path location loc ~new_sym_num mem -> + let traces = TraceSet.singleton (Trace.SymAssign (loc, location)) in let size = let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num - |> Dom.Val.of_itv - |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) + |> Dom.Val.of_itv ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in Dom.Mem.add_heap loc size mem @@ -246,7 +244,10 @@ module Exec = struct Allocsite.make pname ~node_hash ~inst_num ~dimension ~path:field_path in let offset, size = (Itv.zero, length) in - let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size in + let v = + let traces = TraceSet.empty (* TODO: location of field declaration *) in + Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces + in mem |> Dom.Mem.strong_update field_loc v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None | _ -> @@ -268,7 +269,7 @@ module Exec = struct init_fields path typ locs 1 ?dyn_length mem - let rec set_dyn_length tenv typ locs dyn_length mem = + let rec set_dyn_length location tenv typ locs dyn_length mem = match typ.Typ.desc with | Tstruct typename -> ( match Tenv.lookup tenv typename with @@ -277,11 +278,13 @@ module Exec = struct let field_loc = PowLoc.append_field locs ~fn:field_name in match field_typ.Typ.desc with | Tarray {length= Some length} -> - let length = Itv.plus (Itv.of_int_lit length) dyn_length in - let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in + let length = Itv.plus (Itv.of_int_lit length) dyn_length |> Dom.Val.of_itv in + let v = + Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_length location ~length + in Dom.Mem.strong_update field_loc v mem | _ -> - set_dyn_length tenv field_typ field_loc dyn_length mem ) + set_dyn_length location tenv field_typ field_loc dyn_length mem ) | _ -> mem ) | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 0c435a711..312f276de 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -124,7 +124,8 @@ module Exec : sig -> Dom.Mem.astate -> Dom.Mem.astate - val set_dyn_length : Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate + val set_dyn_length : + Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate end module Check : sig diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b420893e0..dc3772a4b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -32,7 +32,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, C codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [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_L2, no_bucket, ERROR, [Parameter: len,ArrayDeclaration,Parameter: len,ArrayAccess: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]] codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10] codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: x[*].f,Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2] @@ -95,7 +95,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, I 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, 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, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: n,ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: 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` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10] @@ -107,25 +107,25 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [-length + length + 1, length] Size: length] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [1, length] Size: length] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: n Size: n] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: length,ArrayDeclaration,Parameter: length,ArrayAccess: Offset: [-length + length + 1, length] Size: length] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: length,ArrayDeclaration,Parameter: length,Assignment,ArrayAccess: Offset: [1, length] Size: length] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: n,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: n Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Assignment,Return,ArrayDeclaration,Call,Assignment,Return,ArrayAccess: 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, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Assignment,Return,ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [5, 15]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: 10] -codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n, +oo] Size: n] -codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: n,ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: Offset: [n, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: n,ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: Offset: [n, +oo] Size: n] codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([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, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: 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_L5, no_bucket, ERROR, [Offset added: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ] +codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: unknown,Assignment,Call,Parameter: len,ArrayDeclaration,Parameter: len,ArrayAccess: 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, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] @@ -159,7 +159,7 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] -codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [-length + length + 1, length] Size: length] +codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: length,ArrayDeclaration,Parameter: length,ArrayAccess: Offset: [-length + length + 1, length] Size: length] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] @@ -208,5 +208,5 @@ codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_ codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: x,Binop: (x + [-oo, +oo]):signed32] -codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 9bfe5484a..787f7114c 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -28,14 +28,14 @@ codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: (1 - [0, +oo]):unsigned64] 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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [1, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Assignment,Return,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5] -codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 7 Size: 5] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 7 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: 5 by call to `loop` ] @@ -75,7 +75,7 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,ArrayDeclaration,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, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 index ffbf744d4..ad4831b11 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 @@ -12,4 +12,4 @@ codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_AL codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, TAINTED_MEMORY_ALLOCATION, no_bucket, ERROR, [Return from __infer_taint_source,Call to __set_array_length with tainted index 1,-----------,Unknown value from: __infer_taint_source,Assignment,Alloc: Length: [-oo, 2147483647]] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: __infer_taint_source,Assignment,Return,Assignment,Call,ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source with tainted data return*,Return from multi_level_source_bad,Call to multi_level_sink_bad with tainted index 0,Call to __array_access with tainted index 0,-----------,Call,Unknown value from: __infer_taint_source,Assignment,Return,Assignment,Call,ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Assignment,Call,Parameter: __param_0[*].ind,Assignment,Call,Parameter: info[*].size,ArrayDeclaration,Parameter: info[*].ind,ArrayAccess: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ]