Description
An execution unit that always fails.
This is a model checker execution unit that always represents an execution failure.
Definition at line 15 of file FailureUnit.h.
#include <Rose/BinaryAnalysis/ModelChecker/FailureUnit.h>
Public Types | |
| using | Ptr = FailureUnitPtr |
 Public Types inherited from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit | |
| using | Ptr = ExecutionUnitPtr |
| Shared ownership pointer for an execution unit. More... | |
Public Member Functions | |
| const std::string & | description () const |
| Property: Description. More... | |
| virtual std::string | printableName () const override |
| Property: Printable name. More... | |
| virtual void | printSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const override |
| Print the steps for this execution unit. More... | |
| virtual void | toYamlHeader (const SettingsPtr &, std::ostream &, const std::string &prefix) const override |
| Print the header information in YAML format. More... | |
| virtual void | toYamlSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const override |
| Print the steps for this execution unit in YAML format. More... | |
| virtual size_t | nSteps () const override |
| Property: Number of steps required to execute this unit. More... | |
| virtual Sawyer::Optional< rose_addr_t > | address () const override |
| Property: Address if it has one. More... | |
| virtual std::vector< TagPtr > | execute (const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override |
| Execute the unit to create a new state. More... | |
| Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit | |
| ExecutionUnit (const SourceLocation &) | |
| SourceLocation | sourceLocation () const |
| Property: Location in source code. More... | |
| virtual bool | containsUnknownInsn () const |
| Predicate to test for unknown instructions. More... | |
| TagPtr | executeInstruction (const SettingsPtr &, SgAsmInstruction *, const InstructionSemantics::BaseSemantics::DispatcherPtr &, size_t nodeStep) |
| Execute a single instruction semantically. More... | |
| void | printSource (const SettingsPtr &, std::ostream &, const std::string &prefix) const |
| List source location. More... | |
| void | printSource (const SettingsPtr &, std::ostream &, const std::string &prefix, const SourceLocation &) const |
| List source location. More... | |
Static Public Member Functions | |
| static Ptr | instance (const Sawyer::Optional< rose_addr_t > &, const SourceLocation &, const std::string &description) |
| Allocating constructor. More... | |
| static Ptr | instance (const Sawyer::Optional< rose_addr_t > &, const SourceLocation &, const std::string &description, const TagPtr &) |
| Allocating constructor. More... | |
Protected Member Functions | |
| FailureUnit (const Sawyer::Optional< rose_addr_t > &, const SourceLocation &, const std::string &description, const TagPtr &) | |
Member Function Documentation
|
static |
Allocating constructor.
Constructs a new execution unit to represent an execution failure. The descriptive string must not be empty and should be a single line of text without vertical characters or leading/trailing white space.
If a tag is provided, then it is thrown when this unit is executed.
Thread safety: This constructor is thread safe.
|
static |
Allocating constructor.
Constructs a new execution unit to represent an execution failure. The descriptive string must not be empty and should be a single line of text without vertical characters or leading/trailing white space.
If a tag is provided, then it is thrown when this unit is executed.
Thread safety: This constructor is thread safe.
| const std::string& Rose::BinaryAnalysis::ModelChecker::FailureUnit::description | ( | ) | const |
Property: Description.
Description of the failure as a single line of text with no vertical characters or leading/trailing white space. The description can only be set in the constructor.
Thread safety: This method is thread safe.
|
overridevirtual |
Property: Printable name.
This returns the name of this unit as a single line that is suitable for terminal output.
Thread safety: The implementation must be thread safe.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Print the steps for this execution unit.
The output should show each step starting on its own line indented by the specified prefix. The steps should be numbered starting from stepOrigin. Additional details about the step should be on subsequent lines and indented in units of two spaces at a time.
Thread safety: The implementation must be thread safe but may allow other threads to output to the same stream concurrently.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Print the header information in YAML format.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Print the steps for this execution unit in YAML format.
The output should show each step starting on its own line indented by the specified prefix. The steps should be numbered starting from stepOrigin. Additional details about the steps should be indented further.
Thread safety: The implementation must be thread safe but may allow other threads to output to the same stream concurrently.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Property: Number of steps required to execute this unit.
This is a user-defined measure of the approximate difficulty of executing this unit. For instance, it could be the number of instructions that are executed. The number of steps returned by this method should generally agree with the number of steps printed when displaying this unit.
Thread safety: The implementation must be thread safe. The easiest way to achieve this is to ensure that the information doesn't change during model checking.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Property: Address if it has one.
Returns the address of this execution unit if it has one.
The default implementation always returns nothing.
Thread safety: The implementation must be thread safe.
Reimplemented from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
overridevirtual |
Execute the unit to create a new state.
The supplied riscOperators argument has an attached state that should be modified in place according to the semantics of the execution unit. It returns zero or more tags to be added to the path node.
This method is not responsible for adding new paths to the work queue–it only updates the state.
Thread safety: The implementation need not be thread safe.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
The documentation for this class was generated from the following file:
