diff options
| author | Martin Nowack <martin_nowack@tu-dresden.de> | 2017-11-02 09:29:49 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-02-18 12:49:41 +0000 |
| commit | 4989af217357a499f21f5bfc6ad897a435d72db1 (patch) | |
| tree | 6477371f07ab17f9bc8f919b216594c5f9daa9de /test | |
| parent | a8fd0b699af4be33ce990c25d3e164d7d391ca25 (diff) | |
| download | klee-4989af217357a499f21f5bfc6ad897a435d72db1.tar.gz | |
Add testcase for constant array handling
Diffstat (limited to 'test')
| -rw-r--r-- | test/Feature/ConstantArray.ll | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/test/Feature/ConstantArray.ll b/test/Feature/ConstantArray.ll new file mode 100644 index 00000000..161b2a16 --- /dev/null +++ b/test/Feature/ConstantArray.ll @@ -0,0 +1,51 @@ +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc 2>&1 | FileCheck %s +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" + +@.str = private unnamed_addr constant [2 x i8] c"0\00", align 1 +@.str2 = private unnamed_addr constant [2 x i8] c"1\00", align 1 + +%struct.dirent = type { i32, i32, i16, i8 } +declare void @klee_print_expr(i8*, ...) + +define i32 @main() { +entry: + %a = alloca %struct.dirent + %tmp1 = getelementptr %struct.dirent* %a, i32 0 + %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>* + ; Initialize with constant vector + store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2 + br label %exit +exit: + ; Print first initialized element + %idx = getelementptr %struct.dirent* %a, i32 0, i32 0 + %val = load i32* %idx + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val) + ; CHECK: 0:42 + + ; Print second initialized element + %idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1 + %val2 = load i32* %idx2 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val2) + ; CHECK: 1:4096 + + ; Initialize with constant array + %array = alloca [2 x i32]; + store [2 x i32][i32 7, i32 9], [2 x i32]* %array + + ; Print first initialized element + %idx3 = getelementptr [2 x i32]* %array, i32 0, i32 0 + %val3 = load i32* %idx3 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val3) + ; CHECK: 0:7 + + ; Print second initialized element + %idx4 = getelementptr [2 x i32]* %array, i32 0, i32 1 + %val4 = load i32* %idx4 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val4) + ; CHECK: 1:9 + + ret i32 0 +} \ No newline at end of file |