cprover
Loading...
Searching...
No Matches
goto_analyzer_parse_options.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto-Analyser Command Line Option Processing
4
5Author: 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
101
104#include <langapi/language.h>
105
106class 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
177{
178public:
179 virtual int doit() override;
180 virtual void help() override;
181
182 goto_analyzer_parse_optionst(int argc, const char **argv);
183
184protected:
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
virtual int doit() override
invoke main modules
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
static void set_default_analysis_flags(optionst &options, const bool enabled)
Program Transformation.
Symbol Table + CFG.
Abstract interface to support a programming language.
Show the goto functions.
Show the properties.
Emit timestamps.
There are different ways of handling arrays, structures, unions and pointers.