cprover
janalyzer_parse_options.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JANALYZER Command Line Option Processing
4
5Author: 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
113
115class ai_baset;
117class optionst;
118
119// clang-format off
120#define JANALYZER_OPTIONS \
121 OPT_FUNCTIONS \
122 "(classpath):(cp):" \
123 OPT_JAVA_JAR \
124 "(main-class):" \
125 OPT_JAVA_GOTO_BINARY \
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_JAVA \
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{
155public:
156 int doit() override;
157 void help() override;
158
159 janalyzer_parse_optionst(int argc, const char **argv);
160
161 bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
162
164 goto_model_functiont &function,
165 const abstract_goto_modelt &model,
166 const optionst &options);
167
168 bool can_generate_function_body(const irep_idt &name);
169
171 const irep_idt &function_name,
172 symbol_table_baset &symbol_table,
173 goto_functiont &function,
174 bool body_available);
175
176protected:
177 std::unique_ptr<class_hierarchyt> class_hierarchy;
178
179 void register_languages() override;
180
181 void get_command_line_options(optionst &options);
182
183 virtual int
184 perform_analysis(goto_modelt &goto_model, const optionst &options);
185
187 goto_modelt &goto_model,
188 const optionst &,
189 const namespacet &ns);
190};
191
192#endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
Abstract interface to eager or lazy GOTO models.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
janalyzer_parse_optionst(int argc, const char **argv)
void help() override
display command line help
bool can_generate_function_body(const irep_idt &name)
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...
std::unique_ptr< class_hierarchyt > class_hierarchy
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
void get_command_line_options(optionst &options)
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
int doit() override
invoke main modules
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table base class interface.
Check for Errors in Java Programs.
Abstract interface to support a programming language.
Show the goto functions.
Show the properties.
Emit timestamps.