ROSE  0.11.145.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_MODEL_CHECKER
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;
30  Sawyer::Optional<uint64_t> solverTimeout;
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:
50  Sawyer::CommandLine::SwitchGroup commandLineDebugSwitches();
51 
61  Sawyer::CommandLine::SwitchGroup commandLineModelSwitches();
62 };
63 
64 
65 } // namespace
66 } // namespace
67 } // namespace
68 
69 #endif
70 #endif
A collection of related switch declarations.
Main namespace for the ROSE library.
const size_t UNLIMITED(static_cast< size_t >(-1))
Effictively unlimited size.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.