FailureUnit.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_FailureUnit_H
#define ROSE_BinaryAnalysis_ModelChecker_FailureUnit_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER

#include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>

namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {

class FailureUnit: public ExecutionUnit {
public:
    using Ptr = FailureUnitPtr;

private:
    const Sawyer::Optional<rose_addr_t> va_;
    const std::string description_;
    TagPtr tag_;

protected:
    FailureUnit() = delete;
    FailureUnit(const Sawyer::Optional<rose_addr_t>&, const SourceLocation&, const std::string &description,
                const TagPtr&);
public:
    ~FailureUnit();

public:
    static Ptr instance(const Sawyer::Optional<rose_addr_t>&, const SourceLocation&, const std::string &description);
    static Ptr instance(const Sawyer::Optional<rose_addr_t>&, const SourceLocation&, const std::string &description, const TagPtr&);
public:
    const std::string& description() const;

public:
    virtual std::string printableName() const override;
    virtual void printSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
                            size_t stepOrigin, size_t maxSteps) const override;
    virtual void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const override;
    virtual void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
                             size_t stepOrigin, size_t maxSteps) const override;
    virtual size_t nSteps() const override;
    virtual Sawyer::Optional<rose_addr_t> address() const override;

    virtual std::vector<TagPtr>
    execute(const SettingsPtr&, const SemanticCallbacksPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
};

} // namespace
} // namespace
} // namespace

#endif
#endif