1 #ifndef ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
2 #define ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>
7 #include <Rose/BinaryAnalysis/CallingConvention.h>
8 #include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
11 namespace BinaryAnalysis {
12 namespace ModelChecker {
20 class ExternalFunctionUnit:
public ExecutionUnit {
22 using Ptr = ExternalFunctionUnitPtr;
28 ExternalFunctionUnit() =
delete;
31 ~ExternalFunctionUnit();
51 virtual std::string printableName()
const override;
52 virtual void printSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
53 size_t stepOrigin,
size_t maxSteps)
const override;
54 virtual void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const override;
55 virtual void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
56 size_t stepOrigin,
size_t maxSteps)
const override;
57 virtual size_t nSteps()
const override;
59 virtual std::vector<TagPtr> execute(
const SettingsPtr&,
const SemanticCallbacksPtr&,
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Main namespace for the ROSE library.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
Sawyer::SharedPointer< Function > FunctionPtr
Shared-ownership pointer for Function.
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.