diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-10-28 16:11:18 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-05 10:39:50 +0000 |
commit | 46463adc26e29075c4cf87cc8f51d5a191929938 (patch) | |
tree | b5b5636d879344e8cbd64ed66095425a240d5348 /test | |
parent | 44325801ed4840cb1c334b9810f16ea8d691e986 (diff) | |
download | klee-46463adc26e29075c4cf87cc8f51d5a191929938.tar.gz |
fix Executor::initializeGlobals for aliases pointing to another alias
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/Alias.c | 5 | ||||
-rw-r--r-- | test/regression/2018-10-28-alias-to-alias.leq36.ll | 21 | ||||
-rw-r--r-- | test/regression/2018-10-28-alias-to-alias.leq37.ll | 23 | ||||
-rw-r--r-- | test/regression/2018-10-28-alias-to-alias.ll | 23 |
4 files changed, 72 insertions, 0 deletions
diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c index 09abb3e0..f83652d8 100644 --- a/test/Feature/Alias.c +++ b/test/Feature/Alias.c @@ -10,6 +10,10 @@ int b = 52; extern int a __attribute__((alias("b"))); +// alias for alias +// NOTE: this does not have to be before foo is known +extern int foo2() __attribute__((alias("foo"))); + // alias for function int __foo() { return 52; } extern int foo() __attribute__((alias("__foo"))); @@ -19,6 +23,7 @@ int *c = &a; int main() { assert(a == 52); assert(foo() == 52); + assert(foo2() == 52); assert(*c == 52); return 0; 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 +} |