cprover
goto_analyzer_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyser Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
88 
89 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
90 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
91 
92 #include <util/config.h>
93 #include <util/parse_options.h>
94 #include <util/timestamper.h>
95 #include <util/ui_message.h>
97 
98 #include <langapi/language.h>
99 
103 
104 #include <analyses/ai.h>
105 #include <analyses/goto_check.h>
106 
107 class goto_functionst;
108 class optionst;
109 
110 // clang-format off
111 #define GOTO_ANALYSER_OPTIONS_TASKS \
112  "(show)(verify)(simplify):" \
113  "(show-on-source)" \
114  "(unreachable-instructions)(unreachable-functions)" \
115  "(reachable-functions)"
116 
117 #define GOTO_ANALYSER_OPTIONS_AI \
118  "(recursive-interprocedural)" \
119  "(three-way-merge)" \
120  "(legacy-ait)" \
121  "(legacy-concurrent)"
122 
123 #define GOTO_ANALYSER_OPTIONS_HISTORY \
124  "(ahistorical)" \
125  "(call-stack):" \
126  "(loop-unwind):" \
127  "(branching):" \
128  "(loop-unwind-and-branching):"
129 
130 #define GOTO_ANALYSER_OPTIONS_DOMAIN \
131  "(intervals)" \
132  "(non-null)" \
133  "(constants)" \
134  "(dependence-graph)" \
135  "(vsd)(variable-sensitivity)" \
136  "(dependence-graph-vs)" \
137 
138 #define GOTO_ANALYSER_OPTIONS_VSD \
139  "(vsd-values):" \
140  "(vsd-structs):" \
141  "(vsd-arrays):" \
142  "(vsd-pointers):" \
143  "(vsd-unions):" \
144  "(vsd-flow-insensitive)" \
145  "(vsd-data-dependencies)"
146 
147 #define GOTO_ANALYSER_OPTIONS_STORAGE \
148  "(one-domain-per-history)" \
149  "(one-domain-per-location)"
150 
151 #define GOTO_ANALYSER_OPTIONS_OUTPUT \
152  "(json):(xml):" \
153  "(text):(dot):"
154 
155 #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
156  "(taint):(show-taint)" \
157  "(show-local-may-alias)"
158 
159 #define GOTO_ANALYSER_OPTIONS \
160  OPT_FUNCTIONS \
161  OPT_CONFIG_C_CPP \
162  OPT_CONFIG_PLATFORM \
163  OPT_SHOW_GOTO_FUNCTIONS \
164  OPT_SHOW_PROPERTIES \
165  OPT_GOTO_CHECK \
166  "(show-loops)" \
167  "(show-symbol-table)(show-parse-tree)" \
168  "(show-reachable-properties)(property):" \
169  "(verbosity):(version)" \
170  OPT_FLUSH \
171  OPT_TIMESTAMP \
172  OPT_VALIDATE \
173  GOTO_ANALYSER_OPTIONS_TASKS \
174  "(no-simplify-slicing)" \
175  "(show-intervals)(show-non-null)" \
176  GOTO_ANALYSER_OPTIONS_AI \
177  "(location-sensitive)(concurrent)" \
178  GOTO_ANALYSER_OPTIONS_HISTORY \
179  GOTO_ANALYSER_OPTIONS_DOMAIN \
180  GOTO_ANALYSER_OPTIONS_VSD \
181  GOTO_ANALYSER_OPTIONS_STORAGE \
182  GOTO_ANALYSER_OPTIONS_OUTPUT \
183  GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
184 // clang-format on
185 
187 {
188 public:
189  virtual int doit() override;
190  virtual void help() override;
191 
192  goto_analyzer_parse_optionst(int argc, const char **argv);
193 
194 protected:
196 
197  virtual void register_languages();
198 
199  virtual void get_command_line_options(optionst &options);
200 
201  virtual bool process_goto_program(const optionst &options);
202 
203  virtual int perform_analysis(const optionst &options);
204 
205  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
206 };
207 
208 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
virtual int doit() override
invoke main modules
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Program Transformation.
Symbol Table + CFG.
Abstract interface to support a programming language.
Show the goto functions.
Show the properties.
Emit timestamps.