inferBO calloc model

Reviewed By: mbouaziz

Differential Revision: D9874186

fbshipit-source-id: 342280666

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

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 <stdlib.h>
+
+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;
+}

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