Go to the documentation of this file.
89 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
90 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
111 #define GOTO_ANALYSER_OPTIONS_TASKS \
112 "(show)(verify)(simplify):" \
114 "(unreachable-instructions)(unreachable-functions)" \
115 "(reachable-functions)"
117 #define GOTO_ANALYSER_OPTIONS_AI \
118 "(recursive-interprocedural)" \
119 "(three-way-merge)" \
121 "(legacy-concurrent)"
123 #define GOTO_ANALYSER_OPTIONS_HISTORY \
128 "(loop-unwind-and-branching):"
130 #define GOTO_ANALYSER_OPTIONS_DOMAIN \
134 "(dependence-graph)" \
135 "(vsd)(variable-sensitivity)" \
136 "(dependence-graph-vs)" \
138 #define GOTO_ANALYSER_OPTIONS_VSD \
144 "(vsd-flow-insensitive)" \
145 "(vsd-data-dependencies)"
147 #define GOTO_ANALYSER_OPTIONS_STORAGE \
148 "(one-domain-per-history)" \
149 "(one-domain-per-location)"
151 #define GOTO_ANALYSER_OPTIONS_OUTPUT \
155 #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
156 "(taint):(show-taint)" \
157 "(show-local-may-alias)"
159 #define GOTO_ANALYSER_OPTIONS \
162 OPT_CONFIG_PLATFORM \
163 OPT_SHOW_GOTO_FUNCTIONS \
164 OPT_SHOW_PROPERTIES \
167 "(show-symbol-table)(show-parse-tree)" \
168 "(show-reachable-properties)(property):" \
169 "(verbosity):(version)" \
173 GOTO_ANALYSER_OPTIONS_TASKS \
174 "(no-simplify-slicing)" \
175 "(show-intervals)(show-non-null)" \
176 GOTO_ANALYSER_OPTIONS_AI \
177 "(location-sensitive)(concurrent)" \
178 GOTO_ANALYSER_OPTIONS_HISTORY \
179 GOTO_ANALYSER_OPTIONS_DOMAIN \
180 GOTO_ANALYSER_OPTIONS_VSD \
181 GOTO_ANALYSER_OPTIONS_STORAGE \
182 GOTO_ANALYSER_OPTIONS_OUTPUT \
183 GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
189 virtual int doit()
override;
190 virtual void help()
override;
208 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
virtual void get_command_line_options(optionst &options)
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
goto_analyzer_parse_optionst(int argc, const char **argv)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual bool process_goto_program(const optionst &options)
virtual int doit() override
invoke main modules
Abstract interface to support a programming language.
virtual void help() override
display command line help
virtual void register_languages()
A collection of goto functions.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.