Rose::BinaryAnalysis::ModelChecker Namespace Reference

Description

Model checking framework.

TODO: [Robb Matzke 2021-04-09] Top level model checker documentation.

Namespaces
	PartitionerModel
	Model checking model using Partitioner.

Classes
class	AlwaysTrue
	Path predicate that's always true. More...
class	BasicBlockUnit
	An execution unit for a basic block. More...
class	Engine
	Main class for model checking. More...
class	ErrorTag
	Tag that describes a model checker abnormal condition. More...
class	Exception
	Base class for model checker exceptions. More...
class	ExecutionUnit
	One unit of execution. More...
class	ExternalFunctionUnit
	An execution unit for an externally linked function. More...
class	FailureUnit
	An execution unit that always fails. More...
class	FastestPathFirst
	Prioritize paths by how long they take. More...
class	HasFinalTags
	Default interesting predicate. More...
class	InstructionUnit
	An execution unit for a single instruction. More...
class	LongestPathFirst
	Prioritize longer paths. More...
class	NameTag
	Base class for tags that have a name. More...
class	NullDereferenceTag
	Tag that describes a null pointer dereference. More...
class	OutOfBoundsTag
	Tag that describes an out-of-bounds memory access. More...
class	ParseError
	Parse errors. More...
class	Path
	Execution path. More...
class	PathNode
class	PathPredicate
	Path predicate. More...
class	PathPrioritizer
	Base class for prioritizing work. More...
class	PathQueue
	List of path endpoints in an execution tree. More...
class	Periodic
	Do something periodically in another thread. More...
class	RandomPathFirst
	Prioritize paths randomly. More...
class	SemanticCallbacks
	User-defined functions for model checking semantics. More...
class	Settings
	Simple settings for the model checker. More...
class	ShortestPathFirst
	Prioritize shorter paths. More...
class	SourceLister
	Lists parts of source files. More...
class	Tag
	Information tagged to a path node. More...
struct	ThrownTag
	Exception wrapper for tags. More...
class	UninitializedVariableTag
	Tag that describes an out-of-bounds memory access. More...
class	WorkerStatus
	Writes information about workers to a text file for debugging. More...
class	WorkPredicate
	Default work queue predicate. More...

Typedefs
using	AlwaysTruePtr = std::shared_ptr< AlwaysTrue >
using	BasicBlockUnitPtr = std::shared_ptr< BasicBlockUnit >
using	EnginePtr = std::shared_ptr< Engine >
using	ErrorTagPtr = std::shared_ptr< ErrorTag >
using	ExecutionUnitPtr = std::shared_ptr< ExecutionUnit >
using	ExternalFunctionUnitPtr = std::shared_ptr< ExternalFunctionUnit >
using	FailureUnitPtr = std::shared_ptr< FailureUnit >
using	FastestPathFirstPtr = std::shared_ptr< FastestPathFirst >
using	HasFinalTagsPtr = std::shared_ptr< HasFinalTags >
using	InstructionUnitPtr = std::shared_ptr< InstructionUnit >
using	LongestPathFirstPtr = std::shared_ptr< LongestPathFirst >
using	NameTagPtr = std::shared_ptr< NameTag >
using	NullDereferenceTagPtr = std::shared_ptr< NullDereferenceTag >
using	OutOfBoundsTagPtr = std::shared_ptr< OutOfBoundsTag >
using	PathPtr = std::shared_ptr< Path >
using	PathNodePtr = std::shared_ptr< PathNode >
using	PathPredicatePtr = std::shared_ptr< PathPredicate >
using	PathPrioritizerPtr = std::shared_ptr< PathPrioritizer >
using	PathQueuePtr = std::shared_ptr< PathQueue >
using	PeriodicPtr = std::shared_ptr< Periodic >
using	RandomPathFirstPtr = std::shared_ptr< RandomPathFirst >
using	SemanticCallbacksPtr = std::shared_ptr< SemanticCallbacks >
using	SettingsPtr = std::shared_ptr< Settings >
using	ShortestPathFirstPtr = std::shared_ptr< ShortestPathFirst >
using	SourceListerPtr = std::shared_ptr< SourceLister >
using	TagPtr = std::shared_ptr< Tag >
using	UninitializedVariableTagPtr = std::shared_ptr< UninitializedVariableTag >
using	WorkerStatusPtr = std::shared_ptr< WorkerStatus >
using	WorkPredicatePtr = std::shared_ptr< WorkPredicate >

Enumerations
enum	TestMode {   TestMode::OFF,   TestMode::MAY,   TestMode::MUST }
	Mode by which comparisons are made. More...
enum	IoMode {   IoMode::WRITE,   IoMode::READ }
	Direction of data wrt storage. More...
enum	WorkerState {   STARTING,   WAITING,   WORKING,   FINISHED }

Functions
void	initDiagnostics ()

Variables
Sawyer::Message::Facility	mlog

Enumeration Type Documentation

enum Rose::BinaryAnalysis::ModelChecker::TestMode

strong

Mode by which comparisons are made.

Enumerator
OFF	Checking is disabled.
MAY	Detection is reported if it may occur.
MUST	Detection is reported only if it must occur.

Definition at line 122 of file ModelChecker/Types.h.

enum Rose::BinaryAnalysis::ModelChecker::IoMode

strong

Direction of data wrt storage.

Enumerator
WRITE	Data is moving to storage.
READ	Data is moving from storage.

Definition at line 129 of file ModelChecker/Types.h.