cprover
janalyzer_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JANALYZER Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
99 
100 #ifndef CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
101 #define CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
102 
103 #include <util/parse_options.h>
104 #include <util/timestamper.h>
105 #include <util/ui_message.h>
106 
107 #include <langapi/language.h>
108 
112 
113 #include <analyses/ai.h>
114 #include <analyses/goto_check.h>
115 
117 
118 class bmct;
119 class goto_functionst;
120 class optionst;
121 
122 // clang-format off
123 #define JANALYZER_OPTIONS \
124  OPT_FUNCTIONS \
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  "(arch):" \
136  "(taint):(show-taint)" \
137  "(show-local-may-alias)" \
138  "(json):(xml):" \
139  "(text):(dot):" \
140  OPT_TIMESTAMP \
141  "(unreachable-instructions)(unreachable-functions)" \
142  "(reachable-functions)" \
143  "(intervals)(show-intervals)" \
144  "(non-null)(show-non-null)" \
145  "(constants)" \
146  "(dependence-graph)" \
147  "(show)(verify)(simplify):" \
148  "(location-sensitive)(concurrent)" \
149  "(no-simplify-slicing)" \
150  JAVA_BYTECODE_LANGUAGE_OPTIONS
151 // clang-format on
152 
154 {
155 public:
156  virtual int doit() override;
157  virtual void help() override;
158 
159  janalyzer_parse_optionst(int argc, const char **argv);
160 
161 protected:
164 
165  virtual void register_languages();
166 
167  virtual void get_command_line_options(optionst &options);
168 
169  virtual bool process_goto_program(const optionst &options);
170  bool set_properties();
171 
172  virtual int perform_analysis(const optionst &options);
173 
174  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
175 
177  {
178  return ui_message_handler.get_ui();
179  }
180 };
181 
182 #endif // CPROVER_JANALYZER_JANALYZER_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
janalyzer_parse_optionst
Definition: janalyzer_parse_options.h:153
ui_message_handlert
Definition: ui_message.h:19
janalyzer_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: janalyzer_parse_options.cpp:271
java_bytecode_language.h
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
janalyzer_parse_optionst::set_properties
bool set_properties()
Definition: janalyzer_parse_options.cpp:638
optionst
Definition: options.h:22
janalyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: janalyzer_parse_options.cpp:666
janalyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: janalyzer_parse_options.cpp:67
goto_model.h
goto_modelt
Definition: goto_model.h:24
show_goto_functions.h
janalyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: janalyzer_parse_options.cpp:733
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
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:60
janalyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:330
janalyzer_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: janalyzer_parse_options.h:162
show_properties.h
language.h
parse_options.h
goto_check.h
ai.h
janalyzer_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition: janalyzer_parse_options.h:176
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
janalyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:72
janalyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: janalyzer_parse_options.cpp:434
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
timestamper.h
Emit timestamps.
janalyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: janalyzer_parse_options.h:163
ui_message.h