New regression test checking that the Array factory correctly distinguishes between arrays created at the same location but with different sizes

1 files changed, 41 insertions, 0 deletions

diff --git a/test/Feature/MultiMkSym.c b/test/Feature/MultiMkSym.c
new file mode 100644
index 00000000..85b6ed70
--- /dev/null
+++ b/test/Feature/MultiMkSym.c
@@ -0,0 +1,41 @@
+// RUN: %llvmgcc -I../../../include -emit-llvm -g -c %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --write-pcs %t.bc > %t.log
+// RUN: cat %t.klee-out/test000001.pc %t.klee-out/test000002.pc %t.klee-out/test000003.pc %t.klee-out/test000004.pc > %t1
+// RUN: grep "a\[1\]" %t1 | wc -l | grep 2
+// RUN: grep "a\[100\]" %t1 | wc -l | grep 2
+
+/* Tests that the Array factory correctly distinguishes between arrays created at the same location but with different sizes */
+
+#include <stdio.h>
+#include <stdlib.h>
+
+char* mk_sym(int size) {
+  char *a = malloc(size);
+  klee_make_symbolic(a, size, "a");
+  return a;
+}
+
+int main() {
+  int t;
+  char *a, *b;
+
+  klee_make_symbolic(&t, sizeof(t), "t");
+
+  if (t) {
+    printf("Allocate obj of size 1\n");
+    a = mk_sym(1);
+    if (a[0] > 'a')
+      printf("Yes\n");
+    else printf("No\n");
+  }
+  else {
+    printf("Allocate obj of size 2\n");
+    b = mk_sym(100);
+    if (b[99] > 'a')
+      printf("Yes\n");
+    else printf("No\n");
+  }
+
+  return 0;
+}