about summary refs log tree commit diff homepage
path: root/lib/Core/CoreStats.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/CoreStats.cpp')
-rw-r--r--lib/Core/CoreStats.cpp21
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));
+  }
+}