Namespaces | Classes | Typedefs | Enumerations | Functions | Variables
Rose::BinaryAnalysis::ModelChecker Namespace Reference


Model checking framework.

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


 Model checking model using Partitioner.


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


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 >


enum  TestMode {
 Mode by which comparisons are made. More...
enum  IoMode {
 Direction of data wrt storage. More...
enum  WorkerState {


void initDiagnostics ()


Sawyer::Message::Facility mlog

Enumeration Type Documentation

Mode by which comparisons are made.


Checking is disabled.


Detection is reported if it may occur.


Detection is reported only if it must occur.

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

Direction of data wrt storage.


Data is moving to storage.


Data is moving from storage.

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