ROSE  0.11.82.0
ModelChecker/Settings.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Settings_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Settings_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 #include <Sawyer/CommandLine.h>
8 
9 namespace Rose {
10 namespace BinaryAnalysis {
11 namespace ModelChecker {
12 
17 class Settings {
18 public:
19  using Ptr = SettingsPtr;
20 public:
21  bool showInitialStates = false;
22  bool showIntermediateStates = false;
23  bool showFinalStates = false;
24  bool showAssertions = false;
25  bool ignoreSemanticFailures = false;
26  size_t kSteps = 1000;
27  size_t kNodes = UNLIMITED;
29  bool rejectUnknownInsns = true;
31  SourceListerPtr sourceLister;
32  uint64_t maxSymbolicSize = 0;
33  bool exploreDuplicateStates = true;
35 public:
36  Settings();
37  virtual ~Settings();
38  static Ptr instance();
39 
40 public:
51 
62 };
63 
64 
65 } // namespace
66 } // namespace
67 } // namespace
68 
69 #endif
70 #endif
size_t kSteps
Maximum path length in steps.
const size_t UNLIMITED(-1)
Effictively unlimited size.
uint64_t maxSymbolicSize
If nonzero, maximum size of symbolic expressions.
Sawyer::CommandLine::SwitchGroup commandLineDebugSwitches()
Command-line switches to adjust debug settings.
Simple settings for the model checker.
bool showAssertions
Show SMT assertions at the beginning of each execution unit.
size_t kNodes
Maximum path length in nodes (usually basic blocks).
A collection of related switch declarations.
bool exploreDuplicateStates
Look for duplicate states and suppress them?
Main namespace for the ROSE library.
bool ignoreSemanticFailures
Treat failed instructions as if they completed.
bool rejectUnknownInsns
Reject "unknown" instructions even if semantic failure is allowed.
Sawyer::CommandLine::SwitchGroup commandLineModelSwitches()
Command-line switches to adjust model settings.
SourceListerPtr sourceLister
Object responsible for listing lines of a source code file.
bool showIntermediateStates
Show intermediate execution unit states when debugging.
Sawyer::Optional< uint64_t > maxTime
Maximum path time in seconds.
bool showFinalStates
Show final execution unit states when debugging.
bool showInitialStates
Show initial execution unit states when debugging.
Sawyer::Optional< uint64_t > solverTimeout
Timeout per SMT solver call in seconds.