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

[inferbo] Pretty-print more abstract locations

Browse Source 
Reviewed By: ezgicicek

Differential Revision: D13114228

fbshipit-source-id: 9f4b16817
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 1a3c29b7c7
commit 8fcbfcb741
6 changed files with 58 additions and 52 deletions
Show Stats Download Patch File Download Diff File

17
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -24,10 +24,15 @@ module Allocsite = struct
let pp fmt = function let pp fmt = function
| Unknown -> | Unknown ->
F.fprintf fmt "Unknown" F.fprintf fmt "Unknown"
| Known {proc_name : string; node_hash : int; inst_num : int; dimension : int} -> | Known {path= Some path} when Config.bo_debug < 1 ->
F.fprintf fmt "%s-%d-%d-%d" proc_name node_hash inst_num dimension Symb.SymbolPath.pp_partial fmt path
| Known {proc_name; node_hash; inst_num; dimension; path} ->
F.fprintf fmt "%s-%d-%d-%d" proc_name node_hash inst_num dimension ;
Option.iter path ~f:(fun path -> F.fprintf fmt "(%a)" Symb.SymbolPath.pp_partial path)
let is_pretty = function Known {path= Some _} -> true | _ -> false
let to_string x = F.asprintf "%a" pp x let to_string x = F.asprintf "%a" pp x
let make : let make :
@ -71,13 +76,13 @@ module Loc = struct
let is_var = function Var _ -> true | _ -> false let is_var = function Var _ -> true | _ -> false
let rec contains_allocsite = function let rec is_pretty = function
| Var _ -> | Var _ ->
false
| Allocsite _ ->
true true
| Allocsite a ->
Allocsite.is_pretty a
| Field (loc, _) -> | Field (loc, _) ->
contains_allocsite loc is_pretty loc
let of_var v = Var v let of_var v = Var v

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

@ -745,11 +745,10 @@ module Report = struct
| Trace.Return location -> | Trace.Return location ->
(Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1) (Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1)
| Trace.SymAssign (loc, location) -> | Trace.SymAssign (loc, location) ->
if Loc.contains_allocsite loc then (* ugly, don't show *) if Loc.is_pretty loc then
(trace, depth)
else
let desc = Format.asprintf "Parameter: %a" Loc.pp loc in let desc = Format.asprintf "Parameter: %a" Loc.pp loc in
(Errlog.make_trace_element depth location desc [] :: trace, depth) (Errlog.make_trace_element depth location desc [] :: trace, depth)
else (trace, depth)
| Trace.UnknownFrom (pname_opt, location) -> | Trace.UnknownFrom (pname_opt, location) ->
let desc = Format.asprintf "Unknown value from: %a" Trace.pp_pname_opt pname_opt in let desc = Format.asprintf "Unknown value from: %a" Trace.pp_pname_opt pname_opt in
(Errlog.make_trace_element depth location desc [] :: trace, depth) (Errlog.make_trace_element depth location desc [] :: trace, depth)

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

@ -27,6 +27,8 @@ module SymbolPath : sig
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit
val pp_partial : F.formatter -> partial -> unit
val of_pvar : Pvar.t -> partial val of_pvar : Pvar.t -> partial
val index : array_kind:c_sym_array_kind -> partial -> partial val index : array_kind:c_sym_array_kind -> partial -> partial

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

@ -35,7 +35,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, COND
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10] codetoanalyze/c/bufferoverrun/array_field.c, 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/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: x[*].f,Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3]
@ -70,9 +70,9 @@ 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, [Here] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,Parameter: arr,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,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,Parameter: x[*].field,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Parameter: x[*].field,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

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

@ -1,23 +1,23 @@
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]):unsigned64] 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, [Parameter: this[*].infer_size,Binop: (this[*].infer_size - [-oo, +oo]):unsigned64]
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]):unsigned64] 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, [Parameter: this[*].infer_size,Binop: (this[*].infer_size + [-oo, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: n,ArrayAccess: Offset: 15 Size: 10 by call to `my_class_access_nth` ] codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Parameter: n,ArrayAccess: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Return,Call,Parameter: nth,ArrayAccess: Offset: 5 Size: 3 by call to `Tree_set_child` ] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter: this[*].children,Return,Call,Parameter: this[*].children,Parameter: nth,ArrayAccess: Offset: 5 Size: 3 by call to `Tree_set_child` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayAccess: Offset: 3 Size: 3 by call to `flexible_array_param_access` ] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: x[*].b,ArrayAccess: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 3] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 3]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Assignment,Call,Parameter: n,Assignment,Return,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Assignment,Call,Parameter: n,Assignment,Return,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter: n,Assignment,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: this[*].arr,Call,Parameter: n,Assignment,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
@ -28,10 +28,10 @@ codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad,
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: (1 - [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: (1 - [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Parameter: __n,Call,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,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/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_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5]
@ -52,15 +52,15 @@ 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, [Here] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
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,Parameter: this[*].infer_size,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,Parameter: __n,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,Parameter: this[*].infer_size,Assignment,Return,Assignment,Return,Assignment,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,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,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, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,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, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter: t[*].bI,Call,Parameter: t[*].bI,Call,Parameter: bi,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,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,Parameter: t[*].bI,Call,Parameter: t[*].bI,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [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, [Parameter: v[*]._size,Call,Parameter: this[*]._size,Call,Parameter: this[*]._size,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 9223372036854775807] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 9223372036854775807]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 9223372036854775807):unsigned64] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 9223372036854775807):unsigned64]
@ -68,25 +68,25 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 18446744073709551615):unsigned64] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 18446744073709551615):unsigned64]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/std_array.cpp, 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/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/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: this[*].h,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/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,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,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,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,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,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,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,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,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):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([3, +oo] + 42):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 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,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<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, 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,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Parameter: __n,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, [Parameter: v[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,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_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Parameter: __param_0[*].a,Assignment,Call,Parameter: count,Call,Parameter: this[*].a,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Parameter: count,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,Parameter: __param_0[*].a,Assignment,Call,Parameter: count,Call,Parameter: this[*].a,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Parameter: __n,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,Parameter: this[*].infer_size,Assignment,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Parameter: __n,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,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Alloc: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

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

@ -144,7 +144,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (a[*] * b[*]):signed64] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a[*],Binop: (a[*] * b[*]):signed64]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]

Write Preview
Loading…
Cancel
Save