ROSE  0.11.109.0
Path.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Path_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Path_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 
8 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/Types.h>
9 #include <Rose/BinaryAnalysis/SmtSolver.h>
10 #include <Rose/BinaryAnalysis/SymbolicExpression.h>
11 #include <Combinatorics.h>
12 
13 namespace Rose {
14 namespace BinaryAnalysis {
15 namespace ModelChecker {
16 
21 class Path {
22 public:
23  using Ptr = PathPtr;
24 
25 private:
26  PathNodePtr end_;
27 
28 protected:
29  Path() = delete;
30  explicit Path(const PathNodePtr &end);
31 public:
32  ~Path();
33 
34 public:
40  static Ptr instance(const ExecutionUnitPtr&);
41 
49  static Ptr instance(const PathPtr &prefix, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
50  const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
51 
57  bool isEmpty() const;
58 
64  size_t nNodes() const;
65 
71  size_t nSteps() const;
72 
80  double processingTime() const;
81 
90  uint64_t hash() const;
91  void hash(Combinatorics::Hasher&) const;
99  bool executionFailed() const;
100 
106  std::vector<SymbolicExpression::Ptr> assertions() const;
107 
113  PathNodePtr lastNode() const;
114 
123  std::vector<PathNodePtr> nodes() const;
124 
128  std::string printableName() const;
129 
136  void print(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
137 
144  void toYaml(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
145 
146 
147 };
148 
149 } // namespace
150 } // namespace
151 } // namespace
152 
153 #endif
154 #endif
boost::filesystem::path Path
Name of entities in a filesystem.
void print(const StackVariables &, const Partitioner2::Partitioner &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
Main namespace for the ROSE library.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Sawyer::Container::Map< std::string, SymbolicExpression::Ptr > Evidence
Evidence of satisfiability.
Definition: SmtSolver.h:566
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
uint64_t nNodes(InputIterator begin, InputIterator end)
Counts the number of nodes.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.