diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 9786b13f1..dafa5bbf0 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -44,7 +44,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = BoUtils.counter_gen 1 in - let rec decl_sym_val pname tenv node location ~depth ~is_last_field loc typ mem = + let rec decl_sym_val pname tenv node location ~depth ~may_last_field loc typ mem = if depth > max_depth then mem else let depth = depth + 1 in @@ -64,35 +64,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> BoUtils.Exec.decl_sym_arr - ~decl_sym_val:(decl_sym_val ~is_last_field:false) + ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length} -> let size = match length with - | Some length when is_last_field && (IntLit.iszero length || IntLit.isone length) -> + | Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) -> Some (Itv.make_sym pname new_sym_num) | _ -> Option.map ~f:Itv.of_int_lit length in let offset = Itv.zero in BoUtils.Exec.decl_sym_arr - ~decl_sym_val:(decl_sym_val ~is_last_field:false) + ~decl_sym_val:(decl_sym_val ~may_last_field:false) pname tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tstruct typename -> ( match Models.TypName.dispatch typename with | Some {Models.declare_symbolic} -> let model_env = Models.mk_model_env pname node location tenv in - declare_symbolic ~decl_sym_val:(decl_sym_val ~is_last_field) model_env ~depth loc + declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem | None -> - let decl_fld ~is_last_field mem (fn, typ, _) = + let decl_fld ~may_last_field mem (fn, typ, _) = let loc_fld = Loc.append_field loc ~fn in - decl_sym_val pname tenv node location ~depth loc_fld typ ~is_last_field mem + decl_sym_val pname tenv node location ~depth loc_fld typ ~may_last_field mem in let decl_flds str = - IList.fold_last ~f:(decl_fld ~is_last_field:false) - ~f_last:(decl_fld ~is_last_field) ~init:mem str.Typ.Struct.fields + IList.fold_last ~f:(decl_fld ~may_last_field:false) + ~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields in let opt_struct = Tenv.lookup tenv typename in Option.value_map opt_struct ~default:mem ~f:decl_flds ) @@ -103,7 +103,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (CFG.loc node) ; mem in - decl_sym_val pname tenv node location ~depth:0 ~is_last_field:false loc typ mem + decl_sym_val pname tenv node location ~depth:0 ~may_last_field:true loc typ mem let declare_symbolic_parameters diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index b77ddf589..59f571b15 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp @@ -150,14 +150,26 @@ class Tree { Tree* children[1]; }; -void flexible_array5_Good_FP() { +void flexible_array5_Good() { Tree* t = Tree::NewNode(3); t->set_child(Tree::NewLeaf(), 0); t->set_child(Tree::NewLeaf(), 1); t->set_child(Tree::NewLeaf(), 2); } -void flexible_array5_Bad() { +void flexible_array5_Bad_FN() { Tree* t = Tree::NewNode(3); t->set_child(Tree::NewLeaf(), 5); } + +void flexible_array_param_access(my_class4* x) { x->b[3] = 0; } + +void flexible_array_param_Good() { + my_class4* x = (my_class4*)malloc(sizeof(my_class4) + 4 * sizeof(int)); + flexible_array_param_access(x); +} + +void flexible_array_param_Bad() { + my_class4* x = (my_class4*)malloc(sizeof(my_class4) + 2 * sizeof(int)); + flexible_array_param_access(x); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e344b3605..d68ec9d5d 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -3,8 +3,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_O codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [5, 5] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Good_FP, 4, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [2, 2] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [3, 3] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:165:50 by call `flexible_array_param_access()` ] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]