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
janalyzer_parse_optionst(int argc, const char **argv)
uit get_ui() const
Definition: ui_message.h:37
Show the goto functions.
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Symbol Table + CFG.
virtual int doit() override
invoke main modules
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Abstract interface to support a programming language.
Program Transformation.
virtual bool process_goto_program(const optionst &options)
virtual void get_command_line_options(optionst &options)
ui_message_handlert::uit get_ui()
Abstract Interpretation.
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: ai.h:128
Emit timestamps.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Show the properties.
virtual void help() override
display command line help
ui_message_handlert ui_message_handler