ROSE  0.11.51.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 k = 1000;
27  double maxTime = NAN;
28  bool rejectUnknownInsns = true;
29  double solverTimeout = NAN;
30  SourceListerPtr sourceLister;
32 public:
33  Settings();
34  virtual ~Settings();
35  static Ptr instance();
36 
37 public:
45 };
46 
47 
48 } // namespace
49 } // namespace
50 } // namespace
51 
52 #endif
53 #endif
size_t k
Maximum path length in steps.
Simple settings for the model checker.
bool showAssertions
Show SMT assertions at the beginning of each execution unit.
A collection of related switch declarations.
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.
SourceListerPtr sourceLister
Object responsible for listing lines of a source code file.
bool showIntermediateStates
Show intermediate execution unit states when debugging.
bool showFinalStates
Show final execution unit states when debugging.
double solverTimeout
Timeout per SMT solver call in seconds.
bool showInitialStates
Show initial execution unit states when debugging.
double maxTime
Maximum path time in seconds.
Sawyer::CommandLine::SwitchGroup commandLineSwitches()
Command-line switches to adjust settings.