ROSE  0.11.50.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

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 96 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 217 of file P2Model.h.

Function Documentation

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.