From 5f60ffaa8fd8373460d22e70903e8767682a27cc Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 23 Nov 2018 13:55:07 -0800 Subject: [PATCH] [inferbo] Trace refactoring Reviewed By: skcho Differential Revision: D13116116 fbshipit-source-id: 0b885dcfb --- .../src/bufferoverrun/bufferOverrunChecker.ml | 48 +-- .../src/bufferoverrun/bufferOverrunDomain.ml | 13 +- .../src/bufferoverrun/bufferOverrunModels.ml | 14 +- .../bufferOverrunProofObligations.ml | 35 +- .../bufferOverrunProofObligations.mli | 13 +- infer/src/bufferoverrun/bufferOverrunTrace.ml | 289 ++++++++++++----- infer/src/bufferoverrun/bufferOverrunUtils.ml | 20 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 306 +++++++++--------- .../codetoanalyze/c/performance/issues.exp | 24 +- .../cpp/bufferoverrun/issues.exp | 174 +++++----- .../cpp/quandaryBO/issues.exp-t1 | 10 +- .../cpp/quandaryBO/issues.exp-t2 | 10 +- .../cpp/quandaryBO/issues.exp-t3 | 16 +- .../cpp/quandaryBO/issues.exp-t4 | 28 +- .../java/bufferoverrun/issues.exp | 2 +- .../codetoanalyze/java/performance/issues.exp | 58 ++-- 16 files changed, 572 insertions(+), 488 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 34f6b7da8..a5b2edea8 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -17,7 +17,6 @@ module L = Logging module Models = BufferOverrunModels module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace -module TraceSet = Trace.Set module Payload = SummaryPayload.Make (struct type t = BufferOverrunSummary.t @@ -40,10 +39,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let copy_reachable_new_locs_from locs mem = let copy loc acc = Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> - let v = - Dom.Val.subst v eval_sym_trace location - |> Dom.Val.add_trace_elem (Trace.Return location) - in + let v = Dom.Val.subst v eval_sym_trace location in Dom.Mem.add_heap loc v acc ) in let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in @@ -71,7 +67,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ret_val = Dom.Mem.find ret_loc callee_exit_mem in let ret_var = Loc.of_var (Var.of_id id) in Dom.Val.subst ret_val eval_sym_trace location - |> Dom.Val.add_trace_elem (Trace.Return location) |> Fn.flip (Dom.Mem.add_stack ret_var) mem |> instantiate_ret_alias |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) @@ -748,50 +743,15 @@ module Report = struct ~init:PO.ConditionSet.empty - let make_err_trace : Trace.t -> string -> Errlog.loc_trace = - fun trace issue_desc -> - let f elem (trace, depth) = - match elem with - | Trace.Alloc location -> - let desc = "Alloc: " ^ issue_desc in - (Errlog.make_trace_element depth location desc [] :: trace, depth) - | Trace.ArrAccess location -> - let desc = "ArrayAccess: " ^ issue_desc in - (Errlog.make_trace_element depth location desc [] :: trace, depth) - | Trace.ArrDecl location -> - (Errlog.make_trace_element depth location "ArrayDeclaration" [] :: trace, depth) - | Trace.Assign location -> - (Errlog.make_trace_element depth location "Assignment" [] :: trace, depth) - | Trace.Binop location -> - let desc = "Binop: " ^ issue_desc in - (Errlog.make_trace_element depth location desc [] :: trace, depth) - | Trace.Call location -> - (Errlog.make_trace_element depth location "Call" [] :: trace, depth + 1) - | Trace.Return location -> - (Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1) - | Trace.SymAssign (loc, location) -> - if Loc.is_pretty loc then - let desc = Format.asprintf "Parameter: %a" Loc.pp loc in - (Errlog.make_trace_element depth location desc [] :: trace, depth) - else (trace, depth) - | Trace.UnknownFrom (pname_opt, location) -> - let desc = Format.asprintf "Unknown value from: %a" Trace.pp_pname_opt pname_opt in - (Errlog.make_trace_element depth location desc [] :: trace, depth) - in - List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev - - let report_errors : Summary.t -> PO.ConditionSet.t -> PO.ConditionSet.t = fun summary cond_set -> let report cond trace issue_type = let location = PO.ConditionTrace.get_report_location trace in let description ~markup = PO.description ~markup cond trace in let trace = - match TraceSet.choose_shortest (PO.ConditionTrace.get_val_traces trace) with - | trace -> - make_err_trace trace (description ~markup:false) - | exception _ -> - [Errlog.make_trace_element 0 location (description ~markup:false) []] + let description = description ~markup:false in + Trace.Issue.make_err_trace ~description (PO.ConditionTrace.get_val_traces trace) + |> Errlog.concat_traces in Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true) in diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 0c00235dc..97cf98c6d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -59,7 +59,7 @@ module Val = struct let unknown_from : callee_pname:_ -> location:_ -> t = fun ~callee_pname ~location -> - let traces = TraceSet.singleton (Trace.UnknownFrom (callee_pname, location)) in + let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in { itv= Itv.top ; sym= Relation.Sym.top ; powloc= PowLoc.unknown @@ -167,7 +167,7 @@ module Val = struct { bot with itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num ; sym= Relation.Sym.of_loc loc - ; traces= TraceSet.singleton (Trace.SymAssign (loc, location)) + ; traces= Trace.(Set.singleton location (Parameter loc)) ; represents_multiple_values } @@ -309,19 +309,16 @@ module Val = struct |> normalize - let add_trace_elem : Trace.elem -> t -> t = - fun elem x -> - let traces = TraceSet.add_elem elem x.traces in + let add_assign_trace_elem location x = + let traces = Trace.(Set.add_elem location Assign) x.traces in {x with traces} - 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 } + ; traces= Trace.(Set.add_elem location ArrayDeclaration) length.traces } let set_array_stride : Z.t -> t -> t = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 2ad01a621..488219cf8 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -15,7 +15,6 @@ module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace -module TraceSet = Trace.Set type model_env = { pname: Typ.Procname.t @@ -87,10 +86,7 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = | Bottom -> cond_set | NonBottom length -> - let alloc_trace_elem = BufferOverrunTrace.Alloc location in - let traces = - Dom.Val.get_traces v_length |> BufferOverrunTrace.Set.add_elem alloc_trace_elem - in + let traces = Dom.Val.get_traces v_length in PO.ConditionSet.add_alloc_size location ~length traces cond_set @@ -110,7 +106,7 @@ let malloc size_exp = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, stride, 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 traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in let path = Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path in let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let offset, size = (Itv.zero, Dom.Val.get_itv length) in @@ -257,7 +253,7 @@ let set_array_length array length_exp = 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 traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let traces = Trace.(Set.add_elem location ArrayDeclaration) (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 @@ -279,7 +275,7 @@ module Split = struct |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field in - let f_trace _ traces = TraceSet.add_elem (Trace.Return location) traces in + let f_trace _ traces = Trace.(Set.add_elem location Through) traces in Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem end @@ -399,7 +395,7 @@ module Collection = struct let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in 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 traces = Trace.(Set.singleton location ArrayDeclaration) 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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 16c37c58e..aee51d1a9 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -9,11 +9,11 @@ open! IStd open! AbstractDomain.Types module F = Format module L = Logging +module Bound = Bounds.Bound module ItvPure = Itv.ItvPure -module Relation = BufferOverrunDomainRelation module MF = MarkupFormatter -module ValTraceSet = BufferOverrunTrace.Set -module Bound = Bounds.Bound +module Relation = BufferOverrunDomainRelation +module ValTrace = BufferOverrunTrace type checked_condition = {report_issue_type: IssueType.t option; propagate: bool} @@ -591,7 +591,7 @@ module ConditionTrace = struct [@@deriving compare] type 'cond_trace t0 = - {cond_trace: 'cond_trace; issue_location: Location.t; val_traces: ValTraceSet.t} + {cond_trace: 'cond_trace; issue_location: Location.t; val_traces: ValTrace.Issue.t} [@@deriving compare] type t = intra_cond_trace t0 [@@deriving compare] @@ -610,9 +610,9 @@ module ConditionTrace = struct | Inter {callee_pname; call_site} -> let pname = Typ.Procname.to_string callee_pname in F.fprintf fmt " by call to %s at %a (%a)" pname Location.pp_file_pos call_site - ValTraceSet.pp ct.val_traces + ValTrace.Issue.pp ct.val_traces | Intra -> - F.fprintf fmt " (%a)" ValTraceSet.pp ct.val_traces + F.fprintf fmt " (%a)" ValTrace.Issue.pp ct.val_traces let pp_description : F.formatter -> t -> unit = @@ -631,16 +631,16 @@ module ConditionTrace = struct fun ct -> match ct.cond_trace with Intra -> ct.issue_location | Inter {call_site} -> call_site - let make : Location.t -> ValTraceSet.t -> t = + let make : Location.t -> ValTrace.Issue.t -> t = fun issue_location val_traces -> {issue_location; cond_trace= Intra; val_traces} let make_call_and_subst ~traces_caller ~callee_pname call_site ct = - let val_traces = ValTraceSet.call call_site ~traces_caller ~traces_callee:ct.val_traces in + let val_traces = ValTrace.Issue.call call_site traces_caller ct.val_traces in {ct with cond_trace= Inter {callee_pname; call_site}; val_traces} - let has_unknown ct = ValTraceSet.has_unknown ct.val_traces + let has_unknown ct = ValTrace.Issue.has_unknown ct.val_traces let check issue_type_u5 : _ t0 -> IssueType.t option = fun ct -> if has_unknown ct then Some issue_type_u5 else None @@ -697,8 +697,8 @@ module ConditionWithTrace = struct | Some cond -> let traces_caller = Symb.SymbolSet.fold - (fun symbol val_traces -> ValTraceSet.join (trace_of_sym symbol) val_traces) - symbols ValTraceSet.empty + (fun symbol val_traces -> ValTrace.Set.join (trace_of_sym symbol) val_traces) + symbols ValTrace.Set.empty in let trace = ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace @@ -818,22 +818,25 @@ module ConditionSet = struct let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp - ~relation val_traces condset = + ~relation ~idx_traces ~arr_traces condset = ArrayAccessCondition.make ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation |> Condition.make_array_access - |> add_opt location val_traces condset + |> add_opt location + (ValTrace.Issue.(binary location ArrayAccess) idx_traces arr_traces) + condset let add_alloc_size location ~length val_traces condset = AllocSizeCondition.make ~length |> Condition.make_alloc_size - |> add_opt location val_traces condset + |> add_opt location (ValTrace.Issue.alloc location val_traces) condset - let add_binary_operation integer_type_widths location bop ~lhs ~rhs val_traces condset = + let add_binary_operation integer_type_widths location bop ~lhs ~rhs ~lhs_traces ~rhs_traces + condset = BinaryOperationCondition.make integer_type_widths bop ~lhs ~rhs |> Condition.make_binary_operation - |> add_opt location val_traces condset + |> add_opt location (ValTrace.Issue.(binary location Binop) lhs_traces rhs_traces) condset let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 4ea473aed..520f1e8fd 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -9,7 +9,6 @@ open! IStd open! AbstractDomain.Types module ItvPure = Itv.ItvPure module Relation = BufferOverrunDomainRelation -module ValTraceSet = BufferOverrunTrace.Set module Condition : sig type t @@ -20,7 +19,7 @@ module ConditionTrace : sig val get_report_location : t -> Location.t - val get_val_traces : t -> ValTraceSet.t + val get_val_traces : t -> BufferOverrunTrace.Issue.t end module ConditionSet : sig @@ -43,11 +42,12 @@ module ConditionSet : sig -> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate - -> ValTraceSet.t + -> idx_traces:BufferOverrunTrace.Set.t + -> arr_traces:BufferOverrunTrace.Set.t -> t -> t - val add_alloc_size : Location.t -> length:ItvPure.astate -> ValTraceSet.t -> t -> t + val add_alloc_size : Location.t -> length:ItvPure.astate -> BufferOverrunTrace.Set.t -> t -> t val add_binary_operation : Typ.IntegerWidths.t @@ -55,7 +55,8 @@ module ConditionSet : sig -> Binop.t -> lhs:ItvPure.astate -> rhs:ItvPure.astate - -> ValTraceSet.t + -> lhs_traces:BufferOverrunTrace.Set.t + -> rhs_traces:BufferOverrunTrace.Set.t -> t -> t @@ -63,7 +64,7 @@ module ConditionSet : sig val subst : summary_t - -> Bounds.Bound.eval_sym * (Symb.Symbol.t -> ValTraceSet.t) + -> Bounds.Bound.eval_sym * (Symb.Symbol.t -> BufferOverrunTrace.Set.t) -> Relation.SubstMap.t -> Relation.astate -> Typ.Procname.t diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index cd65e9ced..e347711d9 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -10,27 +10,30 @@ open AbsLoc module F = Format module BoTrace = struct - type elem = - | Alloc of Location.t - | ArrAccess of Location.t - | ArrDecl of Location.t - | Assign of Location.t - | Binop of Location.t - | Call of Location.t - | Return of Location.t - | SymAssign of Loc.t * Location.t - | UnknownFrom of Typ.Procname.t option * Location.t + type final = UnknownFrom of Typ.Procname.t option [@@deriving compare] + + type elem = ArrayDeclaration | Assign | Parameter of Loc.t | Through [@@deriving compare] + + type t = + | Empty + | Final of {location: Location.t; kind: final} + | Elem of {location: Location.t; length: int; kind: elem; from: t} + | Call of {location: Location.t; length: int; caller: t; callee: t} [@@deriving compare] - type t = {length: int; trace: elem list} [@@deriving compare] + let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length + + let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) + + let final location kind = Final {location; kind} - let singleton elem = {length= 1; trace= [elem]} + let add_elem location kind from = Elem {location; length= length from + 1; from; kind} - let add_elem elem t = {length= t.length + 1; trace= elem :: t.trace} + let singleton location kind = add_elem location kind Empty - let add_elem_last elem t = {length= t.length + 1; trace= t.trace @ [elem]} + let call location ~caller ~callee = + Call {location; length= 1 + length caller + length callee; caller; callee} - let append x y = {length= x.length + y.length; trace= x.trace @ y.trace} let pp_pname_opt fmt = function | None -> @@ -39,91 +42,219 @@ module BoTrace = struct Typ.Procname.pp fmt pname - let pp_elem : F.formatter -> elem -> unit = - fun fmt elem -> - match elem with - | Alloc location -> - F.fprintf fmt "Alloc (%a)" Location.pp_file_pos location - | ArrAccess location -> - F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos location - | ArrDecl location -> - F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos location - | Assign location -> - F.fprintf fmt "Assign (%a)" Location.pp_file_pos location - | Binop location -> - F.fprintf fmt "Binop (%a)" Location.pp_file_pos location - | Call location -> - F.fprintf fmt "Call (%a)" Location.pp_file_pos location - | Return location -> - F.fprintf fmt "Return (%a)" Location.pp_file_pos location - | SymAssign (loc, location) -> - F.fprintf fmt "SymAssign (%a, %a)" Loc.pp loc Location.pp_file_pos location - | UnknownFrom (pname_opt, location) -> - F.fprintf fmt "UnknownFrom (%a, %a)" pp_pname_opt pname_opt Location.pp_file_pos location - - - let pp : F.formatter -> t -> unit = - fun fmt t -> - let pp_sep fmt () = F.pp_print_string fmt " :: " in - F.pp_print_list ~pp_sep pp_elem fmt t.trace - - - let is_unknown_elem = function UnknownFrom _ -> true | _ -> false - - let has_unknown x = List.exists x.trace ~f:is_unknown_elem + let pp_location = Location.pp_file_pos + + let pp_final f = function + | UnknownFrom pname_opt -> + F.fprintf f "UnknownFrom `%a`" pp_pname_opt pname_opt + + + let pp_elem f = function + | ArrayDeclaration -> + F.pp_print_string f "ArrayDeclaration" + | Assign -> + F.pp_print_string f "Assign" + | Parameter loc -> + F.fprintf f "Parameter `%a`" Loc.pp loc + | Through -> + F.pp_print_string f "Through" + + + let rec pp f = function + | Empty -> + F.pp_print_string f "" + | Final {location; kind} -> + F.fprintf f "%a (%a)" pp_final kind pp_location location + | Elem {location; from; kind} -> + F.fprintf f "%a%a (%a)" pp_arrow from pp_elem kind pp_location location + | Call {location; caller; callee} -> + F.fprintf f "%aCall (%a) -> %a" pp_arrow caller pp_location location pp callee + + + and pp_arrow f = function Empty -> () | t -> F.fprintf f "%a -> " pp t + + let rec has_unknown = function + | Empty -> + false + | Final {kind= UnknownFrom _} -> + true + | Elem {from} -> + has_unknown from + | Call {caller; callee} -> + has_unknown caller || has_unknown callee + + + let final_err_desc = function + | UnknownFrom pname_opt -> + F.asprintf "Unknown value from: %a" pp_pname_opt pname_opt + + + let elem_err_desc = function + | ArrayDeclaration -> + "Array declaration" + | Assign -> + "Assignment" + | Parameter loc -> + if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else "" + | Through -> + "Through" + + + let rec make_err_trace depth t tail = + match t with + | Empty -> + tail + | Final {location; kind} -> + let desc = final_err_desc kind in + Errlog.make_trace_element depth location desc [] :: tail + | Elem {location; kind; from} -> + let desc = elem_err_desc kind in + let tail = + if String.is_empty desc then tail + else Errlog.make_trace_element depth location desc [] :: tail + in + make_err_trace depth from tail + | Call {location; caller; callee} -> + let desc = "Call" in + let tail = + Errlog.make_trace_element depth location desc [] + :: make_err_trace (depth + 1) callee tail + in + make_err_trace depth caller tail end module Set = struct include AbstractDomain.FiniteSet (BoTrace) + let set_singleton = singleton + + let singleton location elem = singleton (BoTrace.singleton location elem) + + let singleton_final location kind = set_singleton (BoTrace.final location kind) + (* currently, we keep only one trace for efficiency *) let join x y = if is_empty x then y else if is_empty y then x else let tx, ty = (min_elt x, min_elt y) in - if Int.( <= ) tx.length ty.length then x else y + if Int.( <= ) (BoTrace.length tx) (BoTrace.length ty) then x else y let choose_shortest set = min_elt set - let singleton elem = singleton (BoTrace.singleton elem) + let add_elem location elem t = + if is_empty t then singleton location elem else map (BoTrace.add_elem location elem) t - let add_elem elem t = if is_empty t then singleton elem else map (BoTrace.add_elem elem) t + + let non_empty t = if is_empty t then set_singleton BoTrace.Empty else t 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) - traces_callee - else - fold - (fun trace_callee traces -> - fold - (fun trace_caller traces -> - let new_trace_caller = BoTrace.add_elem (BoTrace.Call location) trace_caller in - let new_trace = BoTrace.append trace_callee new_trace_caller in - add new_trace traces ) - traces_caller traces ) - traces_callee empty - - - let merge ~arr_traces ~idx_traces location = - if is_empty idx_traces then - map (fun arr_traces -> BoTrace.add_elem (BoTrace.ArrAccess location) arr_traces) arr_traces - else - fold - (fun idx_traces traces -> - fold - (fun arr_traces traces -> - let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess location) idx_traces in - let new_trace = BoTrace.append new_trace_idx arr_traces in - add new_trace traces ) - arr_traces traces ) - idx_traces empty + let traces_caller = non_empty traces_caller in + let traces_callee = non_empty traces_callee in + fold + (fun caller traces -> + fold + (fun callee traces -> add (BoTrace.call location ~caller ~callee) traces) + traces_callee traces ) + traces_caller empty let has_unknown t = exists BoTrace.has_unknown t + + let make_err_trace depth set tail = + if is_empty set then tail else BoTrace.make_err_trace depth (choose_shortest set) tail + + + let length set = if is_empty set then 0 else BoTrace.length (choose_shortest set) +end + +module Issue = struct + type elem = Alloc [@@deriving compare] + + type binary = ArrayAccess (* offset, length *) | Binop [@@deriving compare] + + type t = + | Elem of {location: Location.t; length: int; kind: elem; from: Set.t} + | Binary of {location: Location.t; length: int; kind: binary; left: Set.t; right: Set.t} + | Call of {location: Location.t; length: int; caller: Set.t; callee: t} + [@@deriving compare] + + let length = function Elem {length} | Binary {length} | Call {length} -> length + + let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) + + let alloc location from = Elem {location; length= 1 + Set.length from; kind= Alloc; from} + + let binary location kind left right = + Binary {location; length= 3 + Set.length left + Set.length right; kind; left; right} + + + let call location caller callee = + Call {location; length= 1 + Set.length caller + length callee; caller; callee} + + + let rec has_unknown = function + | Elem {from} -> + Set.has_unknown from + | Binary {left; right} -> + Set.has_unknown left || Set.has_unknown right + | Call {caller; callee} -> + Set.has_unknown caller || has_unknown callee + + + let binary_labels = function ArrayAccess -> ("Offset", "Length") | Binop -> ("LHS", "RHS") + + let pp_elem f = function Alloc -> F.pp_print_string f "Alloc" + + let pp_binary f = function + | ArrayAccess -> + F.pp_print_string f "ArrayAccess" + | Binop -> + F.pp_print_string f "Binop" + + + let pp_location = Location.pp_file_pos + + let rec pp f = function + | Elem {location; kind; from} -> + F.fprintf f "{%a} -> %a (%a)" Set.pp from pp_elem kind pp_location location + | Binary {location; kind; left; right} -> + let left_label, right_label = binary_labels kind in + F.fprintf f "{%s: %a} {%s: %a} %a (%a)" left_label Set.pp left right_label Set.pp right + pp_binary kind pp_location location + | Call {location; caller; callee} -> + F.fprintf f "{%a} Call (%a) -> %a" Set.pp caller pp_location location pp callee + + + let elem_err_desc ~description = function Alloc -> "Allocation: " ^ description + + let binary_err_desc ~description = function + | ArrayAccess -> + "Array access: " ^ description + | Binop -> + "Binary operation: " ^ description + + + let format_label label = F.sprintf "<%s trace>" label + + let make_err_trace ~description t = + let rec aux depth = function + | Elem {location; kind; from} -> + let desc = elem_err_desc ~description kind in + [("", Set.make_err_trace depth from [Errlog.make_trace_element depth location desc []])] + | Binary {location; kind; left; right} -> + let left_label, right_label = binary_labels kind in + let desc = binary_err_desc ~description kind in + [ (format_label left_label, Set.make_err_trace depth left []) + ; (format_label right_label, Set.make_err_trace depth right []) + ; ("", [Errlog.make_trace_element depth location desc []]) ] + | Call {location; caller; callee} -> + let desc = "Call" in + ("", Set.make_err_trace depth caller [Errlog.make_trace_element depth location desc []]) + :: aux (depth + 1) callee + in + aux 0 t end include BoTrace diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index bd014dbdb..98e8fd271 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -69,7 +69,7 @@ module Exec = struct let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in let mem = let arr = - let traces = TraceSet.singleton (Trace.ArrDecl location) in + let traces = Trace.(Set.singleton location ArrayDeclaration) in Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in @@ -98,7 +98,7 @@ 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 traces = Trace.(Set.singleton location ArrayDeclaration) in let mem = let alist = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces @@ -163,7 +163,7 @@ module Exec = struct in let mem = let arr = - let traces = TraceSet.singleton (Trace.SymAssign (loc, location)) in + let traces = Trace.(Set.singleton location (Parameter loc)) in let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values @@ -198,7 +198,7 @@ module Exec = struct let alloc_loc = Loc.of_allocsite allocsite in let v = let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in - let traces = TraceSet.singleton (Trace.SymAssign (loc, location)) in + let traces = Trace.(Set.singleton location (Trace.Parameter loc)) in Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values in @@ -216,9 +216,9 @@ 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 + let traces = Trace.(Set.singleton location (Parameter loc)) in Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv ~traces |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values @@ -305,9 +305,8 @@ module Check = struct offset in let arr_traces = Dom.Val.get_traces arr in - let traces = TraceSet.merge ~arr_traces ~idx_traces location in PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp - ~idx_sym_exp ~relation ~is_collection_add traces cond_set + ~idx_sym_exp ~relation ~is_collection_add ~idx_traces ~arr_traces cond_set | _ -> cond_set @@ -378,15 +377,12 @@ module Check = struct let rhs_itv = Dom.Val.get_itv rhs in match (lhs_itv, rhs_itv) with | NonBottom lhs_itv, NonBottom rhs_itv -> - let traces = - TraceSet.join (Dom.Val.get_traces lhs) (Dom.Val.get_traces rhs) - |> TraceSet.add_elem (Trace.Binop location) - in L.(debug BufferOverrun Verbose) "@[Add condition :@,bop:%s@, lhs: %a@, rhs: %a@,@]@." (Binop.str Pp.text bop) Itv.ItvPure.pp lhs_itv Itv.ItvPure.pp rhs_itv ; PO.ConditionSet.add_binary_operation integer_type_widths location bop ~lhs:lhs_itv - ~rhs:rhs_itv traces cond_set + ~rhs:rhs_itv ~lhs_traces:(Dom.Val.get_traces lhs) ~rhs_traces:(Dom.Val.get_traces rhs) + cond_set | _, _ -> cond_set end diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 97c1208a3..a2b70337b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,165 +1,165 @@ -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_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_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] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32] +codetoanalyze/c/bufferoverrun/arith.c, band_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,Assignment,Assignment,,Array declaration,Array access: Offset: [0, 2] Size: 2] +codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_nat,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_Good, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_nat,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 9] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] +codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Parameter `y`,Binary operation: (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, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (300000 × 300000):signed32] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([0, 2000000000] + [0, 2000000000]):signed32] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (300000 × 300000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (-2000000000 - 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/arith.c, minmax_div_const_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [0, 8] Size: 7] -codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (0 - -9223372036854775808):signed64] -codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64] -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] -codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] × 2):unsigned64] -codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-1 × -9223372036854775808):signed64] -codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10] -codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20] -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, 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/arith.c, minmax_div_const_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `n`,,Array declaration,Array access: Offset: [0, 8] Size: 7] +codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - -9223372036854775808):signed64] +codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Unknown value from: unknown_uint,Assignment,Binary operation: ([0, +oo] - 1):unsigned64] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [-4, 4] Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [-4, 4] Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: unknown_uint,Assignment,Binary operation: ([-oo, +oo] × 2):unsigned64] +codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (-1 × -9223372036854775808):signed64] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 14] Size: 10] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 25] Size: 20] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: 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,Binary operation: ([-oo, 9223372036854775807] + 1):signed64] +codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binary operation: (85 × 4294967295):unsigned32] +codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] +codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] 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, [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] -codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3] -codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 6] -codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460] +codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `len`,,Parameter `len`,Array declaration,Array access: 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, [,Assignment,,Array declaration,Array access: 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,Array access: Offset: -1 Size: 2] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 2 Size: 2] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 3] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 6 Size: 6] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Array declaration,Assignment,Assignment,Array access: Offset: 999999999 Size: 26460] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] -codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10] -codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 20 Size: 16] +codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 20 Size: 16] codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, 10] Size: 10 by call to `do_while_sub` ] -codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10] -codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] -codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: m,Assignment,Return,ArrayAccess: Offset: 15 Size: 10] -codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,,Assignment,,Parameter `a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ] +codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ] +codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] +codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,,Assignment,,Parameter `arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] +codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `m`,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] +codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,Parameter: arr,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,Parameter: x[*].field,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,Parameter: x[*].field,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] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `arr[*]`,Assignment,,Parameter `arr`,Array access: 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, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 5] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] × 4):unsigned64] -codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([0, +oo] + 5):signed32] -codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] × 10):signed32] -codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: [5, +oo]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: Length: 2000000000] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: Length: -2] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] -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, 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, [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] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i), i] Size: 10] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [i, min(-1, i)] Size: 10] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] × 10):signed32] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: 5] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 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_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, [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, [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, [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/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Assignment,Assignment,Binary operation: ([5, +oo] × 4):unsigned64] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Assignment,Assignment,Binary operation: ([0, +oo] + 5):signed32] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 10 Size: [5, +oo]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Allocation: Length: 2000000000] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -2] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Allocation: Length: [1, 1000000001]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Allocation: Length: [1, 1000000001]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Allocation: Length: [-5, 5]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Allocation: 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`,Allocation: 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`,,Call,Assignment,Assignment,Binary operation: (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, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: [10, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,Assignment,,Parameter `n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Parameter `n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [max(10, i), i] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [-1, 9] Size: 9] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [-1, 9] Size: 9] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: 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`,Assignment,,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `n`,,Parameter `n`,Array declaration,Array access: Offset: n Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [-1, 9] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: 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,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_function,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [,Parameter `n`,Assignment,,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [,Parameter `n`,Assignment,,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [-19+min(0, x), -1] Size: 1] +codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,,Array declaration,Array access: Offset: [-19+min(0, x), -1] Size: 1] codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: unknown,Assignment,Call,Parameter: len,ArrayDeclaration,Parameter: len,ArrayAccess: 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`,,Parameter `len`,Array declaration,Array access: Offset added: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] -codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [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] -codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: 10000] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 10 Size: 5] -codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] -codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] -codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 255] Size: 255] +codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 256] Size: 256] +codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [-1, 255] Size: 10000] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 10 Size: 5] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024] -codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 (⇐ 5 + 5) Size: 10] -codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ] -codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ] -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, [Parameter: length,ArrayDeclaration,Parameter: length,ArrayAccess: Offset: [-length + length + 1, length] Size: length] +codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024] +codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10] +codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `x`,,Parameter `p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ] +codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ] +codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `x`,Array access: 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, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: 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] @@ -174,24 +174,24 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 10 by call to `prune_add2` ] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 10 by call to `prune_sub2` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1] -codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 1 by call to `array_access_Ok` ] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] +codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 1 by call to `array_access_Ok` ] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -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, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: 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, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 0] +codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: 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] @@ -203,10 +203,10 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, [Here] -codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 4] Size: 1 by call to `do_two_times2_Good` ] -codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ] +codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Assignment,,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times2_Good` ] +codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Assignment,,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ] 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, [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] +codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([-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`,,Parameter `y`,Binary operation: (x + [-oo, +oo]):signed32] +codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Assignment,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index b66f84bdd..ab46baf25 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -25,7 +25,7 @@ codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_wi codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3530, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3530, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3530, degree = 0] -codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3530, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3530, degree = 0] @@ -38,8 +38,8 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] -codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: ([-oo, +oo] + 1):signed32] +codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binary operation: ([-oo, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 726, degree = 0] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104, degree = 0] codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104, degree = 0] @@ -58,7 +58,7 @@ codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTIO codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] @@ -70,11 +70,11 @@ codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 5, EXPENSIVE codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1309, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 614, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 614, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 616, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2551, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2551, degree = 0] @@ -84,12 +84,12 @@ codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 6, EXPENSIVE_EXECUTIO codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2553, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, real_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32] +codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 29]):signed32] codetoanalyze/c/performance/cost_test_deps.c, real_while, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 219, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2530, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2530, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2530, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2530, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2532, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3535, degree = 0] @@ -108,9 +108,9 @@ codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensi codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2537, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32] +codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 29]):signed32] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 219, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 551, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 551, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 553, degree = 0] @@ -148,7 +148,7 @@ codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CAL codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] -codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/loops.c, if_in_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 379, degree = 0] @@ -171,7 +171,7 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUT codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index d0f1436f2..3a57cbb75 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,90 +1,90 @@ -INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: this[*].infer_size,Binop: (this[*].infer_size - [-oo, +oo]):unsigned64] -INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: this[*].infer_size,Binop: (this[*].infer_size + [-oo, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] -codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] -codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] -codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Parameter: n,ArrayAccess: Offset: 15 Size: 10 by call to `my_class_access_nth` ] -codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter: this[*].children,Return,Call,Parameter: this[*].children,Parameter: nth,ArrayAccess: Offset: 5 Size: 3 by call to `Tree_set_child` ] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: x[*].b,ArrayAccess: Offset: 3 Size: 3 by call to `flexible_array_param_access` ] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 3] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Assignment,Call,Parameter: n,Assignment,Return,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Call,Parameter: n,Assignment,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Return,ArrayAccess: Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 32 Size: 30] -codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, 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/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,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, [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` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 8 Size: 5 by call to `minus_params_Ok` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 5 by call to `plus_params2` ] -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_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` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params` ] +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this[*].infer_size`,,Unknown value from: std::distance_>,Binary operation: (this[*].infer_size - [-oo, +oo]):unsigned64] +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this[*].infer_size`,,Unknown value from: std::distance_>,Binary operation: (this[*].infer_size + [-oo, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] +codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Parameter `this[*].arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this[*].children`,Call,,Parameter `nth`,,Parameter `this[*].children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x[*].b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 3] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `n`,Assignment,,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `n`,Assignment,,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 32 Size: 30] +codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `__x[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: 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,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (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,Through,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: 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,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (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,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [1, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 7 Size: 5] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ] +codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 8 Size: 5 by call to `minus_params_Ok` ] +codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params2` ] +codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: 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,,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]] +codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) 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,Array declaration,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12] +codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `arr`,Array access: 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,,Parameter `x`,,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params2` ] +codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params` ] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -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_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter: this[*].infer_size,Assignment,Return,Assignment,Return,Assignment,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Parameter: this[*].infer_size,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,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Parameter: t[*].bI,Call,Parameter: t[*].bI,Call,Parameter: bi,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: t[*].bI,Call,Parameter: t[*].bI,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, [Parameter: v[*]._size,Call,Parameter: this[*]._size,Call,Parameter: this[*]._size,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] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 9223372036854775807] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 × 9223372036854775807):unsigned64] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 18446744073709551615] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 × 18446744073709551615):unsigned64] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] -codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: this[*].h,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,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, 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: 6 Size: 5] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 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, 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,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]] -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]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: v[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: __param_0[*].a,Assignment,Call,Parameter: count,Call,Parameter: this[*].a,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,Parameter: __param_0[*].a,Assignment,Call,Parameter: count,Call,Parameter: this[*].a,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,Parameter: this[*].infer_size,Assignment,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Alloc: Length: 0] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: 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,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: 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,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,,Parameter `bi`,Binary operation: ([-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, [Parameter `v[*]._size`,Call,Parameter `this[*]._size`,Call,,Parameter `i`,,Parameter `this[*]._size`,Array declaration,Assignment,Array access: 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,Allocation: Length: 4611686018427387903] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 18446744073709551615] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 42 Size: 42] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 42 Size: 42] +codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this[*].h`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([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 `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: 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`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Array declaration,Assignment,Assignment,Array access: 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`,Binary operation: ([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`,,Parameter `__n`,Binary operation: ([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`,Array access: 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`,Binary operation: (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 `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: v[*].infer_size Size: v[*].infer_size] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: 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, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: 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,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Allocation: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t1 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t1 index 2f0a5ca00..681d580b0 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t1 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t1 @@ -1,5 +1,5 @@ -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] -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, 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/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +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,Allocation: Length: [-oo, 2147483647]] +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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t2 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t2 index bbdf05057..8c5ed2798 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t2 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t2 @@ -1,10 +1,10 @@ -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, UNTRUSTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad1_FN, 0, UNTRUSTED_VARIABLE_LENGTH_ARRAY, no_bucket, ERROR, [Return from __infer_taint_source,Call to __set_array_length with tainted index 1] -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, 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,Allocation: Length: [-oo, 2147483647]] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, UNTRUSTED_VARIABLE_LENGTH_ARRAY, no_bucket, ERROR, [Return from __infer_taint_source,Call to __set_array_length with tainted index 1] -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, 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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, UNTRUSTED_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] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, UNTRUSTED_VARIABLE_LENGTH_ARRAY, no_bucket, ERROR, [Return from __infer_taint_source with tainted data @val$0.size*,Return from overlapping_issues_source_good,Call to overlapping_issues_sink_good with tainted index 0,Call to __set_array_length with tainted index 1] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t3 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t3 index 6e4f6234e..cc30e05cf 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t3 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t3 @@ -1,8 +1,8 @@ -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Alloc: Length: [-oo, 2147483647]] -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/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Allocation: Length: [-oo, 2147483647]] +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,Allocation: 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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: 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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 index f4c2a73ae..7c4f7cfc1 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 @@ -1,15 +1,15 @@ -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a,Binop: (a × b):unsigned32] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `a`,,Parameter `b`,Binary operation: (a × b):unsigned32] codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Binop: ([0, +oo] × 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: w,Assignment,Assignment,Assignment,Binop: ([-oo, +oo] + 1):unsigned64] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Binop: ([-oo, +oo] × [-oo, +oo]):unsigned32] -codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: w,Assignment,Assignment,Assignment,Binop: ([-oo, +oo] + 1):unsigned32] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Alloc: Length: [-oo, 2147483647]] -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, [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` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Binary operation: ([0, +oo] × 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `w`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: __infer_taint_source,Assignment,,Call,Parameter `w`,Assignment,Assignment,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):unsigned32] +codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `w`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned32] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,,Unknown value from: __infer_taint_source,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Allocation: Length: [-oo, 2147483647]] +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,Allocation: 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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: 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,Assignment,Call,,Parameter `i`,,Array declaration,Array access: 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, [Call,Assignment,Call,Parameter `__param_0[*].ind`,Assignment,Call,,Parameter `info[*].ind`,,Parameter `info[*].size`,Array declaration,Array access: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ] diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 6cd9bbac2..57ec24456 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1 +1 @@ -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_add_zero_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_add_zero_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index dd2fa557b..262d91968 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [2, 8] Size: 8] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [2, 8] Size: 8] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 ⋅ length.ub, degree = 1] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length.ub, degree = 1] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length.ub, degree = 1] @@ -8,27 +8,27 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 890, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 4 Size: 3] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 5 Size: 4] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 4 Size: 3] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 5 Size: 4] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 202, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 1 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: -1 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: -1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 2 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 ⋅ (list1.length.ub - 1) + 4 ⋅ list1.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 13 ⋅ (list1.length.ub - 1) + 4 ⋅ list1.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 5 ⋅ list.length.ub, degree = 1] @@ -48,7 +48,7 @@ codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break. codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,Call,Assignment,Binop: ([0, +oo] + 1):signed32 by call to `void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection)` ] +codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,Call,,Assignment,Binary operation: ([0, +oo] + 1):signed32 by call to `void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection)` ] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] @@ -60,7 +60,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963050, degree = 0] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0] @@ -80,24 +80,24 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1304, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 605, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 610, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2543, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2543, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 29]):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] @@ -107,8 +107,8 @@ codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int, codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: size,Binop: (size + [-oo, +oo]):signed32] -codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `size`,,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] @@ -125,13 +125,13 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils. codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [0, +oo]) Size: [0, +oo]] -codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: char[] String.toCharArray(),Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [0, +oo]) Size: [0, +oo]] +codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] @@ -144,12 +144,12 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a[*],Binop: (a[*] × b[*]):signed64] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `a[*]`,,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]