Go to the documentation of this file.
100 #ifndef CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
101 #define CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
123 #define JANALYZER_OPTIONS \
125 "(classpath):(cp):" \
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 \
135 "(show-symbol-table)(show-parse-tree)" \
136 "(show-reachable-properties)(property):" \
137 "(verbosity):(version)" \
139 "(taint):(show-taint)" \
140 "(show-local-may-alias)" \
144 "(unreachable-instructions)(unreachable-functions)" \
145 "(reachable-functions)" \
146 "(intervals)(show-intervals)" \
147 "(non-null)(show-non-null)" \
149 "(dependence-graph)" \
150 "(show)(verify)(simplify):" \
151 "(location-sensitive)(concurrent)" \
152 "(no-simplify-slicing)" \
153 JAVA_BYTECODE_LANGUAGE_OPTIONS
159 virtual int doit()
override;
160 virtual void help()
override;
177 bool body_available);
195 #endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unique_ptr< class_hierarchyt > class_hierarchy
void register_languages()
virtual void help() override
display command line help
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
janalyzer_parse_optionst(int argc, const char **argv)
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual int doit() override
invoke main modules
The symbol table base class interface.
Abstract interface to support a programming language.
A goto function, consisting of function type (see type), function body (see body),...
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
A collection of goto functions.
void get_command_line_options(optionst &options)
This is the basic interface of the abstract interpreter with default implementations of the core func...
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
bool can_generate_function_body(const irep_idt &name)
Abstract interface to eager or lazy GOTO models.
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...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.