ROSE  0.11.51.0
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 <Settings.h>

Public Types

using Ptr = SettingsPtr
 

Public Member Functions

Sawyer::CommandLine::SwitchGroup commandLineSwitches ()
 Command-line switches to adjust 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 k = 1000
 Maximum path length in steps. More...
 
double maxTime = NAN
 Maximum path time in seconds. More...
 
bool rejectUnknownInsns = true
 Reject "unknown" instructions even if semantic failure is allowed. More...
 
double solverTimeout = NAN
 Timeout per SMT solver call in seconds. More...
 
SourceListerPtr sourceLister
 Object responsible for listing lines of a source code file. More...
 

Member Function Documentation

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

Command-line switches to adjust settings.

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

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::k = 1000

Maximum path length in steps.

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

double Rose::BinaryAnalysis::ModelChecker::Settings::maxTime = NAN

Maximum path time in seconds.

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

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

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

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

double Rose::BinaryAnalysis::ModelChecker::Settings::solverTimeout = NAN

Timeout per SMT solver call in seconds.

NAN means no timeout.

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

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

Object responsible for listing lines of a source code file.

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


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