From a8bf1a78cd20d1c2608faeecc54369d95ceadde7 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Thu, 5 Apr 2018 20:27:10 +0100 Subject: 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. --- test/regression/2018-05-05-number-instructions-dumped-states.c | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test/regression/2018-05-05-number-instructions-dumped-states.c (limited to 'test') 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[]) {} -- cgit 1.4.1