89#ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
90#define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
109#define GOTO_ANALYSER_OPTIONS_TASKS \
110 "(show)(verify)(simplify):" \
112 "(unreachable-instructions)(unreachable-functions)" \
113 "(reachable-functions)"
115#define GOTO_ANALYSER_OPTIONS_AI \
116 "(recursive-interprocedural)" \
117 "(three-way-merge)" \
119 "(legacy-concurrent)"
121#define GOTO_ANALYSER_OPTIONS_HISTORY \
126 "(loop-unwind-and-branching):"
128#define GOTO_ANALYSER_OPTIONS_DOMAIN \
132 "(dependence-graph)" \
133 "(vsd)(variable-sensitivity)" \
134 "(dependence-graph-vs)" \
136#define GOTO_ANALYSER_OPTIONS_STORAGE \
137 "(one-domain-per-history)" \
138 "(one-domain-per-location)"
140#define GOTO_ANALYSER_OPTIONS_OUTPUT \
144#define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
145 "(taint):(show-taint)" \
146 "(show-local-may-alias)"
148#define GOTO_ANALYSER_OPTIONS \
151 OPT_CONFIG_PLATFORM \
152 OPT_SHOW_GOTO_FUNCTIONS \
153 OPT_SHOW_PROPERTIES \
156 "(show-symbol-table)(show-parse-tree)" \
157 "(show-reachable-properties)(property):" \
158 "(verbosity):(version)" \
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 \
170 GOTO_ANALYSER_OPTIONS_STORAGE \
171 GOTO_ANALYSER_OPTIONS_OUTPUT \
172 GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
178 virtual int doit()
override;
179 virtual void help()
override;
virtual int doit() override
invoke main modules
virtual void get_command_line_options(optionst &options)
virtual bool process_goto_program(const optionst &options)
void register_languages() override
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
Abstract interface to support a programming language.
There are different ways of handling arrays, structures, unions and pointers.