diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index e73076798..bd2b1cbec 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -393,27 +393,33 @@ module Report = struct cond_set - let rec check_expr + let check_expr : Typ.Procname.t -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = fun pname exp location mem cond_set -> + let rec check_sub_expr exp cond_set = + match exp with + | Exp.Lindex (array_exp, index_exp) -> + cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp + |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location + | Exp.BinOp (_, e1, e2) -> + cond_set |> check_sub_expr e1 |> check_sub_expr e2 + | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) -> + check_sub_expr e cond_set + | Exp.Closure {captured_vars} -> + List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> + check_sub_expr e cond_set ) + | Exp.Var _ | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ -> + cond_set + in + let cond_set = check_sub_expr exp cond_set in match exp with | Exp.Var _ -> let arr = Sem.eval exp mem in BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set - | Exp.Lindex (array_exp, index_exp) -> - cond_set |> check_expr pname array_exp location mem - |> check_expr pname index_exp location mem - |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location | Exp.BinOp (bop, e1, e2) -> - cond_set |> check_expr pname e1 location mem |> check_expr pname e2 location mem - |> check_binop pname ~bop ~e1 ~e2 location mem - | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) -> - check_expr pname e location mem cond_set - | Exp.Closure {captured_vars} -> - List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> - check_expr pname e location mem cond_set ) - | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ -> + check_binop pname ~bop ~e1 ~e2 location mem cond_set + | _ -> cond_set diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 25a3e48de..9fbfd3d39 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -50,7 +50,6 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, ERROR, []