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 
113 
115 class ai_baset;
117 class 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 {
155 public:
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 
176 protected:
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.