ModelChecker/Settings.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_Settings_H
#define ROSE_BinaryAnalysis_ModelChecker_Settings_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER
 
#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
#include <Rose/Constants.h>
 
#include <Sawyer/CommandLine.h>
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
class Settings {
public:
    using Ptr = SettingsPtr;
public:
    bool showInitialStates = false;                     
    bool showIntermediateStates = false;                
    bool showFinalStates = false;                       
    bool showAssertions = false;                        
    bool ignoreSemanticFailures = false;                
    size_t kSteps = 1000;                               
    size_t kNodes = UNLIMITED;                          
    Sawyer::Optional<uint64_t> maxTime;                 
    bool rejectUnknownInsns = true;                     
    Sawyer::Optional<uint64_t> solverTimeout;           
    SourceListerPtr sourceLister;                       
    uint64_t maxSymbolicSize = 0;                       
    bool exploreDuplicateStates = true;                 
public:
    Settings();
    virtual ~Settings();
    static Ptr instance();
 
public:
    Sawyer::CommandLine::SwitchGroup commandLineDebugSwitches();
 
    Sawyer::CommandLine::SwitchGroup commandLineModelSwitches();
};
 
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif