about summary refs log tree commit diff homepage
path: root/test/regression
diff options
context:
space:
mode:
authorJulian Büning <julian.buening@rwth-aachen.de>2018-10-28 16:11:18 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-03-05 10:39:50 +0000
commit46463adc26e29075c4cf87cc8f51d5a191929938 (patch)
treeb5b5636d879344e8cbd64ed66095425a240d5348 /test/regression
parent44325801ed4840cb1c334b9810f16ea8d691e986 (diff)
downloadklee-46463adc26e29075c4cf87cc8f51d5a191929938.tar.gz
fix Executor::initializeGlobals for aliases pointing to another alias
Diffstat (limited to 'test/regression')
-rw-r--r--test/regression/2018-10-28-alias-to-alias.leq36.ll21
-rw-r--r--test/regression/2018-10-28-alias-to-alias.leq37.ll23
-rw-r--r--test/regression/2018-10-28-alias-to-alias.ll23
3 files changed, 67 insertions, 0 deletions
diff --git a/test/regression/2018-10-28-alias-to-alias.leq36.ll b/test/regression/2018-10-28-alias-to-alias.leq36.ll
new file mode 100644
index 00000000..2d4bd803
--- /dev/null
+++ b/test/regression/2018-10-28-alias-to-alias.leq36.ll
@@ -0,0 +1,21 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: rm -rf %t.klee-out
+; RUN: llvm-as -f %s -o - | %klee --output-dir=%t.klee-out
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; @foo is not known yet
+@foo2 = alias i32 (...)* @foo
+@foo = alias bitcast (i32 ()* @__foo to i32 (...)*)
+
+define i32 @__foo() {
+entry:
+  ret i32 42
+}
+
+define i32 @main() {
+entry:
+  call i32 (...)* @foo()
+  call i32 (...)* @foo2()
+  ret i32 0
+}
diff --git a/test/regression/2018-10-28-alias-to-alias.leq37.ll b/test/regression/2018-10-28-alias-to-alias.leq37.ll
new file mode 100644
index 00000000..9ed5aa47
--- /dev/null
+++ b/test/regression/2018-10-28-alias-to-alias.leq37.ll
@@ -0,0 +1,23 @@
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
+; REQUIRES: lt-llvm-3.8
+; RUN: rm -rf %t.klee-out
+; RUN: llvm-as -f %s -o - | %klee --output-dir=%t.klee-out
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; @foo is not known yet
+@foo2 = alias i32 (...)* @foo
+@foo = alias bitcast (i32 ()* @__foo to i32 (...)*)
+
+define i32 @__foo() {
+entry:
+  ret i32 42
+}
+
+define i32 @main() {
+entry:
+  call i32 (...) @foo()
+  call i32 (...) @foo2()
+  ret i32 0
+}
diff --git a/test/regression/2018-10-28-alias-to-alias.ll b/test/regression/2018-10-28-alias-to-alias.ll
new file mode 100644
index 00000000..0e9415d8
--- /dev/null
+++ b/test/regression/2018-10-28-alias-to-alias.ll
@@ -0,0 +1,23 @@
+; LLVM 3.8 requires a type as the first argument to 'alias'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.8
+; RUN: rm -rf %t.klee-out
+; RUN: llvm-as -f %s -o - | %klee --output-dir=%t.klee-out
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; @foo is not known yet
+@foo2 = alias i32 (...), i32 (...)* @foo
+@foo = alias i32 (...), bitcast (i32 ()* @__foo to i32 (...)*)
+
+define i32 @__foo() {
+entry:
+  ret i32 42
+}
+
+define i32 @main() {
+entry:
+  call i32 (...) @foo()
+  call i32 (...) @foo2()
+  ret i32 0
+}