1 files changed, 44 insertions, 0 deletions
diff --git a/test/VectorInstructions/oob-llvm-lt11.c b/test/VectorInstructions/oob-llvm-lt11.c
new file mode 100644
index 00000000..9d80ef7d
--- /dev/null
+++ b/test/VectorInstructions/oob-llvm-lt11.c
@@ -0,0 +1,44 @@
+// REQUIRES: lt-llvm-11.0
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// NOTE: Have to pass `--optimize=false` to avoid vector operations being
+// constant folded away.
+// RUN: %klee --output-dir=%t.klee-out --optimize=false  %t1.bc > %t.stdout.log 2> %t.stderr.log
+// RUN: FileCheck -input-file=%t.stderr.log %s
+
+#include "klee/klee.h"
+
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef uint32_t v4ui __attribute__((vector_size(16)));
+int main() {
+  v4ui f = {1, 2, 3, 4};
+  int k = klee_range(0, 10, "k");
+
+  if (k == 0) {
+    // CHECK-DAG: [[@LINE+1]]: Out of bounds write when inserting element
+    f[4] = 255; // Out of bounds write
+  }
+
+  if (k == 1) {
+    // CHECK-DAG: [[@LINE+1]]: Out of bounds read when extracting element
+    printf("f[4] = %u\n", f[5]); // Out of bounds
+  }
+
+  if (k > 6) {
+    // Performing read should be ExtractElement instruction.
+    // For now this is an expected limitation.
+    // CHECK-DAG: [[@LINE+1]]: ExtractElement, support for symbolic index not implemented
+    uint32_t readValue = f[k];
+  }
+  else {
+    // Performing write should be InsertElement instructions.
+    // For now this is an expected limitation.
+    // CHECK-DAG: [[@LINE+1]]: InsertElement, support for symbolic index not implemented
+    f[k] = 255;
+  }
+
+  return 0;
+}