pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Add integer overflow issue type

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D10253878

fbshipit-source-id: 9905d7db4
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 1ae393dc76
commit fb4086c6f6
18 changed files with 482 additions and 42 deletions
Show Stats Download Patch File Download Diff File

42
infer/src/IR/Typ.ml
Unescape View File

@ -55,6 +55,8 @@ type ikind =
| IU128 (** [__uint128_t] *)
[@@deriving compare]
let equal_ikind = [%compare.equal: ikind]
let ikind_to_string = function
| IChar ->
"char"
@ -86,6 +88,46 @@ let ikind_to_string = function
"__uint128_t"
let range_of_ikind =
let range bits ~signed =
if signed then
let bound = Z.(shift_left ~$1) (bits - 1) in
Z.(~-bound, bound - ~$1)
else Z.(~$0, shift_left ~$1 bits - ~$1)
in
let u1 = range 1 ~signed:false in
let s128 = range 128 ~signed:true in
let u128 = range 128 ~signed:false in
fun {IntegerWidths.char_width; short_width; int_width; long_width; longlong_width} x ->
match x with
| IBool ->
u1
| ISChar ->
range char_width ~signed:true
| IChar | IUChar ->
range char_width ~signed:false
| IShort ->
range short_width ~signed:true
| IUShort ->
range short_width ~signed:false
| IInt ->
range int_width ~signed:true
| IUInt ->
range int_width ~signed:false
| ILong ->
range long_width ~signed:true
| IULong ->
range long_width ~signed:false
| ILongLong ->
range longlong_width ~signed:true
| IULongLong ->
range longlong_width ~signed:false
| I128 ->
s128
| IU128 ->
u128
let ikind_is_char = function IChar | ISChar | IUChar -> true | _ -> false
let ikind_is_unsigned = function

6
infer/src/IR/Typ.mli
Unescape View File

@ -41,6 +41,12 @@ type ikind =
| IU128 (** [__uint128_t] *)
[@@deriving compare]
val equal_ikind : ikind -> ikind -> bool
val ikind_to_string : ikind -> string
val range_of_ikind : IntegerWidths.t -> ikind -> Z.t * Z.t
val ikind_is_char : ikind -> bool
(** Check whether the integer kind is a char *)

8
infer/src/base/IssueType.ml
Unescape View File

@ -277,6 +277,14 @@ let infinite_execution_time_call = from_string ~enabled:false "INFINITE_EXECUTIO
let inherently_dangerous_function = from_string "INHERENTLY_DANGEROUS_FUNCTION"
let integer_overflow_l1 = from_string "INTEGER_OVERFLOW_L1"
let integer_overflow_l2 = from_string "INTEGER_OVERFLOW_L2"
let integer_overflow_l5 = from_string "INTEGER_OVERFLOW_L5"
let integer_overflow_u5 = from_string "INTEGER_OVERFLOW_U5"
let interface_not_thread_safe = from_string "INTERFACE_NOT_THREAD_SAFE"
let internal_error = from_string "Internal_error"

8
infer/src/base/IssueType.mli
Unescape View File

@ -185,6 +185,14 @@ val infinite_execution_time_call : t
val inherently_dangerous_function : t
val integer_overflow_l1 : t
val integer_overflow_l2 : t
val integer_overflow_l5 : t
val integer_overflow_u5 : t
val interface_not_thread_safe : t
val internal_error : t

