10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H 11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H 19 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 34 typedef std::map<irep_idt, lazy_method_valuet>
43 std::istream &instream,
44 const std::string &path,
45 std::ostream &outstream)
override;
48 std::istream &instream,
49 const std::string &path)
override;
53 const std::string &module)
override;
77 const std::string &code,
78 const std::string &module,
85 std::string
id()
const override {
return "java"; }
86 std::string
description()
const override {
return "Java Bytecode"; }
87 std::set<std::string>
extensions()
const override;
112 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H The type of an expression.
lazy_methodst lazy_methods
java_class_loadert java_class_loader
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
size_t max_user_array_length
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void show_parse(std::ostream &out) override
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
size_t max_nondet_array_length
virtual void lazy_methods_provided(std::set< irep_idt > &) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
bool assume_inputs_non_null
std::set< std::string > extensions() const override
languaget * new_language() override
character_refine_preprocesst character_preprocess
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
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Abstract interface to support a programming language.
std::string id() const override
std::string description() const override
std::map< irep_idt, lazy_method_valuet > lazy_methodst
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT
Base class for all expressions.
bool parse(std::istream &instream, const std::string &path) override
languaget * new_java_bytecode_language()
java_bytecode_languaget()
bool string_refinement_enabled
lazy_methods_modet lazy_methods_mode
std::pair< const symbolt *, const java_bytecode_parse_treet::methodt * > lazy_method_valuet
bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
std::vector< irep_idt > main_jar_classes
virtual ~java_bytecode_languaget()