From 98cd2e59daa16e6a7ac2b81ae21b9eb6c5519aeb Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Wed, 9 Jan 2019 20:42:25 -0800
Subject: [PATCH] [inferbo] Add tests: values representing multiple values

Reviewed By: mbouaziz

Differential Revision: D13606721

fbshipit-source-id: 594d24d4a
---
 .../codetoanalyze/c/bufferoverrun/issues.exp  |  2 +
 .../c/bufferoverrun/prune_alias.c             | 54 +++++++++++++++++++
 2 files changed, 56 insertions(+)

diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index f57f286f2..4ce2b01ac 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/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]
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
index 803deb189..6ca0a46bf 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
+++ b/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);
+}