[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<int> v) {
    if (v.size() >= 10) {
      v[9] = 1; // error: BUFFER_OVERRUN Offset: [9, 9] Size: [5, 5]
    }
  }
  void call_safe_access_Good() {
    std::vector<int> 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

@@ -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

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
+       -> let subst_map, ret_alias =
-          instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem loc
+            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
       | _

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 "@[<v 0>Logical Variables :@,"; *)
       F.fprintf fmt "@[<hov 2>{ @," ;
       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 =
+  let load : Ident.t -> Loc.t -> t -> t = fun id loc m -> M.add id loc m
-    fun id exp m -> match exp with Exp.Lvar x -> M.add id x m | _ -> m
 
-  let store : Exp.t -> Exp.t -> t -> t =
+  let store : Loc.t -> Exp.t -> t -> t = fun l _ m -> M.filter (fun _ y -> not (Loc.equal l y)) m
-    fun e _ m -> match e with Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m | _ -> 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 =
+  let find_ret_alias : t -> Loc.t option = fun m -> Alias.find_ret m.alias
-    fun id e m -> {m with alias= Alias.load id e m.alias}
 
-  let store_alias : Exp.t -> Exp.t -> t -> t =
+  let load_alias : Ident.t -> Loc.t -> t -> t =
-    fun e1 e2 m -> {m with alias= Alias.store e1 e2 m.alias}
+    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)
 

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
+        | Some loc
-         -> Var.of_pvar pvar |> Loc.of_var |> PowLoc.singleton |> Val.of_pow_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'
+        | Some lv
-         -> let lv = Loc.of_pvar x' in
+         -> let v = Mem.find_heap lv mem in
-            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'
+        | Some lv
-         -> let lv = Loc.of_pvar x' in
+         -> let v = Mem.find_heap lv mem in
-            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'
+        | Some lv
-         -> let lv = Loc.of_pvar x' in
+         -> let v = Mem.find_heap lv mem in
-            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'
+        | Some lv
-         -> let lv = Loc.of_pvar x' in
+         -> let v = Mem.find_heap lv mem in
-            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'
+        | Some lv
-         -> let lv = Loc.of_pvar x' in
+         -> let v = Mem.find_heap lv mem in
-            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 =
+        -> callee_ret_alias:Loc.t option
-    fun tenv formal actual typ caller_mem callee_mem ->
+        -> (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 =
+      let append_field v fn = PowLoc.append_field (Val.get_all_locs v) fn in
-        Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem
+      let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in
-      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
+      : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
-        -> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t =
+        -> callee_ret_alias:Loc.t option -> Location.t
-    fun tenv callee_pdesc params caller_mem callee_entry_mem loc ->
+        -> (Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) * Loc.t option =
-      let add_pair (formal, typ) actual l =
+    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
+        let new_matching, ret_alias' =
-        List.rev_append new_matching l
+          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:[]
+      let pairs, ret_alias =
-      |> subst_map_of_pairs
+        list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None)
+      in
+      (subst_map_of_pairs pairs, ret_alias)
 end

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]]

infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp

@@ -44,6 +44,33 @@ void reserve_Bad() {
   v[0] = 2;
 }
 
+void safe_access(std::vector<int> v) {
+  if (v.size() >= 10) {
+    v[9] = 1;
+  }
+}
+
+void call_safe_access_Good() {
+  std::vector<int> v(5, 0);
+  safe_access(v);
+}
+
+void safe_access2(std::vector<int> 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<int> v;
+  safe_access2(v);
+}
+
 struct Int_no_copy {
   Int_no_copy(Int_no_copy&) = delete;
   Int_no_copy(const Int_no_copy&) = delete;