ROSE  0.11.83.2
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | List of all members
Rose::BinaryAnalysis::ModelChecker::Settings Class Reference

Description

Simple settings for the model checker.

These are the simple, non-programming settings for the model checker. Most of these can be adjusted easily from command-line parsers.

Definition at line 17 of file ModelChecker/Settings.h.

#include <Rose/BinaryAnalysis/ModelChecker/Settings.h>

Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::Settings:
Collaboration graph
[legend]

Public Types

using Ptr = SettingsPtr
 

Public Member Functions

Sawyer::CommandLine::SwitchGroup commandLineDebugSwitches ()
 Command-line switches to adjust debug settings. More...
 
Sawyer::CommandLine::SwitchGroup commandLineModelSwitches ()
 Command-line switches to adjust model settings. More...
 

Static Public Member Functions

static Ptr instance ()
 

Public Attributes

bool showInitialStates = false
 Show initial execution unit states when debugging. More...
 
bool showIntermediateStates = false
 Show intermediate execution unit states when debugging. More...
 
bool showFinalStates = false
 Show final execution unit states when debugging. More...
 
bool showAssertions = false
 Show SMT assertions at the beginning of each execution unit. More...
 
bool ignoreSemanticFailures = false
 Treat failed instructions as if they completed. More...
 
size_t kSteps = 1000
 Maximum path length in steps. More...
 
size_t kNodes = UNLIMITED
 Maximum path length in nodes (usually basic blocks). More...
 
Sawyer::Optional< uint64_t > maxTime
 Maximum path time in seconds. More...
 
bool rejectUnknownInsns = true
 Reject "unknown" instructions even if semantic failure is allowed. More...
 
Sawyer::Optional< uint64_t > solverTimeout
 Timeout per SMT solver call in seconds. More...
 
SourceListerPtr sourceLister
 Object responsible for listing lines of a source code file. More...
 
uint64_t maxSymbolicSize = 0
 If nonzero, maximum size of symbolic expressions. More...
 
bool exploreDuplicateStates = true
 Look for duplicate states and suppress them?
 

Member Function Documentation

Sawyer::CommandLine::SwitchGroup Rose::BinaryAnalysis::ModelChecker::Settings::commandLineDebugSwitches ( )

Command-line switches to adjust debug settings.

Returns a switch group describing the command-line switches that adjust the data members of this object that are related to debugging features. This object must not be deleted before the returned switch group is used to parse a command-line.

See also, commandLineModelSwitches.

Thread safety: This method is not thread safe.

Sawyer::CommandLine::SwitchGroup Rose::BinaryAnalysis::ModelChecker::Settings::commandLineModelSwitches ( )

Command-line switches to adjust model settings.

Returns a switch group describing the command-line switches that adjust the data members of this object that are related to model checker features. This object must not be deleted before the returned switch group is used to parse a command-line.

See also, commandLineDebugSwitches.

Thread safety: This method is not thread safe.

Member Data Documentation

bool Rose::BinaryAnalysis::ModelChecker::Settings::showInitialStates = false

Show initial execution unit states when debugging.

Definition at line 21 of file ModelChecker/Settings.h.

bool Rose::BinaryAnalysis::ModelChecker::Settings::showIntermediateStates = false

Show intermediate execution unit states when debugging.

Definition at line 22 of file ModelChecker/Settings.h.

bool Rose::BinaryAnalysis::ModelChecker::Settings::showFinalStates = false

Show final execution unit states when debugging.

Definition at line 23 of file ModelChecker/Settings.h.

bool Rose::BinaryAnalysis::ModelChecker::Settings::showAssertions = false

Show SMT assertions at the beginning of each execution unit.

Definition at line 24 of file ModelChecker/Settings.h.

bool Rose::BinaryAnalysis::ModelChecker::Settings::ignoreSemanticFailures = false

Treat failed instructions as if they completed.

Definition at line 25 of file ModelChecker/Settings.h.

size_t Rose::BinaryAnalysis::ModelChecker::Settings::kSteps = 1000

Maximum path length in steps.

Definition at line 26 of file ModelChecker/Settings.h.

size_t Rose::BinaryAnalysis::ModelChecker::Settings::kNodes = UNLIMITED

Maximum path length in nodes (usually basic blocks).

Definition at line 27 of file ModelChecker/Settings.h.

Sawyer::Optional<uint64_t> Rose::BinaryAnalysis::ModelChecker::Settings::maxTime

Maximum path time in seconds.

Definition at line 28 of file ModelChecker/Settings.h.

bool Rose::BinaryAnalysis::ModelChecker::Settings::rejectUnknownInsns = true

Reject "unknown" instructions even if semantic failure is allowed.

Definition at line 29 of file ModelChecker/Settings.h.

Sawyer::Optional<uint64_t> Rose::BinaryAnalysis::ModelChecker::Settings::solverTimeout

Timeout per SMT solver call in seconds.

Definition at line 30 of file ModelChecker/Settings.h.

SourceListerPtr Rose::BinaryAnalysis::ModelChecker::Settings::sourceLister

Object responsible for listing lines of a source code file.

Definition at line 31 of file ModelChecker/Settings.h.

uint64_t Rose::BinaryAnalysis::ModelChecker::Settings::maxSymbolicSize = 0

If nonzero, maximum size of symbolic expressions.

Definition at line 32 of file ModelChecker/Settings.h.


The documentation for this class was generated from the following file: