about summary refs log tree commit diff homepage
path: root/test/Concrete
diff options
context:
space:
mode:
authorMartin Nowack <martin_nowack@tu-dresden.de>2017-10-30 22:11:00 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-02-18 12:49:41 +0000
commita8fd0b699af4be33ce990c25d3e164d7d391ca25 (patch)
treec28c906de8040c9cdabb1012a22026560efaf100 /test/Concrete
parente98449fff404a88305869849eb066def1bc0323b (diff)
downloadklee-a8fd0b699af4be33ce990c25d3e164d7d391ca25.tar.gz
Add test case for constant vector init
Diffstat (limited to 'test/Concrete')
-rw-r--r--test/Concrete/ConstantInit.ll26
1 files changed, 26 insertions, 0 deletions
diff --git a/test/Concrete/ConstantInit.ll b/test/Concrete/ConstantInit.ll
new file mode 100644
index 00000000..161069df
--- /dev/null
+++ b/test/Concrete/ConstantInit.ll
@@ -0,0 +1,26 @@
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
+%struct.dirent = type { i64, i64, i16, i8, [256 x i8] }
+declare void @print_i64(i64)
+
+define i32 @main() {
+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
+	store <2 x i64> <i64 0, i64 4096>, <2 x i64>* %tmp2, align 8
+	br label %exit
+exit:
+	; Print first initialized element
+	%idx = getelementptr %struct.dirent* %a, i32 0, i32 0
+	%val = load i64* %idx	
+	call void @print_i64(i64 %val)
+
+	; Print second initialized element	
+	%idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1
+	%val2 = load i64* %idx2	
+	call void @print_i64(i64 %val2)
+	
+	ret i32 0
+}