Path.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_Path_H
#define ROSE_BinaryAnalysis_ModelChecker_Path_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER
 
#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
 
#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <Rose/BinaryAnalysis/SymbolicExpression.h>
#include <Combinatorics.h>
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
class Path {
public:
    using Ptr = PathPtr;
 
private:
    PathNodePtr end_;
 
protected:
    Path() = delete;
    explicit Path(const PathNodePtr &end);
public:
    ~Path();
 
public:
    static Ptr instance(const ExecutionUnitPtr&);
 
    static Ptr instance(const PathPtr &prefix, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
                        const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
 
    bool isEmpty() const;
 
    size_t nNodes() const;
 
    size_t nSteps() const;
 
    double processingTime() const;
 
    uint64_t hash() const;
    void hash(Combinatorics::Hasher&) const;
    bool executionFailed() const;
 
    std::vector<SymbolicExpression::Ptr> assertions() const;
 
    PathNodePtr lastNode() const;
 
    PathNodePtr firstNode() const;
 
    std::vector<PathNodePtr> nodes() const;
 
    std::string printableName() const;
 
    void print(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
 
    void toYaml(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
 
    std::vector<Sarif::LocationPtr> toSarif(size_t maxSteps) const;
};
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif