ROSE  0.11.82.0
Classes | Typedefs | Functions
Rose::BinaryAnalysis::ModelChecker::P2Model Namespace Reference

Description

Model checking model using Partitioner.

This model checker uses Rose::BinaryAnalysis::Partitioner2 data structures and is based on the model defined at one time by Rose::BinaryAnalysis::FeasiblePath, which this model is meant to replace.

This model uses the symbolic semantics domain. Registers are stored in a generic register state that adapts to the registers that are in use. Memory can be list- or map-based and could possibly support purely symbolic memory as well. The list- and map-based memory states can also use concrete state from a MemoryMap.

Classes

class  FunctionCall
 Describes one funtion call in the call stack. More...
 
class  RiscOperators
 RISC operators for model checking. More...
 
class  SemanticCallbacks
 Virtual definition of semantic operations for model checking. More...
 
struct  Settings
 Settings for this model. More...
 
class  State
 Semantic state. More...
 
class  SValue
 Symbolic values with memory regions. More...
 

Typedefs

using FunctionCallStack = Sawyer::Container::Stack< FunctionCall >
 Function call stack. More...
 
using StatePtr = boost::shared_ptr< class State >
 Shared-ownership pointer for semantic state. More...
 
using SValuePtr = Sawyer::SharedPointer< SValue >
 
using RiscOperatorsPtr = boost::shared_ptr< RiscOperators >
 
using SemanticCallbacksPtr = std::shared_ptr< SemanticCallbacks >
 

Functions

void commandLineDebugSwitches (Sawyer::CommandLine::SwitchGroup &, Settings &)
 Command-line switches for debug settings. More...
 
Sawyer::CommandLine::SwitchGroup commandLineModelSwitches (Settings &)
 Command-line switches for model settings. More...
 
Sawyer::CommandLine::SwitchGroup commandLineSwitches (Settings &)
 Command-line switches for settings. More...
 

Typedef Documentation

Function call stack.

A stack of functions that are in progress, with the most recent function call at the top of the stack.

Definition at line 126 of file P2Model.h.

using Rose::BinaryAnalysis::ModelChecker::P2Model::StatePtr = typedef boost::shared_ptr<class State>

Shared-ownership pointer for semantic state.

Definition at line 247 of file P2Model.h.

Function Documentation

void Rose::BinaryAnalysis::ModelChecker::P2Model::commandLineDebugSwitches ( Sawyer::CommandLine::SwitchGroup ,
Settings  
)

Command-line switches for debug settings.

Inserts some switches into the specified switch group.

Sawyer::CommandLine::SwitchGroup Rose::BinaryAnalysis::ModelChecker::P2Model::commandLineModelSwitches ( Settings )

Command-line switches for model settings.

Returns a description of command-line switches that can be used to initialize the specified settings object. Switches related to debugging are not included in the return value (see also, commandLineDebugSwitches).

Sawyer::CommandLine::SwitchGroup Rose::BinaryAnalysis::ModelChecker::P2Model::commandLineSwitches ( Settings )

Command-line switches for settings.

Returns a description of command-line switches that can be used to initialize the specified settings object. Debug switches are included in the return value.