116
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -500,8 +500,8 @@ module Report = struct
cond_set
let check_expr : Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t
=
let check_expr_for_array_access :
Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t =
fun exp location mem cond_set ->
let rec check_sub_expr exp cond_set =
match exp with
@ -531,6 +531,41 @@ module Report = struct
cond_set
let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set =
match bop with
| Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) ->
let lhs_v = Sem.eval lhs mem in
let rhs_v = Sem.eval rhs mem in
BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v location
cond_set
| _ ->
cond_set
let rec check_expr_for_integer_overflow integer_type_widths exp location mem cond_set =
match exp with
| Exp.UnOp (_, e, _)
| Exp.Exn e
| Exp.Lfield (e, _, _)
| Exp.Cast (_, e)
| Exp.Sizeof {dynamic_length= Some e} ->
check_expr_for_integer_overflow integer_type_widths e location mem cond_set
| Exp.BinOp (bop, lhs, rhs) ->
cond_set
|> check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem
|> check_expr_for_integer_overflow integer_type_widths lhs location mem
|> check_expr_for_integer_overflow integer_type_widths rhs location mem
| Exp.Lindex (e1, e2) ->
cond_set
|> check_expr_for_integer_overflow integer_type_widths e1 location mem
|> check_expr_for_integer_overflow integer_type_widths e2 location mem
| Exp.Closure {captured_vars} ->
List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) ->
check_expr_for_integer_overflow integer_type_widths e location mem cond_set )
| Exp.Var _ | Exp.Const _ | Exp.Lvar _ | Exp.Sizeof {dynamic_length= None} ->
cond_set
let instantiate_cond :
Tenv.t
-> Procdesc.t
@ -552,34 +587,48 @@ module Report = struct
let check_instr :
Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.Node.t
-> Sil.instr
-> Dom.Mem.astate
-> PO.ConditionSet.t
-> PO.ConditionSet.t =
fun pdesc tenv symbol_table node instr mem cond_set ->
fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set ->
match instr with
| Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
check_expr exp location mem cond_set
| Sil.Load (_, exp, _, location) ->
cond_set
|> check_expr_for_array_access exp location mem
|> check_expr_for_integer_overflow integer_type_widths exp location mem
| Sil.Store (lexp, _, rexp, location) ->
cond_set
|> check_expr_for_array_access lexp location mem
|> check_expr_for_integer_overflow integer_type_widths lexp location mem
|> check_expr_for_integer_overflow integer_type_widths rexp location mem
| Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (
match Models.Call.dispatch tenv callee_pname params with
| Some {Models.check} ->
let node_hash = CFG.Node.hash node in
let pname = Procdesc.get_proc_name pdesc in
check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set
| None -> (
match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
| Some callee_summary -> (
match Payload.of_summary callee_summary with
| Some callee_payload ->
let callee_pdesc = Summary.get_proc_desc callee_summary in
instantiate_cond tenv callee_pdesc params mem callee_payload location
|> PO.ConditionSet.join cond_set
let cond_set =
List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) ->
check_expr_for_integer_overflow integer_type_widths exp location mem cond_set )
in
match Models.Call.dispatch tenv callee_pname params with
| Some {Models.check} ->
let node_hash = CFG.Node.hash node in
let pname = Procdesc.get_proc_name pdesc in
check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set
| None -> (
match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
| Some callee_summary -> (
match Payload.of_summary callee_summary with
| Some callee_payload ->
let callee_pdesc = Summary.get_proc_desc callee_summary in
instantiate_cond tenv callee_pdesc params mem callee_payload location
|> PO.ConditionSet.join cond_set
| None ->
(* no inferbo payload *) cond_set )
| None ->
(* no inferbo payload *) cond_set )
| None ->
(* unknown call *) cond_set ) )
(* unknown call *) cond_set ) )
| Sil.Prune (exp, location, _, _) ->
check_expr_for_integer_overflow integer_type_widths exp location mem cond_set
| _ ->
cond_set
@ -598,6 +647,7 @@ module Report = struct
Summary.t
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> CFG.Node.t
@ -605,7 +655,7 @@ module Report = struct
-> Dom.Mem.astate AbstractInterpreter.State.t
-> PO.ConditionSet.t
-> PO.ConditionSet.t =
fun summary pdesc tenv symbol_table cfg node instrs state cond_set ->
fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set ->
match state with
| _ when Instrs.is_empty instrs ->
cond_set
@ -622,7 +672,9 @@ module Report = struct
| NonBottom _ ->
()
in
let cond_set = check_instr pdesc tenv symbol_table node instr pre cond_set in
let cond_set =
check_instr pdesc tenv integer_type_widths symbol_table node instr pre cond_set
in
print_debug_info instr pre cond_set ;
cond_set
@ -631,17 +683,19 @@ module Report = struct
Summary.t
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> Analyzer.invariant_map
-> PO.ConditionSet.t
-> CFG.Node.t
-> PO.ConditionSet.t =
fun summary pdesc tenv symbol_table cfg inv_map cond_set node ->
fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map cond_set node ->
match Analyzer.extract_state (CFG.Node.id node) inv_map with
| Some state ->
let instrs = CFG.instrs node in
check_instrs summary pdesc tenv symbol_table cfg node instrs state cond_set
check_instrs summary pdesc tenv integer_type_widths symbol_table cfg node instrs state
cond_set
| _ ->
cond_set
@ -650,13 +704,14 @@ module Report = struct
Summary.t
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> Analyzer.invariant_map
-> PO.ConditionSet.t =
fun summary pdesc tenv symbol_table cfg inv_map ->
fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map ->
CFG.fold_nodes cfg
~f:(check_node summary pdesc tenv symbol_table cfg inv_map)
~f:(check_node summary pdesc tenv integer_type_widths symbol_table cfg inv_map)
~init:PO.ConditionSet.empty
@ -674,6 +729,9 @@ module Report = struct
(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 ->
@ -734,7 +792,7 @@ let get_local_decls proc_desc =
let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
fun {proc_desc; tenv; summary; integer_type_widths= _} ->
fun {proc_desc; tenv; integer_type_widths; summary} ->
Preanal.do_preanalysis proc_desc tenv ;
let symbol_table = Itv.SymbolTable.empty () in
let pdata = ProcData.make proc_desc tenv symbol_table in
@ -747,7 +805,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
|> Option.map ~f:(Dom.Mem.forget_locs locals)
in
let cond_set =
Report.check_proc summary proc_desc tenv symbol_table cfg inv_map
Report.check_proc summary proc_desc tenv integer_type_widths symbol_table cfg inv_map
|> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
in
let summary =

172
infer/src/bufferoverrun/bufferOverrunProofObligations.ml
Unescape View File

@ -286,10 +286,133 @@ module ArrayAccessCondition = struct
fun locs c -> {c with relation= Relation.forget_locs locs c.relation}
end
module BinaryOperationCondition = struct
type binop_t = Plus | Minus | Mult [@@deriving compare]
let equal_binop = [%compare.equal: binop_t]
let binop_to_string = function Plus -> "+" | Minus -> "-" | Mult -> "*"
type t =
{ binop: binop_t
; typ: Typ.ikind
; integer_widths: Typ.IntegerWidths.t
; lhs: ItvPure.astate
; rhs: ItvPure.astate }
let get_symbols c = ItvPure.get_symbols c.lhs @ ItvPure.get_symbols c.rhs
let subst eval_sym c =
match (ItvPure.subst c.lhs eval_sym, ItvPure.subst c.rhs eval_sym) with
| NonBottom lhs, NonBottom rhs ->
Some {c with lhs; rhs}
| _, _ ->
None
let have_similar_bounds {binop= binop1; typ= typ1; lhs= lhs1; rhs= rhs1}
{binop= binop2; typ= typ2; lhs= lhs2; rhs= rhs2} =
equal_binop binop1 binop2 && Typ.equal_ikind typ1 typ2
&& ItvPure.have_similar_bounds lhs1 lhs2
&& ItvPure.have_similar_bounds rhs1 rhs2
let has_infty {lhs; rhs} = ItvPure.has_infty lhs || ItvPure.has_infty rhs
let xcompare ~lhs:{binop= binop1; typ= typ1; lhs= lhs1; rhs= rhs1}
~rhs:{binop= binop2; typ= typ2; lhs= lhs2; rhs= rhs2} =
if not (equal_binop binop1 binop2 && Typ.equal_ikind typ1 typ2) then `NotComparable
else
let lhscmp = ItvPure.xcompare ~lhs:lhs1 ~rhs:lhs2 in
let rhscmp = ItvPure.xcompare ~lhs:rhs1 ~rhs:rhs2 in
match (lhscmp, rhscmp) with
| `Equal, `Equal ->
`Equal
| `Equal, `LeftSubsumesRight
| `LeftSubsumesRight, `Equal
| `LeftSubsumesRight, `LeftSubsumesRight ->
`LeftSubsumesRight
| `Equal, `RightSubsumesLeft
| `RightSubsumesLeft, `Equal
| `RightSubsumesLeft, `RightSubsumesLeft ->
`RightSubsumesLeft
| `NotComparable, _
| _, `NotComparable
| `LeftSmallerThanRight, _
| _, `LeftSmallerThanRight
| `RightSmallerThanLeft, _
| _, `RightSmallerThanLeft
| `LeftSubsumesRight, `RightSubsumesLeft
| `RightSubsumesLeft, `LeftSubsumesRight ->
`NotComparable
let pp fmt {binop; typ; lhs; rhs} =
F.fprintf fmt "(%a %s %a):%s" ItvPure.pp lhs (binop_to_string binop) ItvPure.pp rhs
(Typ.ikind_to_string typ)
let pp_description = pp
let check {binop; typ; integer_widths; lhs; rhs} =
let v =
match binop with
| Plus ->
ItvPure.plus lhs rhs
| Minus ->
ItvPure.minus lhs rhs
| Mult ->
ItvPure.mult lhs rhs
in
let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in
let typ_lb, typ_ub =
let lb, ub = Typ.range_of_ikind integer_widths typ in
(Bound.of_big_int lb, Bound.of_big_int ub)
in
if
(* typ_lb <= v_lb and v_ub <= typ_ub, not an error *)
Bound.le v_ub typ_ub && Bound.le typ_lb v_lb
then {report_issue_type= None; propagate= false}
else if
(* v_ub < typ_lb or typ_ub < v_lb, definitely an error *)
Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb
then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false}
else if
(* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *)
(Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
|| (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false}
else
let is_symbolic = ItvPure.is_symbolic v in
let report_issue_type =
if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5
in
{report_issue_type; propagate= is_symbolic}
let make integer_widths bop ~lhs ~rhs =
if ItvPure.is_invalid lhs || ItvPure.is_invalid rhs then None
else
let binop, typ =
match bop with
| Binop.PlusA (Some typ) ->
(Plus, typ)
| Binop.MinusA (Some typ) ->
(Minus, typ)
| Binop.Mult (Some typ) ->
(Mult, typ)
| _ ->
L.(die InternalError)
"Unexpected type %s is given to BinaryOperationCondition." (Binop.str Pp.text bop)
in
Some {binop; typ; integer_widths; lhs; rhs}
end
module Condition = struct
type t =
| AllocSize of AllocSizeCondition.t
| ArrayAccess of {is_collection_add: bool; c: ArrayAccessCondition.t}
| BinaryOperation of BinaryOperationCondition.t
let make_alloc_size = Option.map ~f:(fun c -> AllocSize c)
@ -297,11 +420,15 @@ module Condition = struct
Option.map ~f:(fun c -> ArrayAccess {is_collection_add; c})
let make_binary_operation = Option.map ~f:(fun c -> BinaryOperation c)
let get_symbols = function
| AllocSize c ->
AllocSizeCondition.get_symbols c
| ArrayAccess {c} ->
ArrayAccessCondition.get_symbols c
| BinaryOperation c ->
BinaryOperationCondition.get_symbols c
let subst eval_sym rel_map caller_relation = function
@ -310,6 +437,8 @@ module Condition = struct
| ArrayAccess {is_collection_add; c} ->
ArrayAccessCondition.subst eval_sym rel_map caller_relation c
|> make_array_access ~is_collection_add
| BinaryOperation c ->
BinaryOperationCondition.subst eval_sym c |> make_binary_operation
let have_similar_bounds c1 c2 =
@ -318,11 +447,20 @@ module Condition = struct
AllocSizeCondition.have_similar_bounds c1 c2
| ArrayAccess {c= c1}, ArrayAccess {c= c2} ->
ArrayAccessCondition.have_similar_bounds c1 c2
| BinaryOperation c1, BinaryOperation c2 ->
BinaryOperationCondition.have_similar_bounds c1 c2
| _ ->
false
let has_infty = function ArrayAccess {c} -> ArrayAccessCondition.has_infty c | _ -> false
let has_infty = function
| ArrayAccess {c} ->
ArrayAccessCondition.has_infty c
| BinaryOperation c ->
BinaryOperationCondition.has_infty c
| _ ->
false
let xcompare ~lhs ~rhs =
match (lhs, rhs) with
@ -331,6 +469,8 @@ module Condition = struct
| ArrayAccess {is_collection_add= b1; c= lhs}, ArrayAccess {is_collection_add= b2; c= rhs}
when Bool.equal b1 b2 ->
ArrayAccessCondition.xcompare ~lhs ~rhs
| BinaryOperation lhs, BinaryOperation rhs ->
BinaryOperationCondition.xcompare ~lhs ~rhs
| _ ->
`NotComparable
@ -340,6 +480,8 @@ module Condition = struct
AllocSizeCondition.pp fmt c
| ArrayAccess {c} ->
ArrayAccessCondition.pp fmt c
| BinaryOperation c ->
BinaryOperationCondition.pp fmt c
let pp_description fmt = function
@ -347,6 +489,8 @@ module Condition = struct
AllocSizeCondition.pp_description fmt c
| ArrayAccess {c} ->
ArrayAccessCondition.pp_description fmt c
| BinaryOperation c ->
BinaryOperationCondition.pp_description fmt c
let check = function
@ -354,13 +498,15 @@ module Condition = struct
AllocSizeCondition.check c
| ArrayAccess {is_collection_add; c} ->
ArrayAccessCondition.check ~is_collection_add c
| BinaryOperation c ->
BinaryOperationCondition.check c
let forget_locs locs x =
match x with
| ArrayAccess {is_collection_add; c} ->
ArrayAccess {is_collection_add; c= ArrayAccessCondition.forget_locs locs c}
| AllocSize _ ->
| AllocSize _ | BinaryOperation _ ->
x
end
@ -422,9 +568,13 @@ module ConditionTrace = struct
let has_unknown ct = ValTraceSet.has_unknown ct.val_traces
let check : _ t0 -> IssueType.t option =
fun ct -> if has_unknown ct then Some IssueType.buffer_overrun_u5 else None
let check issue_type_u5 : _ t0 -> IssueType.t option =
fun ct -> if has_unknown ct then Some issue_type_u5 else None
let check_buffer_overrun ct = check IssueType.buffer_overrun_u5 ct
let check_integer_overflow ct = check IssueType.integer_overflow_u5 ct
let for_summary : _ t0 -> summary_t = fun ct -> {ct with cond_trace= ()}
end
@ -481,13 +631,15 @@ module ConditionWithTrace = struct
Some {cond; trace; reported= cwt.reported}
let set_buffer_overrun_u5 {cond; trace} issue_type =
let set_u5 {cond; trace} issue_type =
if
( IssueType.equal issue_type IssueType.buffer_overrun_l3
|| IssueType.equal issue_type IssueType.buffer_overrun_l4
|| IssueType.equal issue_type IssueType.buffer_overrun_l5 )
&& Condition.has_infty cond
then Option.value (ConditionTrace.check trace) ~default:issue_type
then Option.value (ConditionTrace.check_buffer_overrun trace) ~default:issue_type
else if IssueType.equal issue_type IssueType.integer_overflow_l5 && Condition.has_infty cond
then Option.value (ConditionTrace.check_integer_overflow trace) ~default:issue_type
else issue_type
@ -497,7 +649,7 @@ module ConditionWithTrace = struct
| None ->
checked
| Some issue_type ->
let issue_type = set_buffer_overrun_u5 cwt issue_type in
let issue_type = set_u5 cwt issue_type in
(* Only report if the precision has improved.
This is approximated by: only report if the issue_type has changed. *)
let report_issue_type =
@ -602,6 +754,12 @@ module ConditionSet = struct
|> add_opt location val_traces condset
let add_binary_operation integer_type_widths location bop ~lhs ~rhs val_traces condset =
BinaryOperationCondition.make integer_type_widths bop ~lhs ~rhs
|> Condition.make_binary_operation
|> add_opt location val_traces condset
let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site =
let subst_add_cwt condset cwt =
match

10
infer/src/bufferoverrun/bufferOverrunProofObligations.mli
Unescape View File

@ -48,6 +48,16 @@ module ConditionSet : sig
val add_alloc_size : Location.t -> length:ItvPure.astate -> ValTraceSet.t -> t -> t
val add_binary_operation :
Typ.IntegerWidths.t
-> Location.t
-> Binop.t
-> lhs:ItvPure.astate
-> rhs:ItvPure.astate
-> ValTraceSet.t
-> t
-> t
val join : t -> t -> t
val subst :

3
infer/src/bufferoverrun/bufferOverrunTrace.ml
Unescape View File

@ -15,6 +15,7 @@ module BoTrace = struct
| 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
@ -49,6 +50,8 @@ module BoTrace = struct
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 ->

18
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -364,4 +364,22 @@ module Check = struct
let arr = Sem.eval_arr array_exp mem in
let relation = Dom.Mem.get_relation mem in
array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set
let binary_operation integer_type_widths bop ~lhs ~rhs location cond_set =
let lhs_itv = Dom.Val.get_itv lhs in
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)
"@[<v 2>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
| _, _ ->
cond_set
end

