Rose::BinaryAnalysis::ModelChecker::PartitionerModel 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

using Rose::BinaryAnalysis::ModelChecker::PartitionerModel::FunctionCallStack = typedef Sawyer::Container::Stack<FunctionCall>

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 PartitionerModel.h.

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

Shared-ownership pointer for semantic state.

Definition at line 247 of file PartitionerModel.h.

Function Documentation

void Rose::BinaryAnalysis::ModelChecker::PartitionerModel::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::PartitionerModel::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::PartitionerModel::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.