cprover
Loading...
Searching...
No Matches
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
>
96
#include <
util/validation_interface.h
>
97
98
#include <
goto-programs/goto_model.h
>
99
#include <
goto-programs/show_goto_functions.h
>
100
#include <
goto-programs/show_properties.h
>
101
102
#include <
analyses/variable-sensitivity/variable_sensitivity_domain.h
>
103
#include <
ansi-c/goto-conversion/goto_check_c.h
>
104
#include <
langapi/language.h
>
105
106
class
optionst
;
107
108
// clang-format off
109
#define GOTO_ANALYSER_OPTIONS_TASKS \
110
"(show)(verify)(simplify):" \
111
"(show-on-source)" \
112
"(unreachable-instructions)(unreachable-functions)" \
113
"(reachable-functions)" \
114
"(no-standard-checks)"
115
116
#define GOTO_ANALYSER_OPTIONS_AI \
117
"(recursive-interprocedural)" \
118
"(three-way-merge)" \
119
"(legacy-ait)" \
120
"(legacy-concurrent)"
121
122
#define GOTO_ANALYSER_OPTIONS_HISTORY \
123
"(ahistorical)" \
124
"(call-stack):" \
125
"(loop-unwind):" \
126
"(branching):" \
127
"(loop-unwind-and-branching):"
128
129
#define GOTO_ANALYSER_OPTIONS_DOMAIN \
130
"(intervals)" \
131
"(non-null)" \
132
"(constants)" \
133
"(dependence-graph)" \
134
"(vsd)(variable-sensitivity)" \
135
"(dependence-graph-vs)" \
136
137
#define GOTO_ANALYSER_OPTIONS_STORAGE \
138
"(one-domain-per-history)" \
139
"(one-domain-per-location)"
140
141
#define GOTO_ANALYSER_OPTIONS_OUTPUT \
142
"(json):(xml):" \
143
"(text):(dot):"
144
145
#define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
146
"(taint):(show-taint)" \
147
"(show-local-may-alias)"
148
149
#define GOTO_ANALYSER_OPTIONS \
150
OPT_FUNCTIONS \
151
OPT_CONFIG_C_CPP \
152
OPT_CONFIG_PLATFORM \
153
OPT_SHOW_GOTO_FUNCTIONS \
154
OPT_SHOW_PROPERTIES \
155
OPT_GOTO_CHECK \
156
OPT_CONFIG_LIBRARY \
157
"(show-symbol-table)(show-parse-tree)" \
158
"(property):" \
159
"(verbosity):(version)" \
160
OPT_FLUSH \
161
OPT_TIMESTAMP \
162
OPT_VALIDATE \
163
GOTO_ANALYSER_OPTIONS_TASKS \
164
"(no-simplify-slicing)" \
165
"(show-intervals)(show-non-null)" \
166
GOTO_ANALYSER_OPTIONS_AI \
167
"(location-sensitive)(concurrent)" \
168
GOTO_ANALYSER_OPTIONS_HISTORY \
169
GOTO_ANALYSER_OPTIONS_DOMAIN \
170
OPT_VSD \
171
GOTO_ANALYSER_OPTIONS_STORAGE \
172
GOTO_ANALYSER_OPTIONS_OUTPUT \
173
GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
174
// clang-format on
175
176
class
goto_analyzer_parse_optionst
:
public
parse_options_baset
177
{
178
public
:
179
virtual
int
doit
()
override
;
180
virtual
void
help
()
override
;
181
182
goto_analyzer_parse_optionst
(
int
argc,
const
char
**argv);
183
184
protected
:
185
goto_modelt
goto_model
;
186
187
void
register_languages
()
override
;
188
189
virtual
void
get_command_line_options
(
optionst
&options);
190
191
virtual
bool
process_goto_program
(
const
optionst
&options);
192
193
virtual
int
perform_analysis
(
const
optionst
&options);
194
195
// TODO: Add documentation
196
static
void
set_default_analysis_flags
(
optionst
&options,
const
bool
enabled);
197
};
198
199
#endif
// CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
goto_analyzer_parse_optionst
Definition
goto_analyzer_parse_options.h:177
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition
goto_analyzer_parse_options.cpp:396
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition
goto_analyzer_parse_options.h:185
goto_analyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition
goto_analyzer_parse_options.cpp:89
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition
goto_analyzer_parse_options.cpp:48
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition
goto_analyzer_parse_options.cpp:696
goto_analyzer_parse_optionst::register_languages
void register_languages() override
Definition
goto_analyzer_languages.cpp:19
goto_analyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition
goto_analyzer_parse_options.cpp:462
goto_analyzer_parse_optionst::help
virtual void help() override
display command line help
Definition
goto_analyzer_parse_options.cpp:725
goto_analyzer_parse_optionst::set_default_analysis_flags
static void set_default_analysis_flags(optionst &options, const bool enabled)
Definition
goto_analyzer_parse_options.cpp:59
goto_modelt
Definition
goto_model.h:27
optionst
Definition
options.h:23
parse_options_baset
Definition
parse_options.h:20
config.h
goto_check_c.h
Program Transformation.
goto_model.h
Symbol Table + CFG.
language.h
Abstract interface to support a programming language.
parse_options.h
show_goto_functions.h
Show the goto functions.
show_properties.h
Show the properties.
timestamper.h
Emit timestamps.
ui_message.h
validation_interface.h
variable_sensitivity_domain.h
There are different ways of handling arrays, structures, unions and pointers.
goto-analyzer
goto_analyzer_parse_options.h
Generated by
1.12.0