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 
106 #include <langapi/language.h>
107 
110 
111 #include <analyses/goto_check.h>
112 
114 
116 class ai_baset;
118 class optionst;
119 
120 // clang-format off
121 #define JANALYZER_OPTIONS \
122  OPT_FUNCTIONS \
123  "(classpath):(cp):" \
124  OPT_JAVA_JAR \
125  "(main-class):" \
126  OPT_JAVA_GOTO_BINARY \
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  "(arch):" \
137  "(taint):(show-taint)" \
138  "(show-local-may-alias)" \
139  "(json):(xml):" \
140  "(text):(dot):" \
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  JAVA_BYTECODE_LANGUAGE_OPTIONS
152 // clang-format on
153 
155 {
156 public:
157  int doit() override;
158  void help() override;
159 
160  janalyzer_parse_optionst(int argc, const char **argv);
161 
162  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
163 
165  goto_model_functiont &function,
166  const abstract_goto_modelt &model,
167  const optionst &options);
168 
169  bool can_generate_function_body(const irep_idt &name);
170 
172  const irep_idt &function_name,
173  symbol_table_baset &symbol_table,
174  goto_functiont &function,
175  bool body_available);
176 
177 protected:
178  std::unique_ptr<class_hierarchyt> class_hierarchy;
179 
180  void register_languages() override;
181 
182  void get_command_line_options(optionst &options);
183 
184  virtual int
185  perform_analysis(goto_modelt &goto_model, const optionst &options);
186 
188  goto_modelt &goto_model,
189  const optionst &,
190  const namespacet &ns);
191 };
192 
193 #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:155
janalyzer_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: janalyzer_parse_options.h:178
java_bytecode_language.h
optionst
Definition: options.h:23
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
janalyzer_parse_optionst::register_languages
void register_languages() override
Definition: janalyzer_parse_options.cpp:64
janalyzer_parse_optionst::help
void help() override
display command line help
Definition: janalyzer_parse_options.cpp:728
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:55
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:441
janalyzer_parse_optionst::doit
int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:331
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 body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
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:680
janalyzer_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: janalyzer_parse_options.cpp:654
janalyzer_parse_optionst::get_command_line_options
void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:71
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:718
janalyzer_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: janalyzer_parse_options.cpp:711
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:271
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183