Description
Path predicate.
A path predicate is a user-defined function that returns true or false for a specified path. It is used for such things as deciding whether a path should be added to a queue.
For instance, when the model checker is about to add a path to the work queue, it will first consult a predicate to decide if it should do that. The predicate might reject the path based on attributes such as:
- Prune paths that have too many steps.
- Prune paths that go through the same CFG node too many times, thus limiting loop iterations and recursion.
- Prune paths where the SMT solver takes too long, since exploring further from such a path usually makes the solver take even longer.
- Prune paths whose states are becoming too large. An alternative is to reduce the size of large states as part of executing a path vertex.
Definition at line 33 of file PathPredicate.h.
#include <Rose/BinaryAnalysis/ModelChecker/PathPredicate.h>
Public Types | |
| using | Ptr = PathPredicatePtr |
| Shared ownership pointer. More... | |
Public Member Functions | |
| virtual void | reset () |
| Reset internal data. More... | |
| virtual std::pair< bool, const char * > | operator() (const SettingsPtr &, const PathPtr &)=0 |
| The predicate. More... | |
| virtual std::pair< bool, const char * > | test (const SettingsPtr &, const PathPtr &) final |
| The predicate. More... | |
Member Typedef Documentation
| using Rose::BinaryAnalysis::ModelChecker::PathPredicate::Ptr = PathPredicatePtr |
Shared ownership pointer.
Definition at line 36 of file PathPredicate.h.
Member Function Documentation
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::HasFinalTags, Rose::BinaryAnalysis::ModelChecker::WorkPredicate, and Rose::BinaryAnalysis::ModelChecker::AlwaysTrue.
|
finalvirtual |
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.
|
inlinevirtual |
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 in Rose::BinaryAnalysis::ModelChecker::WorkPredicate.
Definition at line 66 of file PathPredicate.h.
The documentation for this class was generated from the following file:
