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/ModelChecker/Variables.h>
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
9#include <Rose/BinaryAnalysis/Variables.h>
12namespace BinaryAnalysis {
13namespace ModelChecker {
16class OutOfBoundsTag:
public Tag {
18 using Ptr = OutOfBoundsTagPtr;
24 const InstructionSemantics::BaseSemantics::SValuePtr addr_;
25 const FoundVariable intendedVariable_;
26 const FoundVariable accessedVariable_;
29 OutOfBoundsTag() =
delete;
31 const InstructionSemantics::BaseSemantics::SValuePtr &addr,
32 const FoundVariable &intendedVariable,
const FoundVariable &accessedVariable);
34 OutOfBoundsTag(
const OutOfBoundsTag&) =
delete;
50 const InstructionSemantics::BaseSemantics::SValuePtr &addr,
51 const FoundVariable &intendedVariable,
const FoundVariable &accessedVariable);
54 virtual std::string name()
const override;
55 virtual std::string printableName()
const override;
56 virtual void print(std::ostream&,
const std::string &prefix)
const override;
57 virtual void toYaml(std::ostream&,
const std::string &prefix)
const override;
58 virtual Sarif::ResultPtr toSarif(
const Sarif::AnalysisPtr&)
const override;
Base class for machine instructions.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
void print(const StackVariables &, const Partitioner2::PartitionerConstPtr &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
const char * IoMode(int64_t)
Convert Rose::BinaryAnalysis::FeasiblePath::IoMode enum constant to a string.
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.