ROSE  0.11.109.0
PathPredicate.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 
8 namespace Rose {
9 namespace BinaryAnalysis {
10 namespace ModelChecker {
11 
13 // Base class
15 
33 class PathPredicate {
34 public:
36  using Ptr = PathPredicatePtr;
37 
38 protected:
39  PathPredicate();
40 public:
41  virtual ~PathPredicate();
42 
43 public:
56  virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) = 0;
57  virtual std::pair<bool, const char*> test(const SettingsPtr&, const PathPtr&) final; // virtual only so we can say final
66  virtual void reset() {}
67 };
68 
70 // Predicate that's always true.
72 
76 class AlwaysTrue: public PathPredicate {
77 public:
78  using Ptr = AlwaysTruePtr;
79 
80 public:
82  static Ptr instance();
83 
84  virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
85 };
86 
88 // Default predicate guarding the work queue.
90 
96 class WorkPredicate: public PathPredicate {
97 public:
98  using Ptr = WorkPredicatePtr;
99 
100 private:
101  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
102  size_t kLimitReached_ = 0; // number of times the K limit was hit
103  size_t timeLimitReached_ = 0; // number of times the time limit was hit
104 
105 public:
107  static Ptr instance();
108 
115  size_t kLimitReached() const;
116 
123  size_t timeLimitReached() const;
124 
125 public: // overrides
126  virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
127  virtual void reset() override;
128 };
129 
131 // Default predicate guarding the "interesting" queue.
133 
138 class HasFinalTags: public PathPredicate {
139 public:
140  using Ptr = HasFinalTagsPtr;
141 
142 public:
144  static Ptr instance();
145 
146  virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
147 };
148 
149 } // namespace
150 } // namespace
151 } // namespace
152 
153 #endif
154 #endif
Main namespace for the ROSE library.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.