diff options
Diffstat (limited to 'lib/Core/CoreStats.cpp')
-rw-r--r-- | lib/Core/CoreStats.cpp | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 06b8b930..54a9a697 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -9,6 +9,9 @@ #include "CoreStats.h" +#include "klee/Support/ErrorHandling.h" + + using namespace klee; Statistic stats::allocations("Allocations", "Alloc"); @@ -28,3 +31,21 @@ Statistic stats::solverTime("SolverTime", "Stime"); Statistic stats::states("States", "States"); Statistic stats::trueBranches("TrueBranches", "Bt"); Statistic stats::uncoveredInstructions("UncoveredInstructions", "Iuncov"); + + +// branch stats and setter + +#undef BTYPE +#define BTYPE(Name,I) Statistic stats::branches ## Name("Branches"#Name, "Br"#Name); +BRANCH_TYPES + +void stats::incBranchStat(BranchType reason, std::uint32_t value) { +#undef BTYPE +#define BTYPE(N,I) case BranchType::N : stats::branches ## N += value; break; + switch (reason) { + BRANCH_TYPES + default: + klee_error("Illegal branch type in incBranchStat(): %hhu", + static_cast<std::uint8_t>(reason)); + } +} |