Go to the documentation of this file.
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
30 #define JAVA_BYTECODE_LANGUAGE_OPTIONS \
31 "(disable-uncaught-exception-check)" \
32 "(throw-assertion-error)" \
33 "(java-assume-inputs-non-null)" \
34 "(throw-runtime-exceptions)" \
35 "(max-nondet-array-length):" \
36 "(max-nondet-tree-depth):" \
37 "(java-max-vla-length):" \
38 "(java-cp-include-files):" \
40 "(lazy-methods-extra-entry-point):" \
41 "(java-load-class):" \
42 "(java-no-load-class):"
44 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP \
45 " --disable-uncaught-exception-check\n" \
46 " ignore uncaught exceptions and errors\n" \
47 " --throw-assertion-error throw java.lang.AssertionError on violated\n" \
48 " assert statements instead of failing\n" \
49 " at the location of the assert statement\n" \
50 " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
51 " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" \
52 " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" \
53 " at level N references are set to null\n" \
54 " --java-assume-inputs-non-null\n" \
55 " never initialize reference-typed parameter to the\n" \
56 " entry point with null\n" \
57 " --java-max-vla-length N limit the length of user-code-created arrays\n" \
58 " --java-cp-include-files r regexp or JSON list of files to load\n" \
59 " (with '@' prefix)\n" \
60 " --no-lazy-methods load and translate all methods given on\n" \
61 " the command line and in --classpath\n" \
62 " Default is to load methods that appear to be\n" \
63 " reachable from the --function entry point\n" \
65 " Note that --show-symbol-table, --show-goto-functions\n" \
66 " and --show-properties output are restricted to\n" \
67 " loaded methods by default.\n" \
68 " --lazy-methods-extra-entry-point METHODNAME\n" \
69 " treat METHODNAME as a possible program entry\n" \
70 " point for the purpose of lazy method loading\n" \
71 " METHODNAME can be a regex that will be matched\n" \
72 " against all symbols. If missing a java:: prefix\n" \
73 " will be added. If no descriptor is found, all\n" \
74 " overloads of a method will also be added.\n"
86 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
94 std::istream &instream,
95 const std::string &path,
96 std::ostream &outstream)
override;
99 std::istream &instream,
100 const std::string &path)
override;
107 const std::string &module)
override;
142 const std::string &code,
143 const std::string &module,
148 {
return util_make_unique<java_bytecode_languaget>(); }
150 std::string
id()
const override {
return "java"; }
151 std::string
description()
const override {
return "Java Bytecode"; }
152 std::set<std::string>
extensions()
const override;
198 virtual std::vector<load_extra_methodst>
218 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
method_bytecodet method_bytecode
std::set< std::string > extensions() const override
@ LAZY_METHODS_MODE_EAGER
Non-graph-based representation of the class hierarchy.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
The type of an expression, extends irept.
std::vector< load_extra_methodst > extra_methods
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Base class for all expressions.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
java_bytecode_languaget()
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
bool parse(std::istream &instream, const std::string &path) override
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) d...
bool throw_runtime_exceptions
stub_global_initializer_factoryt stub_global_initializer_factory
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const
This method should be overloaded to provide alternative approaches for specifying extra entry points.
bool string_refinement_enabled
std::vector< irep_idt > main_jar_classes
virtual ~java_bytecode_languaget()
java_class_loadert java_class_loader
The symbol table base class interface.
void show_parse(std::ostream &out) override
lazy_methods_modet lazy_methods_mode
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::unique_ptr< languaget > new_language() override
bool assert_uncaught_exceptions
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
bool throw_assertion_error
void modules_provided(std::set< std::string > &modules) override
java_string_library_preprocesst string_preprocess
nonstd::optional< T > optionalt
Class responsible to load .class files.
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool assume_inputs_non_null
class_hierarchyt class_hierarchy
const select_pointer_typet & get_pointer_type_selector() const
bool typecheck(symbol_tablet &context, const std::string &module) override
std::string java_cp_include_files
std::vector< irep_idt > java_load_classes
std::string id() const override
size_t max_user_array_length
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
java_object_factory_parameterst object_factory_parameters
java_bytecode_languaget(std::unique_ptr< select_pointer_typet > pointer_type_selector)
std::unique_ptr< languaget > new_java_bytecode_language()
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
std::unordered_set< std::string > no_load_classes
std::string description() const override