From a8dbaf082d374ec971eee6efcbb06828ae3f92eb Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sun, 9 Dec 2018 23:04:06 -0800 Subject: [PATCH] [inferbo] Weak update for array contents Summary: It weakly updates array when there are more than two contents. Reviewed By: mbouaziz Differential Revision: D13318443 fbshipit-source-id: fa740d8b1 --- infer/src/bufferoverrun/absLoc.ml | 34 +++++++++++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 24 ++++++--- .../src/bufferoverrun/bufferOverrunModels.ml | 34 ++++++------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 11 +++- infer/src/bufferoverrun/itv.ml | 2 + infer/src/bufferoverrun/itv.mli | 2 + .../c/bufferoverrun/array_content.c | 51 +++++++++++++++++++ .../c/bufferoverrun/array_multidim.c | 4 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 9 +++- .../cpp/bufferoverrun/issues.exp | 3 +- .../cpp/bufferoverrun/realloc.cpp | 2 +- 11 files changed, 137 insertions(+), 39 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index bb102c161..e46a1a5bd 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -19,6 +19,7 @@ module Allocsite = struct ; node_hash: int ; inst_num: int ; dimension: int + ; represents_multiple_values: bool ; path: Symb.SymbolPath.partial option } [@@deriving compare] @@ -63,9 +64,16 @@ module Allocsite = struct -> inst_num:int -> dimension:int -> path:Symb.SymbolPath.partial option + -> represents_multiple_values:bool -> t = - fun proc_name ~node_hash ~inst_num ~dimension ~path -> - Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension; path} + fun proc_name ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values -> + Known + { proc_name= Typ.Procname.to_string proc_name + ; node_hash + ; inst_num + ; dimension + ; path + ; represents_multiple_values } let make_symbol path = Symbol path @@ -79,6 +87,16 @@ module Allocsite = struct Option.some_if (not (Symb.SymbolPath.represents_callsite_sound_partial path)) path | Unknown | Known _ -> None + + + let represents_multiple_values = function + | Unknown -> + false + | Symbol path -> + Symb.SymbolPath.represents_multiple_values path + | Known {path; represents_multiple_values} -> + represents_multiple_values + || Option.value_map path ~default:false ~f:Symb.SymbolPath.represents_multiple_values end module Loc = struct @@ -179,6 +197,15 @@ module Loc = struct Option.value_map (get_path x) ~default:false ~f:(fun x -> Option.value_map (Symb.SymbolPath.get_pvar x) ~default:false ~f:(fun x -> List.exists formals ~f:(fun (formal, _) -> Pvar.equal x formal) ) ) + + + let rec represents_multiple_values = function + | Var _ -> + false + | Allocsite allocsite -> + Allocsite.represents_multiple_values allocsite + | Field (l, _) -> + represents_multiple_values l end module PowLoc = struct @@ -213,8 +240,7 @@ module PowLoc = struct fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty end -(** unsound but ok for bug catching *) -let always_strong_update = true +let always_strong_update = false let can_strong_update : PowLoc.t -> bool = fun ploc -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9c79c2a93..c420257c8 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -855,14 +855,16 @@ module MemReach = struct let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot - let find_heap : default:Val.t -> Loc.t -> t -> Val.t = + let find_heap_default : default:Val.t -> Loc.t -> t -> Val.t = fun ~default l m -> IOption.value_default_f (find_opt l m) ~f:(fun () -> Option.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) ) + let find_heap : Loc.t -> t -> Val.t = find_heap_default ~default:Val.Itv.top + let find : Loc.t -> t -> Val.t = - fun l m -> if is_stack_loc l m then find_stack l m else find_heap ~default:Val.Itv.top l m + fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m let find_set : PowLoc.t -> t -> Val.t = @@ -933,19 +935,27 @@ module MemReach = struct PowLoc.fold strong_update1 locs m - let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + let transformi_mem : f:(Loc.t -> Val.t -> Val.t) -> PowLoc.t -> t -> t = fun ~f locs m -> let transform_mem1 l m = let add, find = if is_stack_loc l m then (replace_stack, find_stack) - else (add_heap, find_heap ~default:Val.bot) + else (add_heap, find_heap_default ~default:Val.bot) in - add l (f (find l m)) m + add l (f l (find l m)) m in PowLoc.fold transform_mem1 locs m - let weak_update locs v m = transform_mem ~f:(fun v' -> Val.join v' v) locs m + let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + fun ~f -> transformi_mem ~f:(fun _ v -> f v) + + + let weak_update locs v m = + transformi_mem + ~f:(fun l v' -> if Loc.represents_multiple_values l then Val.join v' v else v) + locs m + let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v s -> @@ -1138,8 +1148,6 @@ module Mem = struct let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.strong_update p v) - let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v) - let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t = fun formals locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from formals locs) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index ae363304b..70cc173cf 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -88,17 +88,6 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = PO.ConditionSet.add_alloc_size location ~length traces cond_set -let set_uninitialized location (typ : Typ.t) ploc mem = - match typ.desc with - | Tint _ | Tfloat _ -> - Dom.Mem.weak_update ploc Dom.Val.Itv.top mem - | _ -> - L.(debug BufferOverrun Verbose) - "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp - location ; - mem - - let malloc size_exp = let exec {pname; node_hash; location; tenv; integer_type_widths} ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -106,8 +95,11 @@ let malloc size_exp = let length = Sem.eval integer_type_widths length0 mem in let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let offset, size = (Itv.zero, Dom.Val.get_itv length) in + let allocsite = + let represents_multiple_values = not (Itv.is_one size) in + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path ~represents_multiple_values + in let size_exp_opt = let size_exp = Option.value dyn_length ~default:length0 in Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp @@ -116,7 +108,6 @@ let malloc size_exp = mem |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt - |> set_uninitialized location typ (Dom.Val.get_array_locs v) |> BoUtils.Exec.init_array_fields tenv integer_type_widths pname path ~node_hash typ (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size size_exp in @@ -251,17 +242,19 @@ let get_array_length array_exp = let set_array_length array length_exp = let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = match array with - | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> + | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {stride}} -> let length = Sem.eval integer_type_widths length_exp mem in let stride = Option.map ~f:IntLit.to_int_exn stride in let path = Some (Symb.SymbolPath.of_pvar array_pvar) in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in let size = Dom.Val.get_itv length in + let allocsite = + let represents_multiple_values = not (Itv.is_one size) in + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path + ~represents_multiple_values + in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in - mem - |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v - |> set_uninitialized location elt (Dom.Val.get_array_locs v) + Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem | _ -> L.(die InternalError) "Unexpected type of first argument for __set_array_length() " and check = check_alloc_size length_exp in @@ -386,7 +379,10 @@ module Collection = struct let exec {pname; node_hash; location} ~ret:(id, _) mem = let loc = Loc.of_id id in let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in + let allocsite = + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path + ~represents_multiple_values:true + in let alloc_loc = Loc.of_allocsite allocsite in let init_size = Dom.Val.of_int 0 in let traces = Trace.(Set.singleton location ArrayDeclaration) in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 8c738efee..fdb1c90fc 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -67,7 +67,10 @@ module Exec = struct let offset = Itv.zero in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let path = Loc.get_path loc in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in + let allocsite = + let represents_multiple_values = represents_multiple_values || not (Itv.is_one size) in + Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values + in let mem = let arr = let traces = Trace.(Set.singleton location ArrayDeclaration) in @@ -97,7 +100,9 @@ module Exec = struct -> Dom.Mem.t * int = fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem -> let path = Loc.get_path loc in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in + let allocsite = + Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values:true + in let alloc_loc = Loc.of_allocsite allocsite in let traces = Trace.(Set.singleton location ArrayDeclaration) in let mem = @@ -185,7 +190,9 @@ module Exec = struct in let stride = Option.map stride ~f:IntLit.to_int_exn in let allocsite = + let represents_multiple_values = not (Itv.is_one length) in Allocsite.make pname ~node_hash ~inst_num ~dimension ~path:field_path + ~represents_multiple_values in let offset, size = (Itv.zero, length) in let v = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 49d36a8f2..e3479dddf 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -559,6 +559,8 @@ let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv let is_const : t -> Z.t option = bind1zo ItvPure.is_const +let is_one = bind1bool ItvPure.is_one + let is_mone = bind1bool ItvPure.is_mone let eq_const : Z.t -> t -> bool = fun z -> bind1bool (ItvPure.eq_const z) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index b228e6dbd..c675e3089 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -137,6 +137,8 @@ val of_int64 : Int64.t -> t val is_const : t -> Z.t option +val is_one : t -> bool + val is_mone : t -> bool val eq_const : Z.t -> t -> bool diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index 03f6df90a..e8ece35c7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -52,3 +52,54 @@ void call_array_min_index_from_one_good() { int a[2]; a[array_min_index_from_one_FP(a, 2) - 1] = 0; } + +void weak_update_Good_FP() { + int a[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 15}; + a[a[3]] = 3; +} + +void weak_update_Bad() { + int a[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + if (a[0] == 0) { + a[15] = 1; + } +} + +void strong_update_malloc_Good() { + int a[10]; + int* x = (int*)malloc(sizeof(int)); + *x = 10; + *x = 0; + a[*x] = 0; +} + +void strong_update_malloc_Bad() { + int a[10]; + int* x = (int*)malloc(sizeof(int)); + *x = 0; + *x = 10; + a[*x] = 0; +} + +void weak_update_malloc_Good_FP() { + int a[10]; + int* x = (int*)malloc(sizeof(int) * 2); + x[0] = 0; + x[1] = 10; + a[x[0]] = 0; +} + +void weak_update_malloc_Bad() { + int a[10]; + int* x = (int*)malloc(sizeof(int) * 2); + x[0] = 0; + x[1] = 10; + a[x[1]] = 0; +} + +void weak_update_malloc2_Bad_FN() { + int a[10]; + int* x = (int*)malloc(sizeof(int) * 2); + x[0] = 0; + a[x[1]] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c index 631dc866b..b258177ec 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c @@ -57,7 +57,7 @@ void multidim_arr5_Bad() { a[0][10] = 0; } -void multidim_arr6_Good() { +void multidim_arr6_Good_FP() { int a[3][2]; int b[10]; int* p = a; @@ -65,7 +65,7 @@ void multidim_arr6_Good() { b[a[0][0]] = 1; } -void multidim_arr6_Bad_FN() { +void multidim_arr6_Bad() { int a[3][2]; int b[5]; int* p = a; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index e5b9f1cde..d8485fb8a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -46,13 +46,20 @@ codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, C codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_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_content.c, strong_update_malloc_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 15 Size: 10] +codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 15] Size: 10] +codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Good_FP, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] 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, array_field_access_Bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `y.f[*]`,,Array declaration,Array access: Offset: [min(20, y.f[*]), max(20, y.f[*])] 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_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] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr6_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr6_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 10] codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Array declaration,Assignment,Assignment,Array access: Offset: 999999999 Size: 26460] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 06328027b..0da5151af 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -38,7 +38,6 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt 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] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 7 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] @@ -80,7 +79,7 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, 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 `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`,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`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: 10 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`,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`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,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`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp index 17e747344..4ffea879d 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp @@ -20,7 +20,7 @@ void realloc_Bad() { buf2[buf2[0]] = 0; } -void realloc_Good_FP() { +void realloc2_Good() { int* buf1 = (int*)malloc(2 * sizeof(int)); for (int i = 0; i < 2; i++) { buf1[i] = 3;