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

[inferbo] Use set instead of list on get_symbols

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D12855522

fbshipit-source-id: 4e916654c
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 8a51a70162
commit 9e9deb93be
11 changed files with 56 additions and 41 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/bufferoverrun/arrayBlk.ml
Unescape View File

@ -65,12 +65,12 @@ module ArrInfo = struct
fun fmt arr -> Format.fprintf fmt "offset : %a, size : %a" Itv.pp arr.offset Itv.pp arr.size fun fmt arr -> Format.fprintf fmt "offset : %a, size : %a" Itv.pp arr.offset Itv.pp arr.size
let get_symbols : t -> Itv.Symbol.t list = let get_symbols : t -> Itv.SymbolSet.t =
fun arr -> fun arr ->
let s1 = Itv.get_symbols arr.offset in let s1 = Itv.get_symbols arr.offset in
let s2 = Itv.get_symbols arr.size in let s2 = Itv.get_symbols arr.size in
let s3 = Itv.get_symbols arr.stride in let s3 = Itv.get_symbols arr.stride in
List.concat [s1; s2; s3] Itv.SymbolSet.union3 s1 s2 s3
let normalize : t -> t = let normalize : t -> t =
@ -145,8 +145,9 @@ let subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate =
fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
let get_symbols : astate -> Itv.Symbol.t list = let get_symbols : astate -> Itv.SymbolSet.t =
fun a -> List.concat_map ~f:(fun (_, ai) -> ArrInfo.get_symbols ai) (bindings a) fun a ->
fold (fun _ ai acc -> Itv.SymbolSet.union acc (ArrInfo.get_symbols ai)) a Itv.SymbolSet.empty
let normalize : astate -> astate = fun a -> map ArrInfo.normalize a let normalize : astate -> astate = fun a -> map ArrInfo.normalize a

10
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -139,8 +139,8 @@ module SymLinear = struct
Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s') Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s')
let get_symbols : t -> Symb.Symbol.t list = let get_symbols : t -> Symb.SymbolSet.t =
fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x [] fun x -> M.fold (fun symbol _coeff acc -> Symb.SymbolSet.add symbol acc) x Symb.SymbolSet.empty
(* we can give integer bounds (obviously 0) only when all symbols are unsigned *) (* we can give integer bounds (obviously 0) only when all symbols are unsigned *)
@ -773,13 +773,13 @@ module Bound = struct
let div_const_u = div_const Symb.BoundEnd.UpperBound let div_const_u = div_const Symb.BoundEnd.UpperBound
let get_symbols : t -> Symb.Symbol.t list = function let get_symbols : t -> Symb.SymbolSet.t = function
| MInf | PInf -> | MInf | PInf ->
[] Symb.SymbolSet.empty
| Linear (_, se) -> | Linear (_, se) ->
SymLinear.get_symbols se SymLinear.get_symbols se
| MinMax (_, _, _, _, s) -> | MinMax (_, _, _, _, s) ->
[s] Symb.SymbolSet.singleton s
let are_similar b1 b2 = let are_similar b1 b2 =

2
infer/src/bufferoverrun/bounds.mli
Unescape View File

@ -103,7 +103,7 @@ module Bound : sig
val div_const_u : t -> Ints.NonZeroInt.t -> t sexp_option val div_const_u : t -> Ints.NonZeroInt.t -> t sexp_option
val get_symbols : t -> Symb.Symbol.t list val get_symbols : t -> Symb.SymbolSet.t
val are_similar : t -> t -> bool val are_similar : t -> t -> bool

10
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -285,8 +285,8 @@ module Val = struct
{bot with itv; traces= TraceSet.join x.traces y.traces} {bot with itv; traces= TraceSet.join x.traces y.traces}
let get_symbols : t -> Itv.Symbol.t list = let get_symbols : t -> Itv.SymbolSet.t =
fun x -> List.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk) fun x -> Itv.SymbolSet.union (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk)
let normalize : t -> t = let normalize : t -> t =
@ -301,9 +301,9 @@ module Val = struct
fun x (eval_sym, trace_of_sym) location -> fun x (eval_sym, trace_of_sym) location ->
let symbols = get_symbols x in let symbols = get_symbols x in
let traces_caller = let traces_caller =
List.fold symbols Itv.SymbolSet.fold
~f:(fun traces symbol -> TraceSet.join (trace_of_sym symbol) traces) (fun symbol traces -> TraceSet.join (trace_of_sym symbol) traces)
~init:TraceSet.empty symbols TraceSet.empty
in in
let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in
{x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}

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

