Go to the documentation of this file.
101 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
102 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
123 #define GOTO_ANALYSER_OPTIONS \
125 "D:I:(std89)(std99)(std11)" \
126 "(classpath):(cp):(main-class):" \
127 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
128 "(little-endian)(big-endian)" \
129 OPT_SHOW_GOTO_FUNCTIONS \
130 OPT_SHOW_PROPERTIES \
133 "(show-symbol-table)(show-parse-tree)" \
134 "(show-reachable-properties)(property):" \
135 "(verbosity):(version)" \
137 "(taint):(show-taint)" \
138 "(show-local-may-alias)" \
143 "(unreachable-instructions)(unreachable-functions)" \
144 "(reachable-functions)" \
145 "(intervals)(show-intervals)" \
146 "(non-null)(show-non-null)" \
148 "(dependence-graph)" \
149 "(show)(verify)(simplify):" \
151 "(location-sensitive)(concurrent)" \
152 "(no-simplify-slicing)" \
161 virtual int doit()
override;
162 virtual void help()
override;
187 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
Class that provides messages with a built-in verbosity 'level'.
Bounded model checking or path exploration for goto-programs.
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)
ui_message_handlert ui_message_handler
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
virtual void register_languages()
A collection of goto functions.
ui_message_handlert::uit get_ui()
The basic interface of an abstract interpreter.
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.