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/parse_options.h>
93#include <util/timestamper.h>
94#include <util/ui_message.h>
96
100
102#include <ansi-c/goto_check_c.h>
103#include <langapi/language.h>
104
105class optionst;
106
107// clang-format off
108#define GOTO_ANALYSER_OPTIONS_TASKS \
109 "(show)(verify)(simplify):" \
110 "(show-on-source)" \
111 "(unreachable-instructions)(unreachable-functions)" \
112 "(reachable-functions)"
113
114#define GOTO_ANALYSER_OPTIONS_AI \
115 "(recursive-interprocedural)" \
116 "(three-way-merge)" \
117 "(legacy-ait)" \
118 "(legacy-concurrent)"
119
120#define GOTO_ANALYSER_OPTIONS_HISTORY \
121 "(ahistorical)" \
122 "(call-stack):" \
123 "(loop-unwind):" \
124 "(branching):" \
125 "(loop-unwind-and-branching):"
126
127#define GOTO_ANALYSER_OPTIONS_DOMAIN \
128 "(intervals)" \
129 "(non-null)" \
130 "(constants)" \
131 "(dependence-graph)" \
132 "(vsd)(variable-sensitivity)" \
133 "(dependence-graph-vs)" \
134
135#define GOTO_ANALYSER_OPTIONS_STORAGE \
136 "(one-domain-per-history)" \
137 "(one-domain-per-location)"
138
139#define GOTO_ANALYSER_OPTIONS_OUTPUT \
140 "(json):(xml):" \
141 "(text):(dot):"
142
143#define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
144 "(taint):(show-taint)" \
145 "(show-local-may-alias)"
146
147#define GOTO_ANALYSER_OPTIONS \
148 OPT_FUNCTIONS \
149 OPT_CONFIG_C_CPP \
150 OPT_CONFIG_PLATFORM \
151 OPT_SHOW_GOTO_FUNCTIONS \
152 OPT_SHOW_PROPERTIES \
153 OPT_GOTO_CHECK \
154 "(show-symbol-table)(show-parse-tree)" \
155 "(property):" \
156 "(verbosity):(version)" \
157 OPT_FLUSH \
158 OPT_TIMESTAMP \
159 OPT_VALIDATE \
160 GOTO_ANALYSER_OPTIONS_TASKS \
161 "(no-simplify-slicing)" \
162 "(show-intervals)(show-non-null)" \
163 GOTO_ANALYSER_OPTIONS_AI \
164 "(location-sensitive)(concurrent)" \
165 GOTO_ANALYSER_OPTIONS_HISTORY \
166 GOTO_ANALYSER_OPTIONS_DOMAIN \
167 OPT_VSD \
168 GOTO_ANALYSER_OPTIONS_STORAGE \
169 GOTO_ANALYSER_OPTIONS_OUTPUT \
170 GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
171// clang-format on
172
174{
175public:
176 virtual int doit() override;
177 virtual void help() override;
178
179 goto_analyzer_parse_optionst(int argc, const char **argv);
180
181protected:
183
184 void register_languages() override;
185
186 virtual void get_command_line_options(optionst &options);
187
188 virtual bool process_goto_program(const optionst &options);
189
190 virtual int perform_analysis(const optionst &options);
191};
192
193#endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
virtual int doit() override
invoke main modules
virtual void get_command_line_options(optionst &options)
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
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.