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