diff options
-rw-r--r-- | lib/Core/Executor.cpp | 3 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 4 | ||||
-rw-r--r-- | lib/Core/StatsTracker.h | 1 |
3 files changed, 8 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 1e1a142b..f7c71e8d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -354,6 +354,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, initializeSearchOptions(); + if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats()) + klee_error("To use --only-output-states-covering-new, you need to enable --output-istats."); + if (DebugPrintInstructions.isSet(FILE_ALL) || DebugPrintInstructions.isSet(FILE_COMPACT) || DebugPrintInstructions.isSet(FILE_SRC)) { diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 83e1844f..d9ec35aa 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -110,6 +110,10 @@ bool StatsTracker::useStatistics() { return OutputStats || OutputIStats; } +bool StatsTracker::useIStats() { + return OutputIStats; +} + namespace klee { class WriteIStatsTimer : public Executor::Timer { StatsTracker *statsTracker; diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index 629a723d..23abac06 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -48,6 +48,7 @@ namespace klee { public: static bool useStatistics(); + static bool useIStats(); private: void updateStateStatistics(uint64_t addend); |