12 #include <testing-utils/catch.hpp> 37 const std::string &java_class_name,
38 const std::string &class_path,
39 const std::string &
main)
57 const std::string &java_class_name,
58 const std::string &class_path,
59 const std::string &
main)
62 command_line.
add_flag(
"no-lazy-methods");
63 command_line.
add_flag(
"no-refine-strings");
87 const std::string &java_class_name,
88 const std::string &class_path,
89 const std::string &
main,
90 std::unique_ptr<languaget> &&java_lang,
96 std::string filename=java_class_name +
".class";
102 [](
const irep_idt &name) {
return false; },
107 bool body_available) {
return false; },
120 std::istringstream java_code_stream(
"ignored");
125 language.
parse(java_code_stream, filename);
126 language.
typecheck(lazy_goto_model.symbol_table,
"");
128 language.
final(lazy_goto_model.symbol_table);
130 lazy_goto_model.load_all_functions();
132 std::unique_ptr<goto_modelt> maybe_goto_model=
134 std::move(lazy_goto_model));
135 INVARIANT(maybe_goto_model,
"Freezing lazy_goto_model failed");
138 const std::string class_symbol_name=
"java::"+java_class_name;
142 REQUIRE(class_symbol.is_type);
143 const typet &class_type=class_symbol.type;
144 REQUIRE(class_type.
id()==ID_struct);
150 INFO(
"Working directory: " << path);
155 REQUIRE_FALSE(class_type.
get_bool(ID_incomplete_class));
160 const std::string &java_class_name,
161 const std::string &class_path,
162 const std::string &
main,
163 std::unique_ptr<languaget> &&java_lang)
166 command_line.
add_flag(
"no-lazy-methods");
167 command_line.
add_flag(
"no-refine-strings");
172 command_line.
set(
"java-cp-include-files", class_path);
174 java_class_name, class_path,
main, std::move(java_lang), command_line);
symbol_tablet load_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main)
Go through the process of loading, type-checking and finalising loading a specific class file to buil...
The type of an expression.
Abstract interface to eager or lazy GOTO models.
virtual void get_language_options(const cmdlinet &)
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
null_message_handlert null_message_handler
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Model that holds partially loaded map of functions.
bool get_bool(const irep_namet &name) const
std::string get_current_working_directory()
#define INVARIANT(CONDITION, REASON)
std::unique_ptr< languaget > language
const irep_idt & id() const
virtual bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual void set(const std::string &option)
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
#define PRECONDITION(CONDITION)
std::unique_ptr< languaget > new_java_bytecode_language()
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual void set_message_handler(message_handlert &_message_handler)
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Utility for loading and parsing a specified java class file, returning the symbol table generated by ...
The symbol table base class interface.
bool has_suffix(const std::string &s, const std::string &suffix)
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
symbol_tablet load_java_class_lazy(const std::string &java_class_name, const std::string &class_path, const std::string &main)
Go through the process of loading, type-checking and finalising loading a specific class file to buil...
virtual bool parse(std::istream &instream, const std::string &path)=0
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...