From 1531a3d538fe9345bc53d8c66a6bb96f77da7dba Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 12 Jul 2017 06:27:44 -0700 Subject: [PATCH] [inferbo] Pruning return value of function call Summary: Problem: The analyzer did not know that the value of `v.size()` is an alias of `v.infer_size`, so `v.infer_size` is not pruned by the if condition. As a result it raises a false alarm. void safe_access(std::vector v) { if (v.size() >= 10) { v[9] = 1; // error: BUFFER_OVERRUN Offset: [9, 9] Size: [5, 5] } } void call_safe_access_Good() { std::vector v(5, 0); safe_access(v); } Solution: Adding alias for return value to the abstract domain. Now Inferbo can prune `v.infer_size` because it knows that the value of `v.size()` is an alias of `v.infer_size`. There is already an alias domain in Inferbo, so we added a specific room for the retrun value. Reviewed By: jvillard, mbouaziz Differential Revision: D5396988 fbshipit-source-id: 4a4702c --- infer/src/bufferoverrun/absLoc.ml | 4 + .../src/bufferoverrun/bufferOverrunChecker.ml | 25 ++++- .../src/bufferoverrun/bufferOverrunDomain.ml | 106 +++++++++++++++--- .../bufferoverrun/bufferOverrunSemantics.ml | 78 +++++++------ .../cpp/bufferoverrun/issues.exp | 1 + .../cpp/bufferoverrun/vector.cpp | 27 +++++ 6 files changed, 185 insertions(+), 56 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 3005469be..19b556686 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -30,6 +30,8 @@ module Loc = struct | Field of t * Typ.Fieldname.t [@@deriving compare] + let equal = [%compare.equal : t] + let unknown = Allocsite Allocsite.unknown let rec pp fmt = function @@ -81,4 +83,6 @@ module PowLoc = struct let append_field ploc fn = if is_bot ploc then singleton Loc.unknown else fold (fun l -> add (Loc.append_field l fn)) ploc empty + + let is_singleton x = Int.equal (cardinal x) 1 end diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5ff7d1694..3fefc484b 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -242,12 +242,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc) |> fst - let instantiate_ret ret callee_pname callee_exit_mem subst_map mem loc = + let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias loc = match ret with | Some (id, _) -> let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in let ret_var = Loc.of_var (Var.of_id id) in + let add_ret_alias l = Dom.Mem.load_alias id l mem in + let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in Dom.Val.subst ret_val subst_map loc |> Dom.Val.add_trace_elem (Trace.Return loc) |> Fn.flip (Dom.Mem.add_stack ret_var) mem | None @@ -298,10 +300,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct fun tenv ret callee_pdesc callee_pname params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_exit_mem = Dom.Summary.get_output summary in + let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in match callee_pdesc with | Some pdesc - -> let subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc in - instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem loc + -> let subst_map, ret_alias = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc + in + instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias loc |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc | None -> caller_mem @@ -325,11 +330,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in let v = Dom.Mem.find_heap_set locs mem in if Ident.is_none id then mem - else Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem |> Dom.Mem.load_alias id exp + else + let mem = Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem in + if PowLoc.is_singleton locs then Dom.Mem.load_alias id (PowLoc.choose locs) mem + else mem | Store (exp1, _, exp2, loc) -> let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in - Dom.Mem.update_mem locs v mem |> Dom.Mem.store_alias exp1 exp2 + let mem = Dom.Mem.update_mem locs v mem in + if PowLoc.is_singleton locs then Dom.Mem.store_alias (PowLoc.choose locs) exp2 mem + else mem | Prune (exp, loc, _, _) -> Sem.prune exp loc mem | Call (ret, Const Cfun callee_pname, params, loc, _) -> ( @@ -432,7 +442,10 @@ module Report = struct let callee_cond = Dom.Summary.get_cond_set summary in match callee_pdesc with | Some pdesc - -> let subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc in + -> let subst_map, _ = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None + loc + in let pname = Procdesc.get_proc_name pdesc in Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc | _ diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5fa173989..6519c5a03 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -502,10 +502,10 @@ module Heap = struct if is_empty mem then Val.bot else snd (choose mem) end -module Alias = struct +module AliasMap = struct module M = Caml.Map.Make (Ident) - type t = Pvar.t M.t + type t = Loc.t M.t type astate = t @@ -514,7 +514,7 @@ module Alias = struct let ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> let is_in_rhs k v = - match M.find k rhs with v' -> Pvar.equal v v' | exception Not_found -> false + match M.find k rhs with v' -> Loc.equal v v' | exception Not_found -> false in M.for_all is_in_rhs lhs @@ -527,7 +527,7 @@ module Alias = struct | Some v, None | None, Some v -> Some v | Some v1, Some v2 - -> if Pvar.equal v1 v2 then Some v1 else assert false + -> if Loc.equal v1 v2 then Some v1 else assert false in M.merge join_v x y @@ -537,25 +537,91 @@ module Alias = struct let pp : F.formatter -> t -> unit = fun fmt x -> let pp_sep fmt () = F.fprintf fmt ", @," in - let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v in + let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k Loc.pp v in (* F.fprintf fmt "@[Logical Variables :@,"; *) F.fprintf fmt "@[{ @," ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; F.fprintf fmt " }@]" ; F.fprintf fmt "@]" - let load : Ident.t -> Exp.t -> t -> t = - fun id exp m -> match exp with Exp.Lvar x -> M.add id x m | _ -> m + let load : Ident.t -> Loc.t -> t -> t = fun id loc m -> M.add id loc m - let store : Exp.t -> Exp.t -> t -> t = - fun e _ m -> match e with Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m | _ -> m + let store : Loc.t -> Exp.t -> t -> t = fun l _ m -> M.filter (fun _ y -> not (Loc.equal l y)) m - let find : Ident.t -> t -> Pvar.t option = + let find : Ident.t -> t -> Loc.t option = fun k m -> try Some (M.find k m) with Not_found -> None end +module AliasRet = struct + type astate = Bot | L of Loc.t | Top + + let bot = Bot + + let ( <= ) : lhs:astate -> rhs:astate -> bool = + fun ~lhs ~rhs -> + match (lhs, rhs) with + | Bot, _ | _, Top + -> true + | Top, _ | _, Bot + -> false + | L loc1, L loc2 + -> Loc.equal loc1 loc2 + + let join : astate -> astate -> astate = + fun x y -> + match (x, y) with + | Top, _ | _, Top + -> Top + | Bot, a | a, Bot + -> a + | L loc1, L loc2 + -> if Loc.equal loc1 loc2 then x else Top + + let widen : prev:astate -> next:astate -> num_iters:int -> astate = + fun ~prev ~next ~num_iters:_ -> join prev next + + let pp : F.formatter -> astate -> unit = + fun fmt x -> + match x with + | Top + -> F.fprintf fmt "T" + | L loc + -> Loc.pp fmt loc + | Bot + -> F.fprintf fmt "_|_" + + let find : astate -> Loc.t option = fun x -> match x with L loc -> Some loc | _ -> None +end + +module Alias = struct + include AbstractDomain.Pair (AliasMap) (AliasRet) + + let bot : astate = (AliasMap.bot, AliasRet.bot) + + let lift : (AliasMap.astate -> AliasMap.astate) -> astate -> astate = + fun f a -> (f (fst a), snd a) + + let lift_v : (AliasMap.astate -> 'a) -> astate -> 'a = fun f a -> f (fst a) + + let find : Ident.t -> astate -> Loc.t option = fun x -> lift_v (AliasMap.find x) + + let find_ret : astate -> Loc.t option = fun x -> AliasRet.find (snd x) + + let load : Ident.t -> Loc.t -> astate -> astate = fun id loc -> lift (AliasMap.load id loc) + + let store : Loc.t -> Exp.t -> astate -> astate = + fun loc e a -> + let a = lift (AliasMap.store loc e) a in + match e with + | Exp.Var l when Loc.is_return loc + -> let update_ret retl = (fst a, AliasRet.L retl) in + Option.value_map (find l a) ~default:a ~f:update_ret + | _ + -> a +end + module MemReach = struct type astate = {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate} @@ -605,13 +671,15 @@ module MemReach = struct let find_set : PowLoc.t -> t -> Val.t = fun k m -> Val.join (find_stack_set k m) (find_heap_set k m) - let find_alias : Ident.t -> t -> Pvar.t option = fun k m -> Alias.find k m.alias + let find_alias : Ident.t -> t -> Loc.t option = fun k m -> Alias.find k m.alias - let load_alias : Ident.t -> Exp.t -> t -> t = - fun id e m -> {m with alias= Alias.load id e m.alias} + let find_ret_alias : t -> Loc.t option = fun m -> Alias.find_ret m.alias - let store_alias : Exp.t -> Exp.t -> t -> t = - fun e1 e2 m -> {m with alias= Alias.store e1 e2 m.alias} + let load_alias : Ident.t -> Loc.t -> t -> t = + fun id loc m -> {m with alias= Alias.load id loc m.alias} + + let store_alias : Loc.t -> Exp.t -> t -> t = + fun loc e m -> {m with alias= Alias.store loc e m.alias} let add_stack : Loc.t -> Val.t -> t -> t = fun k v m -> {m with stack= Stack.add k v m.stack} @@ -684,12 +752,14 @@ module Mem = struct let find_set : PowLoc.t -> t -> Val.t = fun k -> f_lift_default Val.bot (MemReach.find_set k) - let find_alias : Ident.t -> t -> Pvar.t option = + let find_alias : Ident.t -> t -> Loc.t option = fun k -> f_lift_default None (MemReach.find_alias k) - let load_alias : Ident.t -> Exp.t -> t -> t = fun id e -> f_lift (MemReach.load_alias id e) + let find_ret_alias : t -> Loc.t option = f_lift_default None MemReach.find_ret_alias + + let load_alias : Ident.t -> Loc.t -> t -> t = fun id loc -> f_lift (MemReach.load_alias id loc) - let store_alias : Exp.t -> Exp.t -> t -> t = fun e1 e2 -> f_lift (MemReach.store_alias e1 e2) + let store_alias : Loc.t -> Exp.t -> t -> t = fun loc e -> f_lift (MemReach.store_alias loc e) let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_stack k v) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 52804c1f6..eb767e0e0 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -79,7 +79,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.Var x1, Exp.Var x2 -> ( match (Mem.find_alias x1 m, Mem.find_alias x2 m) with | Some x1', Some x2' - -> Pvar.equal x1' x2' + -> Loc.equal x1' x2' | _, _ -> false ) | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) @@ -275,8 +275,8 @@ module Make (CFG : ProcCfg.S) = struct match exp with | Exp.Var id -> ( match Mem.find_alias id mem with - | Some pvar - -> Var.of_pvar pvar |> Loc.of_var |> PowLoc.singleton |> Val.of_pow_loc + | Some loc + -> PowLoc.singleton loc |> Val.of_pow_loc | None -> Val.bot ) | Exp.Lvar pvar @@ -315,18 +315,16 @@ module Make (CFG : ProcCfg.S) = struct match e with | Exp.Var x -> ( match Mem.find_alias x mem with - | Some x' - -> let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in + | Some lv + -> let v = Mem.find_heap lv mem in let v' = Val.prune_zero v in Mem.update_mem (PowLoc.singleton lv) v' mem | None -> mem ) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( match Mem.find_alias x mem with - | Some x' - -> let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in + | Some lv + -> let v = Mem.find_heap lv mem in let itv_v = if Itv.is_bot (Val.get_itv v) then Itv.bot else Itv.false_sem in let v' = Val.modify_itv itv_v v in Mem.update_mem (PowLoc.singleton lv) v' mem @@ -343,27 +341,24 @@ module Make (CFG : ProcCfg.S) = struct | Exp.BinOp ((Binop.Le as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( match Mem.find_alias x mem with - | Some x' - -> let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in + | Some lv + -> let v = Mem.find_heap lv mem in let v' = Val.prune_comp comp v (eval e' mem loc) in Mem.update_mem (PowLoc.singleton lv) v' mem | None -> mem ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( match Mem.find_alias x mem with - | Some x' - -> let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in + | Some lv + -> let v = Mem.find_heap lv mem in let v' = Val.prune_eq v (eval e' mem loc) in Mem.update_mem (PowLoc.singleton lv) v' mem | None -> mem ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( match Mem.find_alias x mem with - | Some x' - -> let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in + | Some lv + -> let v = Mem.find_heap lv mem in let v' = Val.prune_ne v (eval e' mem loc) in Mem.update_mem (PowLoc.singleton lv) v' mem | None @@ -424,16 +419,26 @@ module Make (CFG : ProcCfg.S) = struct let get_matching_pairs : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate - -> (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list = - fun tenv formal actual typ caller_mem callee_mem -> + -> callee_ret_alias:Loc.t option + -> (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list * Loc.t option = + fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> let get_itv v = Val.get_itv v in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_field_name (fn, _, _) = fn in - let deref_field v fn mem = - Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem - in + let append_field v fn = PowLoc.append_field (Val.get_all_locs v) fn in + let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in + let ret_alias = ref None in + let add_ret_alias v1 v2 = + match callee_ret_alias with + | Some ret_loc + -> if PowLoc.is_singleton v1 && PowLoc.is_singleton v2 + && Loc.equal (PowLoc.choose v1) ret_loc + then ret_alias := Some (PowLoc.choose v2) + | None + -> () + in let add_pair_itv itv1 itv2 traces l = let open Itv in if itv1 <> bot && itv1 <> top && itv2 <> bot then (lb itv1, lb itv2, traces) @@ -443,16 +448,19 @@ module Make (CFG : ProcCfg.S) = struct else l in let add_pair_val v1 v2 pairs = + add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) in let add_pair_field v1 v2 pairs fn = + add_ret_alias (append_field v1 fn) (append_field v2 fn) ; let v1' = deref_field v1 fn callee_mem in let v2' = deref_field v2 fn caller_mem in add_pair_val v1' v2' pairs in let add_pair_ptr typ v1 v2 pairs = + add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; match typ.Typ.desc with | Typ.Tptr ({desc= Tstruct typename}, _) -> ( match Tenv.lookup tenv typename with @@ -468,7 +476,8 @@ module Make (CFG : ProcCfg.S) = struct | _ -> pairs in - [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual + let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in + (pairs, !ret_alias) let subst_map_of_pairs : (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list @@ -504,16 +513,21 @@ module Make (CFG : ProcCfg.S) = struct -> list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) let get_subst_map - : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> Location.t - -> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t = - fun tenv callee_pdesc params caller_mem callee_entry_mem loc -> - let add_pair (formal, typ) actual l = + : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate + -> callee_ret_alias:Loc.t option -> Location.t + -> (Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) * Loc.t option = + fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc -> + let add_pair (formal, typ) actual (l, ret_alias) = let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in - let new_matching = get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem in - List.rev_append new_matching l + let new_matching, ret_alias' = + get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias + in + (List.rev_append new_matching l, Option.first_some ret_alias ret_alias') in let formals = get_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in - list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:[] - |> subst_map_of_pairs + let pairs, ret_alias = + list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) + in + (subst_map_of_pairs pairs, ret_alias) end diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index d67d76428..cefb94eaa 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -13,6 +13,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAcce codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access2_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, 0] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:65:5 by call `safe_access2()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 37368f99b..de8bdbd32 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -44,6 +44,33 @@ void reserve_Bad() { v[0] = 2; } +void safe_access(std::vector v) { + if (v.size() >= 10) { + v[9] = 1; + } +} + +void call_safe_access_Good() { + std::vector v(5, 0); + safe_access(v); +} + +void safe_access2(std::vector v) { + if (v.empty()) { + return; + } + + unsigned int a[v.size()]; + for (unsigned int i = 0; i < v.size(); i++) { + a[i] = 0; + } +} + +void call_safe_access2_Good_FP() { + std::vector v; + safe_access2(v); +} + struct Int_no_copy { Int_no_copy(Int_no_copy&) = delete; Int_no_copy(const Int_no_copy&) = delete;