aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorMartin Nowack <martin_nowack@tu-dresden.de>2017-11-02 10:17:19 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-02-18 12:49:41 +0000
commitffce29c6b6ddf0c002f9e95498571f9e4a6e27bc (patch)
treee0c52a438ab19ab1d1075ee69fc561937b47ecac
parent7a0e82382e1211ba316af72576fe9a5bbc760fa5 (diff)
downloadklee-ffce29c6b6ddf0c002f9e95498571f9e4a6e27bc.tar.gz
Test complex constant data vectors as well
-rw-r--r--test/Concrete/ConstantInit.ll43
1 files changed, 38 insertions, 5 deletions
diff --git a/test/Concrete/ConstantInit.ll b/test/Concrete/ConstantInit.ll
index 161069df..2127d27b 100644
--- a/test/Concrete/ConstantInit.ll
+++ b/test/Concrete/ConstantInit.ll
@@ -1,15 +1,16 @@
; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
-%struct.dirent = type { i64, i64, i16, i8, [256 x i8] }
+%struct.dirent = type { i64, i64, i16, i8 }
declare void @print_i64(i64)
-define i32 @main() {
-entry:
+define void @test_constant_vector_simple() {
+ entry:
%a = alloca %struct.dirent
%tmp1 = getelementptr %struct.dirent* %a, i32 0
%tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i64>*
- ; Initialize with constant vector
+ ; Initialize with constant vector parsed as ConstantDataSequential
store <2 x i64> <i64 0, i64 4096>, <2 x i64>* %tmp2, align 8
+
br label %exit
exit:
; Print first initialized element
@@ -21,6 +22,38 @@ exit:
%idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1
%val2 = load i64* %idx2
call void @print_i64(i64 %val2)
-
+ ret void
+}
+
+define void @test_constant_vector_complex() {
+entry:
+ ; Create a vector using an uncommon type: i1024: Force usage of constant vector
+ %a = alloca <2 x i1024>
+ store <2 x i1024> <i1024 5, i1024 1024>, <2 x i1024>* %a, align 8
+
+ br label %exit
+exit:
+ ; Print first initialized element
+ %idx = getelementptr <2 x i1024>* %a, i32 0, i32 0
+ %narrow = bitcast i1024* %idx to i64*
+ %val = load i64* %narrow
+ call void @print_i64(i64 %val)
+
+ ; Print second initialized element
+ %idx2 = getelementptr <2 x i1024>* %a, i32 0, i32 1
+ %narrow2 = bitcast i1024* %idx2 to i64*
+ %val2 = load i64* %narrow2
+ call void @print_i64(i64 %val2)
+
+ ret void
+}
+
+define i32 @main() {
+entry:
+ call void @test_constant_vector_simple()
+ call void @test_constant_vector_complex()
+
+ br label %exit
+exit:
ret i32 0
}