[inferbo] Add tests: values representing multiple values

Reviewed By: mbouaziz

Differential Revision: D13606721

fbshipit-source-id: 594d24d4a

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

@@ -211,6 +211,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BU
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne_CAT` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
+codetoanalyze/c/bufferoverrun/prune_alias.c, not_prune_multiple1_Bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 5]
+codetoanalyze/c/bufferoverrun/prune_alias.c, not_prune_multiple3_Bad, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 5]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -288,3 +288,57 @@ void forget_locs_latest_prune(unsigned int n) {
 }
 
 void call_forget_locs_latest_prune_Bad() { forget_locs_latest_prune(10); }
+
+void not_prune_multiple1_Bad() {
+  int a[5];
+  int m[2] = {0, 10};
+  if (m[0] < 5) {
+    a[m[1]] = 0;
+  }
+}
+
+void not_prune_multiple2(int* m) {
+  int a[5];
+  if (m[0] < 5) {
+    a[m[1]] = 0;
+  }
+}
+
+void call_not_prune_multiple2_Good() {
+  int m[2] = {0, 4};
+  not_prune_multiple2(m);
+}
+
+void call_not_prune_multiple2_Bad_FN() {
+  int m[2] = {0, 10};
+  not_prune_multiple2(m);
+}
+
+void not_prune_multiple3_Bad() {
+  int a[5];
+  int* m = (int*)malloc(sizeof(int) * 2);
+  m[0] = 0;
+  m[1] = 10;
+  if (*m < 5) {
+    m++;
+    a[*m] = 0;
+  }
+}
+
+void not_prune_multiple4(int* m) {
+  int a[5];
+  if (*m < 5) {
+    m++;
+    a[*m] = 0;
+  }
+}
+
+void call_not_prune_multiple4_Good() {
+  int m[2] = {0, 4};
+  not_prune_multiple4(m);
+}
+
+void call_not_prune_multiple4_Bad_FN() {
+  int m[2] = {0, 10};
+  not_prune_multiple4(m);
+}