1 #ifndef ROSE_BinaryAnalysis_ModelChecker_OutOfBoundsTag_H
2 #define ROSE_BinaryAnalysis_ModelChecker_OutOfBoundsTag_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/ModelChecker/Tag.h>
7 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/Types.h>
8 #include <Rose/BinaryAnalysis/Variables.h>
11 namespace BinaryAnalysis {
12 namespace ModelChecker {
15 class OutOfBoundsTag:
public Tag {
17 using Ptr = OutOfBoundsTagPtr;
24 const Variables::StackVariable intendedVariable_;
26 const Variables::StackVariable accessedVariable_;
30 OutOfBoundsTag() =
delete;
33 const Variables::StackVariable &intendedVariable,
const AddressInterval &intendedVariableLocation,
34 const Variables::StackVariable &accessedVariable,
const AddressInterval &accessedVariableLocation);
36 OutOfBoundsTag(
const OutOfBoundsTag&) =
delete;
53 const Variables::StackVariable &intendedVariable,
const AddressInterval &intendedVariableLocation,
54 const Variables::StackVariable &accessedVariable,
const AddressInterval &accessedVariableLocation);
57 virtual std::string name()
const override;
58 virtual std::string printableName()
const override;
59 virtual void print(std::ostream&,
const std::string &prefix)
const override;
60 virtual void toYaml(std::ostream&,
const std::string &prefix)
const override;
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.
Base class for machine instructions.
const char * IoMode(int64_t)
Convert Rose::BinaryAnalysis::FeasiblePath::IoMode enum constant to a string.
void print(const StackVariables &, const Partitioner2::Partitioner &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
Main namespace for the ROSE library.
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.