@ -108,7 +108,8 @@ module ArrayAccessCondition = struct
[@@deriving compare] [@@deriving compare]
let get_symbols c = let get_symbols c =
ItvPure.get_symbols c.offset @ ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size Symb.SymbolSet.union3 (ItvPure.get_symbols c.offset) (ItvPure.get_symbols c.idx)
(ItvPure.get_symbols c.size)
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
@ -325,7 +326,7 @@ module BinaryOperationCondition = struct
; lhs: ItvPure.astate ; lhs: ItvPure.astate
; rhs: ItvPure.astate } ; rhs: ItvPure.astate }
let get_symbols c = ItvPure.get_symbols c.lhs @ ItvPure.get_symbols c.rhs let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs)
let subst eval_sym c = let subst eval_sym c =
match (ItvPure.subst c.lhs eval_sym, ItvPure.subst c.rhs eval_sym) with match (ItvPure.subst c.lhs eval_sym, ItvPure.subst c.rhs eval_sym) with
@ -675,7 +676,7 @@ module ConditionWithTrace = struct
let subst (eval_sym, trace_of_sym) rel_map caller_relation callee_pname call_site cwt = let subst (eval_sym, trace_of_sym) rel_map caller_relation callee_pname call_site cwt =
let symbols = Condition.get_symbols cwt.cond in let symbols = Condition.get_symbols cwt.cond in
if List.is_empty symbols then if Symb.SymbolSet.is_empty symbols then
L.(die InternalError) L.(die InternalError)
"Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \ "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
the first place?" the first place?"
@ -685,8 +686,9 @@ module ConditionWithTrace = struct
None None
| Some cond -> | Some cond ->
let traces_caller = let traces_caller =
List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> Symb.SymbolSet.fold
ValTraceSet.join (trace_of_sym symbol) val_traces ) (fun symbol val_traces -> ValTraceSet.join (trace_of_sym symbol) val_traces)
symbols ValTraceSet.empty
in in
let trace = let trace =
ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace

10
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -29,9 +29,9 @@ module Boolean = struct
end end
open Ints open Ints
module Symbol = Symb.Symbol
module SymbolPath = Symb.SymbolPath module SymbolPath = Symb.SymbolPath
module SymbolTable = Symb.SymbolTable module SymbolTable = Symb.SymbolTable
module SymbolSet = Symb.SymbolSet
(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *)
module NonNegativeBound = struct module NonNegativeBound = struct
@ -797,8 +797,8 @@ module ItvPure = struct
if is_invalid (l, u) then NonBottom x else if Bound.eq l u then prune_diff x l else NonBottom x if is_invalid (l, u) then NonBottom x else if Bound.eq l u then prune_diff x l else NonBottom x
let get_symbols : t -> Symbol.t list = let get_symbols : t -> SymbolSet.t =
fun (l, u) -> List.append (Bound.get_symbols l) (Bound.get_symbols u) fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u)
let make_positive : t -> t = let make_positive : t -> t =
@ -978,9 +978,9 @@ let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t =
fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x
let get_symbols : t -> Symbol.t list = function let get_symbols : t -> SymbolSet.t = function
| Bottom -> | Bottom ->
[] SymbolSet.empty
| NonBottom x -> | NonBottom x ->
ItvPure.get_symbols x ItvPure.get_symbols x

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

@ -25,9 +25,9 @@ module Boolean : sig
val is_true : t -> bool val is_true : t -> bool
end end
module Symbol = Symb.Symbol
module SymbolPath = Symb.SymbolPath module SymbolPath = Symb.SymbolPath
module SymbolTable = Symb.SymbolTable module SymbolTable = Symb.SymbolTable
module SymbolSet = Symb.SymbolSet
module NonNegativePolynomial : sig module NonNegativePolynomial : sig
include AbstractDomain.WithTop include AbstractDomain.WithTop
@ -134,7 +134,7 @@ module ItvPure : sig
| `LeftSubsumesRight | `LeftSubsumesRight
| `RightSubsumesLeft ] | `RightSubsumesLeft ]
val get_symbols : t -> Symbol.t list val get_symbols : t -> SymbolSet.t
val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted
@ -197,7 +197,7 @@ val neg : t -> t
val normalize : t -> t val normalize : t -> t
val get_symbols : t -> Symbol.t list val get_symbols : t -> SymbolSet.t
val eq : t -> t -> bool val eq : t -> t -> bool

6
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -106,6 +106,12 @@ module SymbolTable = struct
s s
end end
module SymbolSet = struct
include PrettyPrintable.MakePPSet (Symbol)
let union3 x y z = union (union x y) z
end
module SymbolMap = struct module SymbolMap = struct
include PrettyPrintable.MakePPMap (Symbol) include PrettyPrintable.MakePPMap (Symbol)

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

@ -53,6 +53,12 @@ module Symbol : sig
val bound_end : t -> BoundEnd.t val bound_end : t -> BoundEnd.t
end end
module SymbolSet : sig
include PrettyPrintable.PPSet with type elt = Symbol.t
val union3 : t -> t -> t -> t
end
module SymbolMap : sig module SymbolMap : sig
include PrettyPrintable.PPMap with type key = Symbol.t include PrettyPrintable.PPMap with type key = Symbol.t

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

@ -57,7 +57,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ]
codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]

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

@ -20,7 +20,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1,
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 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/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]
@ -43,12 +43,12 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_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/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):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned64]
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, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64]
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):signed32] 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):signed32]
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, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Call,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903]
@ -61,10 +61,10 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERR
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/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/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned64]
@ -74,11 +74,11 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVER
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Binop: (4 * [45, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Binop: (4 * [45, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 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]):unsigned64] 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]):unsigned64]
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, 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,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Parameter: count,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Parameter: count,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []

Write Preview
Loading…
Cancel
Save