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/ui_message.h>
105 #include <util/parse_options.h>
106 #include <util/timestamper.h>
107 
108 #include <langapi/language.h>
109 
113 
114 #include <analyses/ai.h>
115 #include <analyses/goto_check.h>
116 
117 class bmct;
118 class goto_functionst;
119 class optionst;
120 
121 // clang-format off
122 #define GOTO_ANALYSER_OPTIONS \
123  OPT_FUNCTIONS \
124  "D:I:(std89)(std99)(std11)" \
125  "(classpath):(cp):(main-class):" \
126  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
127  "(little-endian)(big-endian)" \
128  OPT_SHOW_GOTO_FUNCTIONS \
129  OPT_SHOW_PROPERTIES \
130  OPT_GOTO_CHECK \
131  "(show-loops)" \
132  "(show-symbol-table)(show-parse-tree)" \
133  "(show-reachable-properties)(property):" \
134  "(verbosity):(version)" \
135  "(gcc)(arch):" \
136  "(taint):(show-taint)" \
137  "(show-local-may-alias)" \
138  "(json):(xml):" \
139  "(text):(dot):" \
140  OPT_FLUSH \
141  OPT_TIMESTAMP \
142  "(unreachable-instructions)(unreachable-functions)" \
143  "(reachable-functions)" \
144  "(intervals)(show-intervals)" \
145  "(non-null)(show-non-null)" \
146  "(constants)" \
147  "(dependence-graph)" \
148  "(show)(verify)(simplify):" \
149  "(location-sensitive)(concurrent)" \
150  "(no-simplify-slicing)" \
151 // clang-format on
152 
154  public parse_options_baset,
155  public messaget
156 {
157 public:
158  virtual int doit() override;
159  virtual void help() override;
160 
161  goto_analyzer_parse_optionst(int argc, const char **argv);
162 
163 protected:
166 
167  virtual void register_languages();
168 
169  virtual void get_command_line_options(optionst &options);
170 
171  virtual bool process_goto_program(const optionst &options);
172  bool set_properties();
173 
174  virtual int perform_analysis(const optionst &options);
175 
176  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
177 
179  {
180  return ui_message_handler.get_ui();
181  }
182 };
183 
184 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
uit get_ui() const
Definition: ui_message.h:37
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...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Abstract interface to support a programming language.
virtual bool process_goto_program(const optionst &options)
Program Transformation.
virtual void help() override
display command line help
virtual void get_command_line_options(optionst &options)
Abstract Interpretation.
Definition: ai.h:128
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