diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index be4d75cac..c9e3c05e0 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -127,6 +127,11 @@ let malloc size_exp = {exec; check} +let calloc size_exp stride_exp = + let byte_size_exp = Exp.BinOp (Binop.Mult, size_exp, stride_exp) in + malloc byte_size_exp + + let memcpy dest_exp src_exp size_exp = let exec _ ~ret:_ mem = mem and check {location} mem cond_set = @@ -473,6 +478,7 @@ module Call = struct ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 ; -"infer_print" <>$ capt_exp $!--> infer_print ; -"malloc" <>$ capt_exp $+...$--> malloc + ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc ; -"__new" <>$ capt_exp_of_typ (+PatternMatch.implements_collection) $+...$--> Collection.new_list diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/calloc.c b/infer/tests/codetoanalyze/c/bufferoverrun/calloc.c new file mode 100644 index 000000000..d05aeeae4 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/calloc.c @@ -0,0 +1,19 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void calloc_ok1() { + int* arr = (int*)calloc(10, sizeof(int)); + arr[0] = 0; + arr[9] = 0; +} + +void calloc_bad1() { + int* arr = (int*)calloc(10, sizeof(int)); + arr[-1] = 0; + arr[10] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 99a6ad264..6d7a4406c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -9,6 +9,8 @@ codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_O codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 4 Size: 4] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ]