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
uit get_ui() const
Definition: ui_message.h:30
goto_analyzer_parse_optionst(int argc, const char **argv)
Show the goto functions.
Symbol Table + CFG.
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Abstract interface to support a programming language.
virtual bool process_goto_program(const optionst &options)
A collection of goto functions.
Program Transformation.
virtual void help() override
display command line help
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
virtual void get_command_line_options(optionst &options)
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Emit timestamps.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Show the properties.
virtual int doit() override
invoke main modules