9
infer/src/bufferoverrun/bufferOverrunUtils.mli
Unescape View File

@ -167,4 +167,13 @@ module Check : sig
-> Location.t
-> PO.ConditionSet.t
-> PO.ConditionSet.t
val binary_operation :
Typ.IntegerWidths.t
-> Binop.t
-> lhs:Dom.Val.t
-> rhs:Dom.Val.t
-> Location.t
-> PO.ConditionSet.t
-> PO.ConditionSet.t
end

6
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -127,6 +127,12 @@ module ItvPure : sig
val get_symbols : t -> Symbol.t list
val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted
val plus : t -> t -> t
val minus : t -> t -> t
val mult : t -> t -> t
end
include module type of AbstractDomain.BottomLifted (ItvPure)

1
infer/tests/build_systems/differential_of_costs_report/introduced.exp
Unescape View File

@ -1,2 +1,3 @@
INTEGER_OVERFLOW_L5, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 3
PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, int DiffExample.f4(int), 39
INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, void DiffExample.f1(int), 19

16
infer/tests/codetoanalyze/c/bufferoverrun/arith.c
Unescape View File

@ -111,7 +111,7 @@ void plus_linear_min3_Good_FP() {
a[plus_linear_min(15)] = 1;
}
void integer_overflow_by_addition_Bad_FN() {
void integer_overflow_by_addition_Bad() {
char arr[10];
int32_t x = 2000000000;
int32_t y = 2000000000;
@ -121,7 +121,17 @@ void integer_overflow_by_addition_Bad_FN() {
}
}
void integer_overflow_by_subtraction_Bad_FN() {
void integer_overflow_by_addition_l2_Bad(int x) {
int32_t y;
if (x) {
y = 0;
} else {
y = 2000000000;
}
y = y + y;
}
void integer_overflow_by_subtraction_Bad() {
char arr[10];
int32_t x = -2000000000;
int32_t y = 2000000000;
@ -131,7 +141,7 @@ void integer_overflow_by_subtraction_Bad_FN() {
}
}
void integer_overflow_by_multiplication_Bad_FN() {
void integer_overflow_by_multiplication_Bad() {
char arr[10];
int32_t x = 300000;
int32_t y = 300000;

26
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -1,6 +1,10 @@
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):int]
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):int]
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (300000 * 300000):int]
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):int]
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
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, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
@ -9,6 +13,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2
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/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([1, +oo] - 1):int]
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
@ -16,6 +21,7 @@ codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_
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, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
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]
@ -28,6 +34,7 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ]
codetoanalyze/c/bufferoverrun/do_while.c, do_while_sub, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
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` ]
@ -50,6 +57,9 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CON
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/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
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):unsigned long]
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):int]
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):int]
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]
@ -59,11 +69,14 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERB
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]):int by call to `alloc_may_be_big2_Silenced` ]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Assignment,Binop: ([1, +oo] + 1):int 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.lb), i.ub] 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.lb, min(-1, i.ub)] 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):int]
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]
@ -74,11 +87,14 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2,
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_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):int]
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):int]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n]
codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n]
codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, []
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]
@ -99,7 +115,9 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_b
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
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_with_label.c, nested_loop_with_label, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024]
codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10]
@ -107,6 +125,8 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFE
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 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_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: 5 by call to `prune_arrblk_eq` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax1_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Binop: (0 - 1):unsigned int by call to `prune_minmax1_Ok` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax2_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 2):unsigned int by call to `prune_minmax2_Ok` ]
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, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []

18
infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
Unescape View File

@ -138,3 +138,21 @@ void FP_call_prune_arrblk_eq_Ok() {
int* x = (int*)malloc(sizeof(int) * 5);
prune_arrblk_eq(x);
}
void prune_minmax1_Ok(unsigned int x, unsigned int y) {
if (x > 0) {
if (y >= x + 1) {
unsigned int z = y - 1;
}
}
}
void FP_call_prune_minmax1_Ok() { prune_minmax1_Ok(0, 0); }
void prune_minmax2_Ok(unsigned int x, unsigned int y) {
if (x > y) {
unsigned int z = x - y;
}
}
void FP_call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); }

23
infer/tests/codetoanalyze/c/performance/issues.exp
Unescape View File

@ -17,12 +17,14 @@ codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDI
codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 603, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@ -32,6 +34,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 9 + 7 * 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, []
codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: ([-oo, +oo] + 1):int]
codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0]
codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1103, degree = 0]
codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1103, degree = 0]
@ -47,6 +51,7 @@ codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTIO
codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (-m.lb + 20), degree = 1]
codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * (-m.lb + 20), degree = 1]
codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0]
@ -54,20 +59,29 @@ 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 1207, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 613, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):int]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):int]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):int]
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 548, degree = 0]
@ -83,20 +97,25 @@ codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME
codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1]
codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0]
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0]
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2005, degree = 0]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0]
codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 227, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/loops.c, if_in_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
codetoanalyze/c/performance/loops.c, if_in_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0]
@ -106,6 +125,7 @@ codetoanalyze/c/performance/loops.c, if_out_loop, 8, EXPENSIVE_EXECUTION_TIME_CA
codetoanalyze/c/performance/loops.c, if_out_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 514, degree = 0]
codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0]
codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0]
codetoanalyze/c/performance/loops.c, larger_state_FN, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0]
codetoanalyze/c/performance/loops.c, larger_state_FN, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0]
codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
@ -114,7 +134,10 @@ 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 604, 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, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Binop: (n + [-oo, +oo]):int]
codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 15, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Assignment,Binop: ([-oo, +oo] - 1):int]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * 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 + 7 * m.ub, degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub, degree = 1]

20
infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
Unescape View File

@ -1,3 +1,5 @@
INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<Int_no_copy,std::allocator<Int_no_copy>>_erase, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size - [-oo, +oo]):unsigned long]
INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<int,std::allocator<int>>_insert<std::__list_iterator<int,_void_*>_>, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size + [-oo, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,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]
@ -16,7 +18,10 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFE
codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Return,ArrayAccess: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [0, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned long]
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]
@ -36,18 +41,33 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Binop: ([-oo, +oo] - 1):int]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):int by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, 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, [ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([1, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([2, +oo] + 1):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([3, +oo] + 42):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Binop: (4 * [45, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Call,Binop: (4 * [0, +oo]):unsigned long]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ]

22
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -11,6 +11,7 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 4 Size: 3]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 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):int]
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: 1 Size: 0]
@ -19,6 +20,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_o
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_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):int]
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]
@ -39,9 +41,12 @@ codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, maxJ.ub + -1]):int]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
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(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_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):int 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 6 + 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 5 + 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, []
@ -53,7 +58,9 @@ 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, []
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, []
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):int]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([2, +oo] + 1):int]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 * k.ub, degree = 1]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 13 * k.ub, degree = 1]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202, degree = 0]
@ -69,26 +76,36 @@ 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: ([-oo, +oo] + 1):int]
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):int]
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):int]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
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]):int]
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):int]
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, []
codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: j,Assignment,Assignment,Assignment,Assignment,Binop: ([-oo, 9] + 1):int]
codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1]
codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * (k.ub + -1), 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 6 + 7 * (k.ub + -1), 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]):int]
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):int]
codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 9 * items.length.ub, 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 6 + 9 * items.length.ub, degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
@ -108,9 +125,11 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.
codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(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,ArrayAccess: Offset: [-oo, +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):int]
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]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 * (length.ub + -1), degree = 1]
@ -120,10 +139,13 @@ 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 4 + 76 * (length.ub + -1)^2 + 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 + 76 * (length.ub + -1)^2 + 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 + 76 * (length.ub + -1)^2 + 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, [Binop: (a[*] * b[*]):long]
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 + 76 * (length.ub + -1)^2 + 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 + 76 * (length.ub + -1)^2 + 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 + 76 * (length.ub + -1)^2 + 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):int]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([10, +oo] + 1):int]
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 799, degree = 0]
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]

Write Preview
Loading…
Cancel
Save