ROSE  0.11.50.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_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 
8 namespace Rose {
9 namespace BinaryAnalysis {
10 namespace ModelChecker {
11 
13 // Base class
15 
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 
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 
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
Path predicate that's always true.
Definition: PathPredicate.h:76
virtual void reset() override
Reset internal data.
static Ptr instance()
Allocating constructor.
virtual std::pair< bool, const char * > operator()(const SettingsPtr &, const PathPtr &)=0
The predicate.
size_t timeLimitReached() const
Property: Number of times the time limit was reached.
virtual std::pair< bool, const char * > test(const SettingsPtr &, const PathPtr &) final
The predicate.
Main namespace for the ROSE library.
PathPredicatePtr Ptr
Shared ownership pointer.
Definition: PathPredicate.h:36
virtual std::pair< bool, const char * > operator()(const SettingsPtr &, const PathPtr &) override
The predicate.
static Ptr instance()
Allocating constructor.
static Ptr instance()
Allocating constructor.
virtual std::pair< bool, const char * > operator()(const SettingsPtr &, const PathPtr &) override
The predicate.
size_t kLimitReached() const
Property: Number of times K limit was reached.
virtual std::pair< bool, const char * > operator()(const SettingsPtr &, const PathPtr &) override
The predicate.
virtual void reset()
Reset internal data.
Definition: PathPredicate.h:66