diff options
author | Frank Busse <bb0xfb@gmail.com> | 2018-04-05 20:27:10 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-04-09 15:57:00 +0100 |
commit | a8bf1a78cd20d1c2608faeecc54369d95ceadde7 (patch) | |
tree | 0651f5c6674cd2036204404cf11a1eb4faa1bfe1 /test | |
parent | 110e97a4e07339cb9593a48b6a23df0f484a4750 (diff) | |
download | klee-a8bf1a78cd20d1c2608faeecc54369d95ceadde7.tar.gz |
doDumpStates: incorrectly increments stats
doDumpStates calls stepInstruction and therefore indirectly increases time and instruction statistics for all dangling (dumped) states. This patch removes the call, but now the timing stats for the last executed state are lost, as StatsTracker::stepInstruction isn't called anymore.
Diffstat (limited to 'test')
-rw-r--r-- | test/regression/2018-05-05-number-instructions-dumped-states.c | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/regression/2018-05-05-number-instructions-dumped-states.c b/test/regression/2018-05-05-number-instructions-dumped-states.c new file mode 100644 index 00000000..5f2af61e --- /dev/null +++ b/test/regression/2018-05-05-number-instructions-dumped-states.c @@ -0,0 +1,9 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -stop-after-n-instructions=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s + +// CHECK: KLEE: done: total instructions = 1 + +#include "klee/klee.h" + +int main(int argc, char * argv[]) {} |