1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
9 namespace BinaryAnalysis {
10 namespace ModelChecker {
36 using Ptr = PathPredicatePtr;
41 virtual ~PathPredicate();
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;
66 virtual
void reset() {}
76 class AlwaysTrue:
public PathPredicate {
78 using Ptr = AlwaysTruePtr;
82 static Ptr instance();
84 virtual std::pair<bool, const char*> operator()(
const SettingsPtr&,
const PathPtr&)
override;
96 class WorkPredicate:
public PathPredicate {
98 using Ptr = WorkPredicatePtr;
101 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
102 size_t kLimitReached_ = 0;
103 size_t timeLimitReached_ = 0;
107 static Ptr instance();
115 size_t kLimitReached()
const;
123 size_t timeLimitReached()
const;
126 virtual std::pair<bool, const char*> operator()(
const SettingsPtr&,
const PathPtr&)
override;
127 virtual void reset()
override;
138 class HasFinalTags:
public PathPredicate {
140 using Ptr = HasFinalTagsPtr;
144 static Ptr instance();
146 virtual std::pair<bool, const char*> operator()(
const SettingsPtr&,
const PathPtr&)
override;
Main namespace for the ROSE library.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.