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

[inferbo] Revise pp of Symb.partial

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D13253989

fbshipit-source-id: 87a55a764
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 485b9c7bf5
commit 2a94e907e2
6 changed files with 79 additions and 59 deletions
Show Stats Download Patch File Download Diff File

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

@ -38,18 +38,21 @@ module Allocsite = struct
Boolean.False
let pp fmt = function
let pp_paren ~paren fmt = function
| Unknown ->
F.fprintf fmt "Unknown"
| Param path ->
Symb.SymbolPath.pp_partial fmt path
Symb.SymbolPath.pp_partial_paren ~paren fmt path
| Known {path= Some path} when Config.bo_debug < 1 ->
Symb.SymbolPath.pp_partial fmt path
Symb.SymbolPath.pp_partial_paren ~paren 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)
Option.iter path ~f:(fun path ->
F.fprintf fmt "(%a)" (Symb.SymbolPath.pp_partial_paren ~paren:false) path )
let pp = pp_paren ~paren:false
let is_pretty = function Param _ | Known {path= Some _} -> true | _ -> false
let to_string x = F.asprintf "%a" pp x
@ -86,7 +89,9 @@ module Loc = struct
let unknown = Allocsite Allocsite.unknown
let rec pp fmt = function
let rec pp_paren ~paren fmt =
let module SP = Symb.SymbolPath in
function
| Var v ->
Var.pp F.str_formatter v ;
let s = F.flush_str_formatter () in
@ -94,10 +99,15 @@ module Loc = struct
F.pp_print_string fmt (String.sub s ~pos:1 ~len:(String.length s - 1))
else F.pp_print_string fmt s
| Allocsite a ->
Allocsite.pp fmt a
Allocsite.pp_paren ~paren fmt a
| Field (Allocsite (Allocsite.Param (SP.Deref (SP.Deref_CPointer, p))), f)
| Field (Allocsite (Allocsite.Known {path= Some (SP.Deref (SP.Deref_CPointer, p))}), f) ->
F.fprintf fmt "%a->%s" (SP.pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string f)
| Field (l, f) ->
F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f
F.fprintf fmt "%a.%a" (pp_paren ~paren:true) l Typ.Fieldname.pp f
let pp = pp_paren ~paren:false
let to_string x = F.asprintf "%a" pp x

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

@ -42,15 +42,23 @@ module SymbolPath = struct
let length p = Length p
let rec pp_partial fmt = function
let rec pp_partial_paren ~paren fmt = function
| Pvar pvar ->
Pvar.pp_value fmt pvar
| Deref (_, p) ->
F.fprintf fmt "%a[*]" pp_partial p
| Deref (Deref_ArrayIndex, p) ->
F.fprintf fmt "%a[*]" (pp_partial_paren ~paren:true) p
| Deref (Deref_CPointer, p) ->
if paren then F.fprintf fmt "(" ;
F.fprintf fmt "*%a" (pp_partial_paren ~paren:false) p ;
if paren then F.fprintf fmt ")"
| Field (fn, Deref (Deref_CPointer, p)) ->
F.fprintf fmt "%a->%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
| Field (fn, p) ->
F.fprintf fmt "%a.%s" pp_partial p (Typ.Fieldname.to_flat_string fn)
F.fprintf fmt "%a.%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
let pp_partial = pp_partial_paren ~paren:false
let pp fmt = function
| Normal p ->
pp_partial fmt p

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

@ -31,6 +31,8 @@ module SymbolPath : sig
val pp_partial : F.formatter -> partial -> unit
val pp_partial_paren : paren:bool -> F.formatter -> partial -> unit
val of_pvar : Pvar.t -> partial
val deref : deref_kind:deref_kind -> partial -> partial

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

@ -3,9 +3,9 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
@ -48,7 +48,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_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 20 Size: 10]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x[*].f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 6 Size: 6]
@ -84,9 +84,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, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `arr[*]`,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x[*].field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x[*].field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]

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

@ -1,5 +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_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Binary operation: (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_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Unknown value from: std::distance<std::__list_iterator<int,_void_*>_>,Binary operation: (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_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Binary operation: (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_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__list_iterator<int,_void_*>_>,Binary operation: (this->infer_size + [-oo, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@ -9,19 +9,19 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVER
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this[*].arr`,Array access: 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,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this->arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this[*].children`,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this[*].children`,Array access: 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`,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this->children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x[*].b`,Array access: 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,<Length trace>,Parameter `x->b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
@ -29,13 +29,13 @@ 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, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
@ -56,15 +56,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, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-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,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v[*]._size`,Call,Parameter `this[*]._size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this[*]._size`,Array declaration,Assignment,Array access: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-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,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,Parameter `this->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64]
@ -72,25 +72,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, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this[*].h`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,<LHS trace>,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):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,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):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,<RHS trace>,Parameter `this->infer_size`,Binary operation: (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,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<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,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: v[*].infer_size Size: v[*].infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Allocation: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, 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,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<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,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

2
infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4
Unescape View File

@ -12,4 +12,4 @@ codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, INFERBO_AL
codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, TAINTED_MEMORY_ALLOCATION, no_bucket, ERROR, [Return from __infer_taint_source,Call to __set_array_length with tainted index 1,-----------,Unknown value from: __infer_taint_source,Assignment,Allocation: Length: [-oo, 2147483647]]
codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: __infer_taint_source,Assignment,Assignment,Call,<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ]
codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source with tainted data return*,Return from multi_level_source_bad,Call to multi_level_sink_bad with tainted index 0,Call to __array_access with tainted index 0,-----------,Call,Unknown value from: __infer_taint_source,Assignment,Assignment,Call,<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ]
codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Assignment,Call,Parameter `__param_0[*].ind`,Assignment,Call,<Offset trace>,Parameter `info[*].ind`,<Length trace>,Parameter `info[*].size`,Array declaration,Array access: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ]
codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Assignment,Call,Parameter `__param_0->ind`,Assignment,Call,<Offset trace>,Parameter `info->ind`,<Length trace>,Parameter `info->size`,Array declaration,Array access: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ]

Write Preview
Loading…
Cancel
Save