From 2a94e907e2ae6a6aad7c0ccf916941efebd566d3 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 29 Nov 2018 10:13:42 -0800 Subject: [PATCH] [inferbo] Revise pp of Symb.partial Reviewed By: mbouaziz Differential Revision: D13253989 fbshipit-source-id: 87a55a764 --- infer/src/bufferoverrun/absLoc.ml | 24 ++++-- infer/src/bufferoverrun/symb.ml | 16 +++- infer/src/bufferoverrun/symb.mli | 2 + .../codetoanalyze/c/bufferoverrun/issues.exp | 14 ++-- .../cpp/bufferoverrun/issues.exp | 80 +++++++++---------- .../cpp/quandaryBO/issues.exp-t4 | 2 +- 6 files changed, 79 insertions(+), 59 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 58c015ba8..edf432871 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -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 diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 5df9a81b9..f657e5c84 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -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 diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 904beab8a..75547782f 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index f8d07ba78..a87794b36 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -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, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,Assignment,Assignment,,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, [,Assignment,,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,,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,,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,,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,,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,,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,,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,,Call,Assignment,Assignment,,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,,Parameter `x`,,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] @@ -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, [,Parameter `len`,,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]] codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 20 Size: 10] -codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x[*].f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2] +codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x->f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 3] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 6 Size: 6] @@ -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, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `arr[*]`,Assignment,,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ] -codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] -codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `*arr`,Assignment,,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ] +codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x->field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x->field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,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, [,Array declaration,Array access: Offset: 10 Size: 10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 6ab4e2642..804232f0d 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,5 +1,5 @@ -INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this[*].infer_size`,,Unknown value from: std::distance_>,Binary operation: (this[*].infer_size - [-oo, +oo]):unsigned64] -INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this[*].infer_size`,,Unknown value from: std::distance_>,Binary operation: (this[*].infer_size + [-oo, +oo]):unsigned64] +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,Binary operation: (this->infer_size - [-oo, +oo]):unsigned64] +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,Binary operation: (this->infer_size + [-oo, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/arith.cpp, 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, [,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, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] -codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Parameter `this[*].arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Parameter `this->arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this[*].children`,Call,,Parameter `nth`,,Parameter `this[*].children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this->children`,Call,,Parameter `nth`,,Parameter `this->children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x[*].b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x->b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,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, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `n`,Assignment,,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `n`,Assignment,,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `n`,Assignment,,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `n`,Assignment,,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] @@ -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, [,Call,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 32 Size: 30] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `__x[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [1, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [1, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 5] @@ -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, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `this[*].infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Call,Parameter `this[*].infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t[*].bI`,Call,Parameter `t[*].bI`,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v[*]._size`,Call,Parameter `this[*]._size`,Call,,Parameter `i`,,Parameter `this[*]._size`,Array declaration,Assignment,Array access: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ] +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,Parameter `this->_size`,Call,,Parameter `i`,,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64] @@ -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, [,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 42 Size: 42] -codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this[*].h`,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->h`,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 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`,Binary operation: (4 × [45, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 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`,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,,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: v[*].infer_size Size: v[*].infer_size] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0[*].a`,Assignment,Call,,Parameter `count`,Call,Parameter `this[*].a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Allocation: Length: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 index 7c4f7cfc1..251199afd 100644 --- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 @@ -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,,Parameter `i`,,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source with tainted data return*,Return from multi_level_source_bad,Call to multi_level_sink_bad with tainted index 0,Call to __array_access with tainted index 0,-----------,Call,Unknown value from: __infer_taint_source,Assignment,Assignment,Call,,Parameter `i`,,Array declaration,Array access: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] -codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Assignment,Call,Parameter `__param_0[*].ind`,Assignment,Call,,Parameter `info[*].ind`,,Parameter `info[*].size`,Array declaration,Array access: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, overlapping_issues_good, 1, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Assignment,Call,Parameter `__param_0->ind`,Assignment,Call,,Parameter `info->ind`,,Parameter `info->size`,Array declaration,Array access: Offset: 10 Size: [0, +oo] by call to `overlapping_issues_sink_good` ]