diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b4f15db5a..ae7c843b8 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -724,11 +724,145 @@ module Alias = struct let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp) end +module CoreVal = struct + type t = Val.t + + let compare x y = + let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in + if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y) + + + let pp fmt x = F.fprintf fmt "(%a, %a)" Itv.pp (Val.get_itv x) ArrayBlk.pp (Val.get_array_blk x) + + let is_symbolic v = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v) + + let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) +end + +module PruningExp = struct + type t = Unknown | Binop of {bop: Binop.t; lhs: CoreVal.t; rhs: CoreVal.t} [@@deriving compare] + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | _, Unknown -> + true + | Unknown, _ -> + false + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} -> + Binop.equal bop1 bop2 && Val.( <= ) ~lhs:lhs1 ~rhs:lhs2 && Val.( <= ) ~lhs:rhs1 ~rhs:rhs2 + + + let join x y = + match (x, y) with + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} + when Binop.equal bop1 bop2 -> + Binop {bop= bop1; lhs= Val.join lhs1 lhs2; rhs= Val.join rhs1 rhs2} + | _, _ -> + Unknown + + + let widen ~prev ~next ~num_iters = + match (prev, next) with + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} + when Binop.equal bop1 bop2 -> + Binop + { bop= bop1 + ; lhs= Val.widen ~prev:lhs1 ~next:lhs2 ~num_iters + ; rhs= Val.widen ~prev:rhs1 ~next:rhs2 ~num_iters } + | _, _ -> + Unknown + + + let pp fmt x = + match x with + | Unknown -> + F.pp_print_string fmt "Unknown" + | Binop {bop; lhs; rhs} -> + F.fprintf fmt "(%a %s %a)" CoreVal.pp lhs (Binop.str Pp.text bop) CoreVal.pp rhs + + + let make bop ~lhs ~rhs = Binop {bop; lhs; rhs} + + let is_unknown = function Unknown -> true | Binop _ -> false + + let is_symbolic = function + | Unknown -> + false + | Binop {lhs; rhs} -> + CoreVal.is_symbolic lhs || CoreVal.is_symbolic rhs + + + let is_empty = + let le_false v = Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:Itv.zero in + function + | Unknown -> + false + | Binop {bop= Lt; lhs; rhs} -> + le_false (Val.lt_sem lhs rhs) + | Binop {bop= Gt; lhs; rhs} -> + le_false (Val.gt_sem lhs rhs) + | Binop {bop= Le; lhs; rhs} -> + le_false (Val.le_sem lhs rhs) + | Binop {bop= Ge; lhs; rhs} -> + le_false (Val.ge_sem lhs rhs) + | Binop {bop= Eq; lhs; rhs} -> + le_false (Val.eq_sem lhs rhs) + | Binop {bop= Ne; lhs; rhs} -> + le_false (Val.ne_sem lhs rhs) + | Binop _ -> + assert false + + + let subst x eval_sym_trace location = + match x with + | Unknown -> + Unknown + | Binop {bop; lhs; rhs} -> + Binop + { bop + ; lhs= Val.subst lhs eval_sym_trace location + ; rhs= Val.subst rhs eval_sym_trace location } +end + +module PrunedVal = struct + type t = {v: CoreVal.t; pruning_exp: PruningExp.t} [@@deriving compare] + + let ( <= ) ~lhs ~rhs = + Val.( <= ) ~lhs:lhs.v ~rhs:rhs.v && PruningExp.( <= ) ~lhs:lhs.pruning_exp ~rhs:rhs.pruning_exp + + + let join x y = {v= Val.join x.v y.v; pruning_exp= PruningExp.join x.pruning_exp y.pruning_exp} + + let widen ~prev ~next ~num_iters = + { v= Val.widen ~prev:prev.v ~next:next.v ~num_iters + ; pruning_exp= PruningExp.widen ~prev:prev.pruning_exp ~next:next.pruning_exp ~num_iters } + + + let pp fmt x = + CoreVal.pp fmt x.v ; + if not (PruningExp.is_unknown x.pruning_exp) then + F.fprintf fmt " by %a" PruningExp.pp x.pruning_exp + + + let make v pruning_exp = {v; pruning_exp} + + let get_val x = x.v + + let subst {v; pruning_exp} eval_sym_trace location = + { v= Val.subst v eval_sym_trace location + ; pruning_exp= PruningExp.subst pruning_exp eval_sym_trace location } + + + let is_symbolic {v; pruning_exp} = CoreVal.is_symbolic v || PruningExp.is_symbolic pruning_exp + + let is_empty {v; pruning_exp} = CoreVal.is_empty v || PruningExp.is_empty pruning_exp +end + (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses [InvertedMap] because more pruning means smaller abstract states. *) module PrunePairs = struct - include AbstractDomain.InvertedMap (Loc) (Val) + include AbstractDomain.InvertedMap (Loc) (PrunedVal) let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x end @@ -846,21 +980,6 @@ module LatestPrune = struct end module Reachability = struct - module PrunedVal = struct - type t = Val.t - - let compare x y = - let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in - if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y) - - - let pp = Val.pp - - let is_symbolic : t -> bool = fun x -> Itv.is_symbolic x.itv || ArrayBlk.is_symbolic x.arrayblk - - let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) - end - module M = PrettyPrintable.MakePPSet (PrunedVal) type t = M.t @@ -871,9 +990,9 @@ module Reachability = struct reachability. *) let add v x = if PrunedVal.is_symbolic v then M.add v x else x - let make = + let make latest_prune = let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in - function + match latest_prune with | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) -> of_prune_pairs p | LatestPrune.V (_, ptrue, pfalse) -> @@ -885,7 +1004,7 @@ module Reachability = struct let subst x eval_sym_trace location = let exception Unreachable in let subst1 x acc = - let v = Val.subst x eval_sym_trace location in + let v = PrunedVal.subst x eval_sym_trace location in if PrunedVal.is_empty v then raise Unreachable else add v acc in match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable @@ -1089,17 +1208,18 @@ module MemReach = struct let apply_latest_prune : Exp.t -> t -> t = - fun e m -> - match (m.latest_prune, e) with - | LatestPrune.V (x, prunes, _), Exp.Var r - | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( - match find_simple_alias r m with - | Some (Loc.Var (Var.ProgramVar y)) when Pvar.equal x y -> - PrunePairs.fold (fun l v acc -> update_mem (PowLoc.singleton l) v acc) prunes m + let apply1 l v acc = update_mem (PowLoc.singleton l) (PrunedVal.get_val v) acc in + fun e m -> + match (m.latest_prune, e) with + | LatestPrune.V (x, prunes, _), Exp.Var r + | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( + match find_simple_alias r m with + | Some (Loc.Var (Var.ProgramVar y)) when Pvar.equal x y -> + PrunePairs.fold apply1 prunes m + | _ -> + m ) | _ -> - m ) - | _ -> - m + m let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 21f9e6577..0d354fc6e 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -446,8 +446,8 @@ let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_ty module Prune = struct type t = {prune_pairs: PrunePairs.t; mem: Mem.t} - let update_mem_in_prune lv v {prune_pairs; mem} = - let prune_pairs = PrunePairs.add lv v prune_pairs in + let update_mem_in_prune lv v ?(pruning_exp = PruningExp.Unknown) {prune_pairs; mem} = + let prune_pairs = PrunePairs.add lv (PrunedVal.make v pruning_exp) prune_pairs in let mem = Mem.update_mem (PowLoc.singleton lv) v mem in {prune_pairs; mem} @@ -503,25 +503,31 @@ module Prune = struct | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_comp comp v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_comp comp lhs rhs in + let pruning_exp = PruningExp.make comp ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_eq v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_eq lhs rhs in + let pruning_exp = PruningExp.make Binop.Eq ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_ne v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_ne lhs rhs in + let pruning_exp = PruningExp.make Binop.Ne ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index d4a393603..6be3b9b6e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -263,7 +263,7 @@ void unsigned_prune_ge1_Good(unsigned int x, unsigned int y) { } } -void call_unsigned_prune_ge1_Good_FP() { unsigned_prune_ge1_Good(0, 1); } +void call_unsigned_prune_ge1_Good() { unsigned_prune_ge1_Good(0, 1); } void unsigned_prune_ge2_Good(unsigned int x, unsigned int y) { if (y > 0) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 5d6acc2d3..695fff658 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -10,7 +10,6 @@ codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, INTEGER_OVERFL codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*cp`,Array access: Offset: [0, +oo] Size: 2 by call to `scan_hex_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: (0 - 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] codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (2000000000 + 2000000000):signed32] @@ -220,7 +219,6 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 2, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith5_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Array access: Offset: [4, 2044] (⇐ [0, 1020] + [4, 1024]) Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_eq_CAF` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] @@ -263,7 +261,6 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, COND codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] -codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 1 by call to `array_access_Ok` ] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 0] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index 6ca0a46bf..cb2b3635c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -142,7 +142,7 @@ void prune_arrblk_eq_CAF(int* x) { } } -void FP_call_prune_arrblk_eq_Ok() { +void call_prune_arrblk_eq_Ok() { int* x = (int*)malloc(sizeof(int) * 5); prune_arrblk_eq_CAF(x); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c index 0b3d5af36..2eafffbd2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c @@ -11,7 +11,7 @@ void array_access_Ok(int x, int y) { } } -void FP_call_array_access_Ok() { array_access_Ok(0, 0); } +void call_array_access_Ok() { array_access_Ok(0, 0); } void FP_array_access2_Ok(int x, int y) { int a[1]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 07ab1c7ca..7054f19e9 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -126,6 +126,79 @@ void conditional_inequality(int idx) { } } -void call_conditional_inequality_Good_FP() { conditional_inequality(5); } +void call_conditional_inequality_Good() { conditional_inequality(5); } void call_conditional_inequality_Bad() { conditional_inequality(6); } + +void conditional_inequality_join1(int idx) { + int a[5]; + if (idx == 5) { + } else { + // pruning exp is "idx != 5" + L: + // joined pruning exp is "Unknown" + a[idx] = 0; + } + + if (idx == 6) { + // pruning exp is "idx == 6" + goto L; + } +} + +void call_conditional_inequality_join1_Good_FP() { + conditional_inequality_join1(5); +} + +void call_conditional_inequality_join1_Bad() { + conditional_inequality_join1(6); +} + +void conditional_inequality_join2(int idx) { + int a[5]; + if (idx == 5) { + } else { + // pruning exp is "idx != 5" + L: + // joined pruning exp is "idx != [5, 6]" + a[idx] = 0; + } + + if (idx != 6) { + // pruning exp is "idx != 6" + goto L; + } +} + +void call_conditional_inequality_join2_1_Bad() { + conditional_inequality_join2(5); +} + +void call_conditional_inequality_join2_2_Bad() { + conditional_inequality_join2(6); +} + +void conditional_inequality_depth2(int i) { + int a[5]; + if (i != 1) { + a[i] = 0; + } +} + +void conditional_inequality_depth1(int i) { + if (i != 5) { + conditional_inequality_depth2(i); + } +} + +void call_conditional_inequality_depth1_1_Good_FP() { + conditional_inequality_depth1(5); +} + +void call_conditional_inequality_depth1_2_Good() { + conditional_inequality_depth1(1); +} + +void call_conditional_inequality_depth1_3_Bad() { + conditional_inequality_depth1(6); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 57f34b2be..cbec7b353 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -36,7 +36,12 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `size`,,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Good_FP, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_depth1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_3_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_depth1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_2_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] 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]] @@ -53,9 +58,6 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFF 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] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 8 Size: 5 by call to `minus_params_Ok` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params2` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params` ] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp index 6a51f4eec..97b7d8e3b 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp @@ -15,7 +15,7 @@ void minus_params_Ok(int x, int y) { void call1_minus_params_Ok() { minus_params_Ok(5, 2); } -void FP_call2_minus_params_Ok() { minus_params_Ok(10, 2); } +void call2_minus_params_Ok() { minus_params_Ok(10, 2); } void plus_params(int x, int y) { int a[5]; @@ -28,7 +28,7 @@ void call1_plus_params_Ok() { plus_params(1, 2); } void call2_plus_params_Bad() { plus_params(10, 2); } -void FP_call3_plus_params_Ok() { plus_params(0, 0); } +void call3_plus_params_Ok() { plus_params(0, 0); } void plus_params2(int x, int y) { int a[5]; @@ -41,7 +41,7 @@ void call1_plus_params2_Ok() { plus_params2(1, 2); } void call2_plus_params2_Bad() { plus_params2(10, 2); } -void FP_call3_plus_params2_Ok() { plus_params2(0, 0); } +void call3_plus_params2_Ok() { plus_params2(0, 0); } void loop(char* arr, int len) { while (len > 0) {