ROSE  0.11.98.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.
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.
const size_t UNLIMITED(static_cast< size_t >(-1))
Effictively unlimited size.
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.
Binary analysis.
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.