Go to the documentation of this file.
12 #include <testing-utils/catch.hpp>
36 const std::string &java_class_name,
37 const std::string &class_path,
38 const std::string &
main)
48 const std::string &java_class_name,
49 const std::string &class_path,
50 const std::string &
main)
58 const std::string &java_class_name,
59 const std::string &class_path,
60 const std::string &
main,
61 std::unique_ptr<languaget> &&java_lang,
88 const std::string &java_class_name,
89 const std::string &class_path,
90 const std::string &
main,
91 std::unique_ptr<languaget> &&java_lang,
97 std::string filename=java_class_name +
".class";
103 [](
const irep_idt &) {
return false; },
119 std::istringstream java_code_stream(
"ignored");
127 language.
parse(java_code_stream, filename);
128 language.
typecheck(lazy_goto_model.symbol_table,
"");
130 language.
final(lazy_goto_model.symbol_table);
132 lazy_goto_model.load_all_functions();
134 std::unique_ptr<goto_modelt> maybe_goto_model=
136 std::move(lazy_goto_model));
137 INVARIANT(maybe_goto_model,
"Freezing lazy_goto_model failed");
140 const std::string class_symbol_name=
"java::"+java_class_name;
144 REQUIRE(class_symbol.is_type);
145 const typet &class_type=class_symbol.type;
146 REQUIRE(class_type.
id()==ID_struct);
152 INFO(
"Working directory: " << path);
158 return std::move(*maybe_goto_model);
165 const std::string &java_class_name,
166 const std::string &class_path,
167 const std::string &
main,
168 std::unique_ptr<languaget> &&java_lang)
171 command_line.
add_flag(
"no-lazy-methods");
172 command_line.
add_flag(
"no-refine-strings");
177 command_line.
set(
"java-cp-include-files", class_path);
179 java_class_name, class_path,
main, std::move(java_lang), command_line);
186 const std::string &java_class_name,
187 const std::string &class_path,
188 const std::string &
main)
191 command_line.
add_flag(
"no-lazy-methods");
192 command_line.
add_flag(
"no-refine-strings");
197 java_class_name, class_path,
main, std::move(lang), command_line);
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
struct configt::javat java
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
The type of an expression, extends irept.
symbol_tablet load_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main)
Returns the symbol table from load_goto_model_from_java_class(const std::string &java_class_name,...
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...
std::unique_ptr< languaget > new_java_bytecode_language()
goto_modelt load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main, std::unique_ptr< languaget > &&java_lang, const cmdlinet &command_line)
Go through the process of loading, type-checking and finalising a specific class file to build a goto...
virtual bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
bool has_suffix(const std::string &s, const std::string &suffix)
virtual void set_language_options(const optionst &)
Set language-specific options.
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
A GOTO model that produces function bodies on demand.
The symbol table base class interface.
virtual bool parse(std::istream &instream, const std::string &path)=0
virtual void set_message_handler(message_handlert &_message_handler)
const irep_idt & id() const
A goto function, consisting of function type (see type), function body (see body),...
std::unique_ptr< languaget > language
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...
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::string get_current_working_directory()
Abstract interface to eager or lazy GOTO models.
const java_class_typet & to_java_class_type(const typet &type)
null_message_handlert null_message_handler
symbol_tablet symbol_table
Symbol table.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.