1#ifndef ROSE_BinaryAnalysis_ModelChecker_InstructionUnit_H
2#define ROSE_BinaryAnalysis_ModelChecker_InstructionUnit_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
6#include <Rose/BinaryAnalysis/Address.h>
7#include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>
12namespace BinaryAnalysis {
13namespace ModelChecker {
18class InstructionUnit:
public ExecutionUnit {
20 using Ptr = InstructionUnitPtr;
26 InstructionUnit() =
delete;
49 virtual std::string printableName()
const override;
50 virtual void printSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
51 size_t stepOrigin,
size_t maxSteps)
const override;
52 virtual void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const override;
53 virtual void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
54 size_t stepOrigin,
size_t maxSteps)
const override;
55 virtual std::vector<Sarif::LocationPtr> toSarif(
size_t maxSteps)
const override;
56 virtual size_t nSteps()
const override;
59 virtual std::vector<TagPtr>
60 execute(
const SettingsPtr&,
const SemanticCallbacksPtr&,
61 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
Holds a value or nothing.
Base class for machine instructions.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.