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):" \
126  OPT_JAVA_JAR \
127  "(main-class):" \
128  OPT_JAVA_GOTO_BINARY \
129  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
130  "(little-endian)(big-endian)" \
131  OPT_SHOW_GOTO_FUNCTIONS \
132  OPT_SHOW_PROPERTIES \
133  OPT_GOTO_CHECK \
134  "(show-loops)" \
135  "(show-symbol-table)(show-parse-tree)" \
136  "(show-reachable-properties)(property):" \
137  "(verbosity):(version)" \
138  "(arch):" \
139  "(taint):(show-taint)" \
140  "(show-local-may-alias)" \
141  "(json):(xml):" \
142  "(text):(dot):" \
143  OPT_TIMESTAMP \
144  "(unreachable-instructions)(unreachable-functions)" \
145  "(reachable-functions)" \
146  "(intervals)(show-intervals)" \
147  "(non-null)(show-non-null)" \
148  "(constants)" \
149  "(dependence-graph)" \
150  "(show)(verify)(simplify):" \
151  "(location-sensitive)(concurrent)" \
152  "(no-simplify-slicing)" \
153  JAVA_BYTECODE_LANGUAGE_OPTIONS
154 // clang-format on
155 
157 {
158 public:
159  virtual int doit() override;
160  virtual void help() override;
161 
162  janalyzer_parse_optionst(int argc, const char **argv);
163 
164  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
165 
167  goto_model_functiont &function,
168  const abstract_goto_modelt &model,
169  const optionst &options);
170 
171  bool can_generate_function_body(const irep_idt &name);
172 
174  const irep_idt &function_name,
175  symbol_table_baset &symbol_table,
176  goto_functiont &function,
177  bool body_available);
178 
179 protected:
180  std::unique_ptr<class_hierarchyt> class_hierarchy;
181 
182  void register_languages();
183 
184  void get_command_line_options(optionst &options);
185 
186  virtual int
187  perform_analysis(goto_modelt &goto_model, const optionst &options);
188 
190  goto_modelt &goto_model,
191  const optionst &,
192  const namespacet &ns);
193 };
194 
195 #endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
parse_options_baset
Definition: parse_options.h:20
janalyzer_parse_optionst
Definition: janalyzer_parse_options.h:157
janalyzer_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: janalyzer_parse_options.h:180
java_bytecode_language.h
optionst
Definition: options.h:23
janalyzer_parse_optionst::register_languages
void register_languages()
Definition: janalyzer_parse_options.cpp:72
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
janalyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: janalyzer_parse_options.cpp:741
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:63
janalyzer_parse_optionst::perform_analysis
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: janalyzer_parse_options.cpp:454
janalyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:339
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
show_properties.h
Show the properties.
language.h
Abstract interface to support a programming language.
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
parse_options.h
goto_check.h
Program Transformation.
janalyzer_parse_optionst::process_goto_function
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
Definition: janalyzer_parse_options.cpp:693
janalyzer_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: janalyzer_parse_options.cpp:667
ai.h
Abstract Interpretation.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
janalyzer_parse_optionst::get_command_line_options
void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:79
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
janalyzer_parse_optionst::generate_function_body
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
Definition: janalyzer_parse_options.cpp:731
janalyzer_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: janalyzer_parse_options.cpp:724
timestamper.h
Emit timestamps.
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
janalyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(goto_modelt &goto_model, 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:279
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
ui_message.h