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