From a40818cab8e1b2315ac40d2c2cb125fc422e8ed7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 23 Mar 2017 12:51:45 +0000 Subject: Add test case to check that on early exits stats are flushed --- test/regression/2017-03-23-early-exit-log-stats.c | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test/regression/2017-03-23-early-exit-log-stats.c (limited to 'test') diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c new file mode 100644 index 00000000..96d3c30f --- /dev/null +++ b/test/regression/2017-03-23-early-exit-log-stats.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -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: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s +#include "klee/klee.h" +#include +int main(){ + int a; + klee_make_symbolic (&a, sizeof(int), "a"); + if (a) { + // CHECK-KLEE: EXITING ON ERROR + // CHECK-KLEE-NEXT: Error: abort failure + abort(); + } + return 0; +} +// First check we find a line with the expected format +// 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])}} -- cgit 1.4.1