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

Description

Model checking framework.

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

Namespaces

 P2Model
 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 error. 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  NullDerefTag
 Tag that describes a null pointer dereference. More...
 
class  OobTag
 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  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 NullDerefTagPtr = std::shared_ptr< NullDerefTag >
 
using OobTagPtr = std::shared_ptr< OobTag >
 
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 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...
 

Functions

void initDiagnostics ()
 

Variables

Sawyer::Message::Facility mlog
 

Enumeration Type Documentation

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 116 of file ModelChecker/Types.h.

Direction of data wrt storage.

Enumerator
WRITE 

Data is moving to storage.

READ 

Data is moving from storage.

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