1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Path_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Path_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
9 #include <Rose/BinaryAnalysis/SmtSolver.h>
10 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
11 #include <Combinatorics.h>
14 namespace BinaryAnalysis {
15 namespace ModelChecker {
30 explicit Path(
const PathNodePtr &end);
40 static Ptr
instance(
const ExecutionUnitPtr&);
90 uint64_t
hash()
const;
106 std::vector<SymbolicExpr::Ptr>
assertions()
const;
123 std::vector<PathNodePtr>
nodes()
const;
136 void print(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
size_t maxSteps)
const;
144 void toYaml(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
size_t maxSteps)
const;
uint64_t hash() const
Path hash.
void toYaml(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
Multi-line output of path.
size_t nNodes() const
Length of path in nodes.
void print(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
Multi-line output of path.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Main namespace for the ROSE library.
static Ptr instance(const ExecutionUnitPtr &)
Construct a path that is one vertex in length.
PathNodePtr lastNode() const
Last node of the path.
bool executionFailed() const
Property: Whether execution has failed.
std::string printableName() const
Short name suitable for printing in diagnostics.
size_t nSteps() const
Length of path in steps.
bool isEmpty() const
Test for empty path.
std::vector< PathNodePtr > nodes() const
Nodes composing path.
std::vector< SymbolicExpr::Ptr > assertions() const
All SMT assertions along the path.
double processingTime() const
Total time to process path.