Add test case to check that on early exits stats are flushed

1 files changed, 22 insertions, 0 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
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 <stdlib.h>
+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])}}