ROSE  0.11.123.0
Types.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Types_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Types_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
6 #include <memory>
7 
8 namespace Rose {
9 namespace BinaryAnalysis {
10 
14 namespace ModelChecker {
15 
16 class AlwaysTrue;
17 using AlwaysTruePtr = std::shared_ptr<AlwaysTrue>;
18 
19 class BasicBlockUnit;
20 using BasicBlockUnitPtr = std::shared_ptr<BasicBlockUnit>;
21 
22 class Engine;
23 using EnginePtr = std::shared_ptr<Engine>;
24 
25 class ErrorTag;
26 using ErrorTagPtr = std::shared_ptr<ErrorTag>;
27 
28 class Exception;
29 
30 class ExecutionUnit;
31 using ExecutionUnitPtr = std::shared_ptr<ExecutionUnit>;
32 
33 class ExternalFunctionUnit;
34 using ExternalFunctionUnitPtr = std::shared_ptr<ExternalFunctionUnit>;
35 
36 class FailureUnit;
37 using FailureUnitPtr = std::shared_ptr<FailureUnit>;
38 
39 class FastestPathFirst;
40 using FastestPathFirstPtr = std::shared_ptr<FastestPathFirst>;
41 
42 class FoundVariable;
43 
44 class HasFinalTags;
45 using HasFinalTagsPtr = std::shared_ptr<HasFinalTags>;
46 
47 class InstructionUnit;
48 using InstructionUnitPtr = std::shared_ptr<InstructionUnit>;
49 
50 class LongestPathFirst;
51 using LongestPathFirstPtr = std::shared_ptr<LongestPathFirst>;
52 
53 class NameTag;
54 using NameTagPtr = std::shared_ptr<NameTag>;
55 
56 class NullDereferenceTag;
57 using NullDereferenceTagPtr = std::shared_ptr<NullDereferenceTag>;
58 
59 class OutOfBoundsTag;
60 using OutOfBoundsTagPtr = std::shared_ptr<OutOfBoundsTag>;
61 
62 class ParseError;
63 
64 class Path;
65 using PathPtr = std::shared_ptr<Path>;
66 
67 class PathNode;
68 using PathNodePtr = std::shared_ptr<PathNode>;
69 
70 class PathPredicate;
71 using PathPredicatePtr = std::shared_ptr<PathPredicate>;
72 
73 class PathPrioritizer;
74 using PathPrioritizerPtr = std::shared_ptr<PathPrioritizer>;
75 
76 class PathQueue;
77 using PathQueuePtr = std::shared_ptr<PathQueue>;
78 
79 class Periodic;
80 using PeriodicPtr = std::shared_ptr<Periodic>;
81 
82 class RandomPathFirst;
83 using RandomPathFirstPtr = std::shared_ptr<RandomPathFirst>;
84 
85 class SemanticCallbacks;
86 using SemanticCallbacksPtr = std::shared_ptr<SemanticCallbacks>;
87 
88 class Settings;
89 using SettingsPtr = std::shared_ptr<Settings>;
90 
91 class ShortestPathFirst;
92 using ShortestPathFirstPtr = std::shared_ptr<ShortestPathFirst>;
93 
94 class SourceLister;
95 using SourceListerPtr = std::shared_ptr<SourceLister>;
96 
97 class Tag;
98 using TagPtr = std::shared_ptr<Tag>;
99 
100 class UninitializedVariableTag;
101 using UninitializedVariableTagPtr = std::shared_ptr<UninitializedVariableTag>;
102 
103 class WorkerStatus;
104 using WorkerStatusPtr = std::shared_ptr<WorkerStatus>;
105 
106 class WorkPredicate;
107 using WorkPredicatePtr = std::shared_ptr<WorkPredicate>;
108 
110 void initDiagnostics();
111 
112 namespace PartitionerModel {
113  class SValue;
115 
116  class RiscOperators;
117  using RiscOperatorsPtr = boost::shared_ptr<RiscOperators>;
118 
119  class SemanticCallbacks;
120  using SemanticCallbacksPtr = std::shared_ptr<SemanticCallbacks>;
121 }
122 
124 enum class TestMode {
125  OFF,
126  MAY,
127  MUST
128 };
129 
131 enum class IoMode {
132  WRITE,
133  READ
134 };
135 
136 
137 // Worker states. Used internally.
138 enum class WorkerState {
139  STARTING, // thread is initializing
140  WAITING, // thread is looking for new work
141  WORKING, // thread is actively working on a path
142  FINISHED // thread will never work again and is cleaning up
143 };
144 
145 #define UNMANAGED_WORKER ((size_t)-1) // non-ID for an unmanaged worker; I.e., a user thread
146 
147 } // namespace
148 } // namespace
149 } // namespace
150 
151 #endif
152 #endif
boost::filesystem::path Path
Name of entities in a filesystem.
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.
Collection of streams.
Definition: Message.h:1606
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
ROSE_DLL_API Sawyer::Message::Facility mlog
Diagnostic facility for the ROSE library as a whole.
const char * IoMode(int64_t)
Convert Rose::BinaryAnalysis::FeasiblePath::IoMode enum constant to a string.
Main namespace for the ROSE library.
Disable colored output.
Definition: Color.h:23
Rose::BinaryAnalysis::DataFlow::Engine< DfCfg, InstructionSemantics::BaseSemantics::StatePtr, TransferFunction, MergeFunction > Engine
Data-Flow engine.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
const char * WorkerState(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::WorkerState enum constant to a string.
void initDiagnostics()
Initialize diagnostics.