diff options
author | Martin Nowack <martin_nowack@tu-dresden.de> | 2017-11-02 10:17:19 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-02-18 12:49:41 +0000 |
commit | ffce29c6b6ddf0c002f9e95498571f9e4a6e27bc (patch) | |
tree | e0c52a438ab19ab1d1075ee69fc561937b47ecac /test/Concrete | |
parent | 7a0e82382e1211ba316af72576fe9a5bbc760fa5 (diff) | |
download | klee-ffce29c6b6ddf0c002f9e95498571f9e4a6e27bc.tar.gz |
Test complex constant data vectors as well
Diffstat (limited to 'test/Concrete')
-rw-r--r-- | test/Concrete/ConstantInit.ll | 43 |
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 } |