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 "(java-throw-runtime-exceptions)" \ 35 "(java-max-input-array-length):" \ 36 "(java-max-input-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" \ 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 " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" \ 51 " entry point with null\n" \ 52 " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ 53 " --java-max-input-array-length N limit input array size to <= N\n" \ 54 " --java-max-input-tree-depth N object references are (deterministically) set to null in\n" \ 56 " --java-max-vla-length limit the length of user-code-created arrays\n" \ 57 " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" \ 58 " --lazy-methods only translate methods that appear to be reachable from\n" \ 59 " the --function entry point or main class\n" \ 60 " Note --show-symbol-table/goto-functions/properties output\n" \ 61 " will be restricted to loaded methods in this case\n" \ 62 " --lazy-methods-extra-entry-point METHODNAME\n" \ 63 " treat METHODNAME as a possible program entry point for\n" \ 64 " the purpose of lazy method loading\n" \ 65 " A '.*' wildcard is allowed to specify all class members\n" 77 #define JAVA_CLASS_MODEL_SUFFIX "@class_model" 85 std::istream &instream,
86 const std::string &path,
87 std::ostream &outstream)
override;
90 std::istream &instream,
91 const std::string &path)
override;
98 const std::string &module)
override;
132 const std::string &code,
133 const std::string &module,
138 {
return util_make_unique<java_bytecode_languaget>(); }
140 std::string
id()
const override {
return "java"; }
141 std::string
description()
const override {
return "Java Bytecode"; }
142 std::set<std::string>
extensions()
const override;
202 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H std::vector< irep_idt > java_load_classes
The type of an expression.
bool throw_assertion_error
std::unique_ptr< languaget > new_language() override
java_class_loadert java_class_loader
bool assert_uncaught_exceptions
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
size_t max_user_array_length
std::unique_ptr< languaget > new_java_bytecode_language()
const select_pointer_typet & get_pointer_type_selector() const
std::vector< irep_idt > lazy_methods_extra_entry_points
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
class_hierarchyt class_hierarchy
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...
object_factory_parameterst object_factory_parameters
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
std::set< std::string > extensions() const override
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...
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
bool typecheck(symbol_tablet &context, const std::string &module) override
nonstd::optional< T > optionalt
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Collect methods needed to be loaded using the lazy method.
Abstract interface to support a programming language.
std::string id() const override
java_bytecode_languaget(std::unique_ptr< 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...
std::string description() const override
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
std::unordered_set< std::string > no_load_classes
method_bytecodet method_bytecode
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...
Base class for all expressions.
bool parse(std::istream &instream, const std::string &path) override
The symbol table base class interface.
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
java_bytecode_languaget()
Context-insensitive lazy methods container.
bool string_refinement_enabled
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
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...
stub_global_initializer_factoryt stub_global_initializer_factory
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
std::vector< irep_idt > main_jar_classes
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produce code for simple implementation of String Java libraries.
virtual ~java_bytecode_languaget()
bool throw_runtime_exceptions