diff options
| -rw-r--r-- | test/Feature/KleeStats.c | 19 | ||||
| -rwxr-xr-x | tools/klee-stats/klee-stats | 2 |
2 files changed, 20 insertions, 1 deletions
diff --git a/test/Feature/KleeStats.c b/test/Feature/KleeStats.c new file mode 100644 index 00000000..48305358 --- /dev/null +++ b/test/Feature/KleeStats.c @@ -0,0 +1,19 @@ +// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: klee-stats --print-more %t.klee-out > %t.stats +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s +#include "klee/klee.h" +#include <stdlib.h> +int main(){ + int a; + klee_make_symbolic (&a, sizeof(int), "a"); + if (a) { + abort(); + } + return 0; +} +// First check we find a line with the expected format +// CHECK-STATS: | Path | Instrs| Time(s)| ICov(%)| BCov(%)| ICount| TSolver(%)| +//Check there is a line with .klee-out dir, non zero instruction, less than 1 second execution time and 100 ICov. +// CHECK-STATS: {{.*\.klee-out\|[ ]*[1-9]+\|[ ]*0\.([0-9]+)\|[ ]*100\.00}} diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 38d8f750..c0171343 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -133,7 +133,7 @@ def getRow(record, stats, pr): if BTot == 0: BFull = BTot = 1 - Ts, Tcex, Tf, Tr = [e / 1000000 for e in [Ts, Tcex, Tf, Tr]] #convert from microseconds + Ts, Tcex, Tf, Tr, T, Treal = [e / 1000000 for e in [Ts, Tcex, Tf, Tr, T, Treal]] #convert from microseconds Mem = Mem / 1024 / 1024 AvgQC = int(QCon / max(1, QTot)) |