Description
Default work queue predicate.
Any paths inserted into the work queue, other than initial paths inserted by the user when configuring the model checker, are checked by a predicate, and if the predicate returns false then the path is not inserted. This predicate is the default.
Definition at line 96 of file PathPredicate.h.
#include <Rose/BinaryAnalysis/ModelChecker/PathPredicate.h>
Public Types | |
| using | Ptr = WorkPredicatePtr |
 Public Types inherited from Rose::BinaryAnalysis::ModelChecker::PathPredicate | |
| using | Ptr = PathPredicatePtr |
| Shared ownership pointer. More... | |
Public Member Functions | |
| size_t | kLimitReached () const |
| Property: Number of times K limit was reached. More... | |
| size_t | timeLimitReached () const |
| Property: Number of times the time limit was reached. More... | |
| virtual std::pair< bool, const char * > | operator() (const SettingsPtr &, const PathPtr &) override |
| The predicate. More... | |
| virtual void | reset () override |
| Reset internal data. More... | |
| Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::PathPredicate | |
| virtual std::pair< bool, const char * > | test (const SettingsPtr &, const PathPtr &) final |
| The predicate. More... | |
Static Public Member Functions | |
| static Ptr | instance () |
| Allocating constructor. More... | |
Member Function Documentation
|
static |
Allocating constructor.
| size_t Rose::BinaryAnalysis::ModelChecker::WorkPredicate::kLimitReached | ( | ) | const |
Property: Number of times K limit was reached.
This property stores the number of times that this predicate returned false due to the path length limit being reached.
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::WorkPredicate::timeLimitReached | ( | ) | const |
Property: Number of times the time limit was reached.
This property stores the number of times that this predicate returned false due to the path time limit being reached.
Thread safety: This method is thread safe.
|
overridevirtual |
The predicate.
Tests the path for some condition and returns true or false and an optional reason which is a short C-style string containing only horizontal, printable characters without leading or trailing white space. The string must not be null, but may be empty.
For convenience, the predicate can be applied using either the function operator or the test method, although it's the operator that gets overloaded in the subclasses.
Thread safety: All implementations must be thread safe.
Implements Rose::BinaryAnalysis::ModelChecker::PathPredicate.
|
overridevirtual |
Reset internal data.
Some predicates keep track of various statistics, such as how many paths were rejected because they had too many steps. This function resets that kind of information. The base implementation does nothing.
Thread safety: All implementations must be thread safe.
Reimplemented from Rose::BinaryAnalysis::ModelChecker::PathPredicate.
The documentation for this class was generated from the following file:
