cprover
goto_analyzer_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyser Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
99 
100 
101 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
102 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
103 
104 #include <util/parse_options.h>
105 #include <util/timestamper.h>
106 #include <util/ui_message.h>
108 
109 #include <langapi/language.h>
110 
114 
115 #include <analyses/ai.h>
116 #include <analyses/goto_check.h>
117 
118 class bmct;
119 class goto_functionst;
120 class optionst;
121 
122 // clang-format off
123 #define GOTO_ANALYSER_OPTIONS \
124  OPT_FUNCTIONS \
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 \
131  OPT_GOTO_CHECK \
132  "(show-loops)" \
133  "(show-symbol-table)(show-parse-tree)" \
134  "(show-reachable-properties)(property):" \
135  "(verbosity):(version)" \
136  "(gcc)(arch):" \
137  "(taint):(show-taint)" \
138  "(show-local-may-alias)" \
139  "(json):(xml):" \
140  "(text):(dot):" \
141  OPT_FLUSH \
142  OPT_TIMESTAMP \
143  "(unreachable-instructions)(unreachable-functions)" \
144  "(reachable-functions)" \
145  "(intervals)(show-intervals)" \
146  "(non-null)(show-non-null)" \
147  "(constants)" \
148  "(dependence-graph)" \
149  "(show)(verify)(simplify):" \
150  "(show-on-source)" \
151  "(location-sensitive)(concurrent)" \
152  "(no-simplify-slicing)" \
153  OPT_VALIDATE \
154 // clang-format on
155 
157  public parse_options_baset,
158  public messaget
159 {
160 public:
161  virtual int doit() override;
162  virtual void help() override;
163 
164  goto_analyzer_parse_optionst(int argc, const char **argv);
165 
166 protected:
169 
170  virtual void register_languages();
171 
172  virtual void get_command_line_options(optionst &options);
173 
174  virtual bool process_goto_program(const optionst &options);
175  bool set_properties();
176 
177  virtual int perform_analysis(const optionst &options);
178 
179  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
180 
182  {
183  return ui_message_handler.get_ui();
184  }
185 };
186 
187 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
parse_options_baset
Definition: parse_options.h:17
ui_message_handlert
Definition: ui_message.h:19
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
optionst
Definition: options.h:22
goto_analyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: goto_analyzer_parse_options.cpp:83
validation_interface.h
goto_model.h
goto_modelt
Definition: goto_model.h:24
show_goto_functions.h
goto_analyzer_parse_optionst::build_analyzer
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...
Definition: goto_analyzer_parse_options.cpp:314
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition: goto_analyzer_parse_options.cpp:67
ui_message_handlert::uit
uit
Definition: ui_message.h:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: goto_analyzer_parse_options.cpp:744
goto_analyzer_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: goto_analyzer_parse_options.h:167
show_properties.h
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: goto_analyzer_parse_options.cpp:373
language.h
goto_analyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: goto_analyzer_parse_options.cpp:817
parse_options.h
goto_check.h
ai.h
goto_analyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: goto_analyzer_parse_options.cpp:76
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_analyzer_parse_optionst
Definition: goto_analyzer_parse_options.h:156
goto_analyzer_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition: goto_analyzer_parse_options.h:181
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
timestamper.h
Emit timestamps.
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_analyzer_parse_options.h:168
goto_analyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: goto_analyzer_parse_options.cpp:483
goto_analyzer_parse_optionst::set_properties
bool set_properties()
Definition: goto_analyzer_parse_options.cpp:716
ui_message.h