Wired up model for memmove which is identical to memcopy

Reviewed By: skcho

Differential Revision: D9810324

fbshipit-source-id: d06d411db

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -476,6 +476,7 @@ module Call = struct
       ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length
       ; -"strlen" <>--> by_value Dom.Val.Itv.nat
       ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
+      ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
       ; -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -70,6 +70,10 @@ codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bu
 codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
+codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -96,3 +96,52 @@ void memcpy_good4() {
   int dst[3];
   memcpy(dst, src, sizeof(dst));
 }
+
+void memmove_bad1() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr1, arr2, 44);
+}
+
+void memmove_bad2() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr2, arr1, 44);
+}
+
+void memmove_bad3() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr1, arr2, -1);
+}
+
+void memmove_bad4() {
+  int src[1];
+  int buff[1];
+  int* dst = &buff[0];
+  memmove(dst, src, sizeof(dst));
+}
+
+void memmove_good1() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr2, arr1, 40);
+}
+
+void memmove_good2() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr2, arr1, 0);
+}
+
+void memmove_good3() {
+  int arr1[10];
+  int arr2[20];
+  memmove(arr2, arr1, 20);
+}
+
+void memmove_good4() {
+  int src[3];
+  int dst[3];
+  memmove(dst, src, sizeof(dst));
+}