1 #ifndef ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
2 #define ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
8 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
9 #include <Rose/SourceLocation.h>
12 namespace BinaryAnalysis {
13 namespace ModelChecker {
22 using Ptr = ExecutionUnitPtr;
25 const SourceLocation sourceLocation_;
28 ExecutionUnit() =
delete;
29 explicit ExecutionUnit(
const SourceLocation&);
30 virtual ~ExecutionUnit();
38 virtual std::string printableName()
const = 0;
48 virtual void printSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
49 size_t stepOrigin,
size_t maxSteps)
const = 0;
52 virtual void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const = 0;
61 virtual void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
62 size_t stepOrigin,
size_t maxSteps)
const = 0;
72 void printSource(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const;
73 void printSource(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
const SourceLocation&)
const;
84 virtual size_t nSteps()
const = 0;
100 SourceLocation sourceLocation()
const;
110 virtual bool containsUnknownInsn()
const;
120 virtual std::vector<TagPtr>
121 execute(
const SettingsPtr&,
const SemanticCallbacksPtr&,
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Base class for machine instructions.
Main namespace for the ROSE library.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.