about summary refs log tree commit diff homepage
path: root/test/VectorInstructions/extract_element_symbolic.c
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-11-28 20:56:14 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-12-04 15:57:01 +0000
commit9be3e76ed1f9eb0ec86531e2437091f7f1f02c88 (patch)
tree3589e114ad33c053a38c94f69dfd415efaeb30f7 /test/VectorInstructions/extract_element_symbolic.c
parent549206763cab1154fe05fc7a9a5f0e089405dcbd (diff)
downloadklee-9be3e76ed1f9eb0ec86531e2437091f7f1f02c88.tar.gz
Move all overflows from the vector instructions tests into a new file, as the overflow behaviour is different in LLVM 11.
Diffstat (limited to 'test/VectorInstructions/extract_element_symbolic.c')
-rw-r--r--test/VectorInstructions/extract_element_symbolic.c20
1 files changed, 0 insertions, 20 deletions
diff --git a/test/VectorInstructions/extract_element_symbolic.c b/test/VectorInstructions/extract_element_symbolic.c
deleted file mode 100644
index ff9a7164..00000000
--- a/test/VectorInstructions/extract_element_symbolic.c
+++ /dev/null
@@ -1,20 +0,0 @@
-// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t1.bc > %t.log 2>&1
-// RUN: FileCheck -input-file=%t.log %s
-#include "klee/klee.h"
-#include <assert.h>
-#include <stdio.h>
-#include <stdint.h>
-
-typedef uint32_t v4ui __attribute__ ((vector_size (16)));
-int main() {
-  v4ui f = { 0, 1, 2, 3 };
-  unsigned index = 0;
-  klee_make_symbolic(&index, sizeof(unsigned), "index");
-  // Performing read should be ExtractElement instruction.
-  // For now this is an expected limitation.
-  // CHECK: extract_element_symbolic.c:[[@LINE+1]]: ExtractElement, support for symbolic index not implemented
-  uint32_t readValue = f[index];
-  return readValue % 255;
-}