about summary refs log tree commit diff homepage
path: root/lib/Core/CoreStats.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/CoreStats.h')
-rw-r--r--lib/Core/CoreStats.h8
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h
index c0dcac7d..15850354 100644
--- a/lib/Core/CoreStats.h
+++ b/lib/Core/CoreStats.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_CORESTATS_H
 #define KLEE_CORESTATS_H
 
+#include "klee/Core/BranchTypes.h"
 #include "klee/Statistics/Statistic.h"
 
 namespace klee {
@@ -49,6 +50,13 @@ namespace stats {
   /// distance to a function return.
   extern Statistic minDistToReturn;
 
+  /// Count branch types in execution tree. Inhibited branches are ignored.
+  #undef BTYPE
+  #define BTYPE(Name,I) extern Statistic branches ## Name;
+  BRANCH_TYPES
+
+  /// Increase a branch statistic for the given reason by value.
+  void incBranchStat(BranchType reason, std::uint32_t value);
 }
 }