diff options
| author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2016-05-12 11:17:48 +0100 |
|---|---|---|
| committer | Andrea Mattavelli <andreamattavelli@gmail.com> | 2016-05-18 10:22:51 +0100 |
| commit | eba0093c4887473be2562a7ab4e16b3d09793f4e (patch) | |
| tree | e03582fee517db083a42b3057b1f4bad187de059 /test/Feature | |
| parent | e481f415042b9bcb5af6d057648852a9d8ef7d4e (diff) | |
| download | klee-eba0093c4887473be2562a7ab4e16b3d09793f4e.tar.gz | |
Modified -debug-print-instructions to allow to write directly on log file.
The option now contains 4 different options: 1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst]; 2) src:stderr, which logs all instructions to file in format [src, inst_id]; 3) compact:stderr, which logs all instructions to file in format [inst_id]; 4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst]; 5) src:file, which logs all instructions to file in format [src, inst_id]; 6) compact:file, which logs all instructions to file in format [inst_id]; Writing to file gives a speedup of ~50x.
Diffstat (limited to 'test/Feature')
| -rw-r--r-- | test/Feature/LoggingInstructions.c | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/test/Feature/LoggingInstructions.c b/test/Feature/LoggingInstructions.c new file mode 100644 index 00000000..049aa9da --- /dev/null +++ b/test/Feature/LoggingInstructions.c @@ -0,0 +1,47 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:stderr %t2.bc 2>%t3.txt +// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-DBG %s +// RUN: not test -f %t.klee-out/instructions.txt +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-DBG %s +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=src:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=compact:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-COMPACT %s +// +#include "klee/klee.h" +#include <assert.h> +#include <stdio.h> + +char array[5] = { 1, 2, 3, -4, 5 }; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + if (array[k] == -4) + printf("Yes\n"); + + // CHECK-FILE-SRC: LoggingInstructions.c:27 + // CHECK-FILE-SRC: LoggingInstructions.c:28 + // CHECK-FILE-SRC: LoggingInstructions.c:30 + // CHECK-FILE-SRC: LoggingInstructions.c:31 + + // CHECK-FILE-DBG: call void @klee_make_symbolic + // CHECK-FILE-DBG: load + + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:21 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:22 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:24 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:25 + + return 0; +} |