diff options
Diffstat (limited to 'test/regression')
| -rw-r--r-- | test/regression/2017-03-23-early-exit-log-stats.c | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c index 4de3aa3d..3a76b9f8 100644 --- a/test/regression/2017-03-23-early-exit-log-stats.c +++ b/test/regression/2017-03-23-early-exit-log-stats.c @@ -1,9 +1,10 @@ // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // Delay writing instructions so that we ensure on exit that flush happens -// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log +// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 -stats-commit-after=1 %t.bc 2> %t.log +// RUN: klee-stats -to-csv %t.klee-out > %t.stats.csv // RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s -// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats.csv %s #include "klee/klee.h" #include <stdlib.h> int main(){ @@ -17,6 +18,6 @@ int main(){ return 0; } // First check we find a line with the expected format -// CHECK-STATS:{{^\('Instructions'}} +// CHECK-STATS:{{^Instructions}} // Now check that we eventually get a line where a non zero amount of instructions were executed -// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}} +// CHECK-STATS:{{^\([ ]*[1-9]|([1-9]+)[0-9]}} |