ROSE  0.11.102.0
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::ModelChecker::ErrorTag Class Reference

Description

Tag that describes a model checker abnormal condition.

Although these tags are always treated as non-fatal errors within the model checker in that they halt any further exploration along that path, they have a property that indicates the severity level so they can be printed more reasonably by tools.

Definition at line 19 of file ErrorTag.h.

#include <Rose/BinaryAnalysis/ModelChecker/ErrorTag.h>

Inheritance diagram for Rose::BinaryAnalysis::ModelChecker::ErrorTag:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::ErrorTag:
Collaboration graph
[legend]

Public Types

using Ptr = ErrorTagPtr
 
- Public Types inherited from Rose::BinaryAnalysis::ModelChecker::NameTag
using Ptr = NameTagPtr
 
- Public Types inherited from Rose::BinaryAnalysis::ModelChecker::Tag
using Ptr = TagPtr
 Shared ownership pointer. More...
 

Public Member Functions

std::string message () const
 Property: Error message. More...
 
void print (std::ostream &out, const std::string &prefix) const override
 Print multi-line information about the tag. More...
 
void toYaml (std::ostream &out, const std::string &prefix) const override
 Print multi-line information about the tag in YAML format. More...
 
Sawyer::Message::Importance importance () const
 Property: Importance. More...
 
void importance (Sawyer::Message::Importance)
 Property: Importance. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::NameTag
virtual std::string name () const override
 Property: Generic name of tag. More...
 
virtual std::string printableName () const override
 String to identify this tag. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::Tag
size_t nodeStep () const
 Property: Node step. More...
 

Static Public Member Functions

static Ptr instance (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *)
 Allocating constructor. More...
 
static Ptr instance (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, uint64_t)
 Allocating constructor. More...
 
static Ptr instance (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, const SymbolicExpression::Ptr &)
 Allocating constructor. More...
 
static Ptr instance (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, const InstructionSemantics::BaseSemantics::SValuePtr &)
 Allocating constructor. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::NameTag
static Ptr instance (size_t nodeStep, const std::string &name)
 Allocating constructor. More...
 

Protected Member Functions

 ErrorTag (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, const Sawyer::Optional< uint64_t > &)
 
 ErrorTag (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, const SymbolicExpression::Ptr &)
 
 ErrorTag (size_t nodeStep, const std::string &name, const std::string &mesg, SgAsmInstruction *, const InstructionSemantics::BaseSemantics::SValuePtr &)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::NameTag
 NameTag (size_t nodeStep, const std::string &name)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::Tag
 Tag (size_t nodeStep)
 

Protected Attributes

const std::string mesg_
 
SgAsmInstruction *const insn_
 
Sawyer::Optional< uint64_t > concrete_
 
const SymbolicExpression::Ptr symbolic_
 
const InstructionSemantics::BaseSemantics::SValuePtr svalue_
 
Sawyer::Message::Importance importance_ = Sawyer::Message::ERROR
 
- Protected Attributes inherited from Rose::BinaryAnalysis::ModelChecker::NameTag
const std::string name_
 

Member Function Documentation

static Ptr Rose::BinaryAnalysis::ModelChecker::ErrorTag::instance ( size_t  nodeStep,
const std::string &  name,
const std::string &  mesg,
SgAsmInstruction  
)
static

Allocating constructor.

Thread safety: This constructor is thread safe.

static Ptr Rose::BinaryAnalysis::ModelChecker::ErrorTag::instance ( size_t  nodeStep,
const std::string &  name,
const std::string &  mesg,
SgAsmInstruction ,
uint64_t   
)
static

Allocating constructor.

Thread safety: This constructor is thread safe.

static Ptr Rose::BinaryAnalysis::ModelChecker::ErrorTag::instance ( size_t  nodeStep,
const std::string &  name,
const std::string &  mesg,
SgAsmInstruction ,
const SymbolicExpression::Ptr  
)
static

Allocating constructor.

Thread safety: This constructor is thread safe.

static Ptr Rose::BinaryAnalysis::ModelChecker::ErrorTag::instance ( size_t  nodeStep,
const std::string &  name,
const std::string &  mesg,
SgAsmInstruction ,
const InstructionSemantics::BaseSemantics::SValuePtr  
)
static

Allocating constructor.

Thread safety: This constructor is thread safe.

std::string Rose::BinaryAnalysis::ModelChecker::ErrorTag::message ( ) const

Property: Error message.

Thread safety: This property access is thread safe.

Sawyer::Message::Importance Rose::BinaryAnalysis::ModelChecker::ErrorTag::importance ( ) const

Property: Importance.

ErrorTags are always treated as errors within the model checker in that they always halt exploration along the path to which they're associated. However, this importance property can be used to convey additional information to the tool that ultimately processes these tags.

void Rose::BinaryAnalysis::ModelChecker::ErrorTag::importance ( Sawyer::Message::Importance  )

Property: Importance.

ErrorTags are always treated as errors within the model checker in that they always halt exploration along the path to which they're associated. However, this importance property can be used to convey additional information to the tool that ultimately processes these tags.

void Rose::BinaryAnalysis::ModelChecker::ErrorTag::print ( std::ostream &  ,
const std::string &  prefix 
) const
overridevirtual

Print multi-line information about the tag.

First line should be the full name of the tag. Next lines are indented by at least two spaces and contain additional information about the tag. All lines start with the prefix.

Thread safety: The implementation must be thread safe for gathering the information but need not concern itself with ensuring that no other threads are sending output to the same stream.

Reimplemented from Rose::BinaryAnalysis::ModelChecker::NameTag.

void Rose::BinaryAnalysis::ModelChecker::ErrorTag::toYaml ( std::ostream &  ,
const std::string &  prefix 
) const
overridevirtual

Print multi-line information about the tag in YAML format.

The first line starts with the prefix, and the following lines start with that number of spaces.

Thread safety: The implementation must be thread safe for gathering the information but need not concern itself with ensuring that no other threads are sending output to the same stream.

Reimplemented from Rose::BinaryAnalysis::ModelChecker::NameTag.


The documentation for this class was generated from the following file: