35 size_t _max_array_length,
38 bool _string_refinement_enabled,
88 debug() <<
"Skip class " << c.
name <<
" (already loaded)" <<
eom;
95 class_type.
set(ID_base_name, c.
name);
98 ID_java_enum_static_unwind,
106 base_class_field.
type()=base;
110 class_type.
components().push_back(base_class_field);
124 new_symbol.
name=qualified_classname;
125 class_type.
set(ID_name, new_symbol.
name);
126 new_symbol.
type=class_type;
127 new_symbol.
mode=ID_java;
135 error() <<
"failed to add class symbol " << new_symbol.
name <<
eom;
140 for(
const auto &field : c.
fields)
144 for(
const auto &method : c.
methods)
149 ":"+method.signature;
171 lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
185 class_type.
set_tag(class_name);
186 class_type.
set(ID_base_name, class_name);
188 class_type.
set(ID_incomplete_class,
true);
195 class_type.
set(ID_name, new_symbol.
name);
196 new_symbol.
type=class_type;
197 new_symbol.
mode=ID_java;
204 warning() <<
"stub class symbol " << new_symbol.
name 205 <<
" already exists" <<
eom;
231 new_symbol.
type=field_type;
234 new_symbol.
mode=ID_java;
250 assert(
false &&
"failed to add static field symbol");
262 component.
type()=field_type;
277 const std::string letters=
"ijsbcfdza";
279 for(
const char l : letters)
291 comp0(
"@java.lang.Object",
symbol_typet(
"java::java.lang.Object"));
305 symbol.
type=struct_type;
314 size_t max_array_length,
317 bool string_refinement_enabled,
326 string_refinement_enabled,
327 character_preprocess);
344 catch(
const std::string &e)
357 string_type.
set_tag(
"java.lang.String");
359 string_type.
components()[0].set_name(
"@java.lang.Object");
360 string_type.
components()[0].set_pretty_name(
"@java.lang.Object");
362 string_type.
components()[1].set_name(
"length");
363 string_type.
components()[1].set_pretty_name(
"length");
366 string_type.
components()[2].set_pretty_name(
"data");
375 string_symbol.
name=
"java::java.lang.String";
376 string_symbol.
base_name=
"java.lang.String";
377 string_symbol.
type=string_type;
386 string_equals_symbol.
name=
387 "java::java.lang.String.equals:(Ljava/lang/Object;)Z";
388 string_equals_symbol.
base_name=
"java.lang.String.equals";
389 string_equals_symbol.
pretty_name=
"java.lang.String.equals";
390 string_equals_symbol.
mode=ID_java;
399 string_equals_type.
parameters().push_back(thisparam);
400 string_equals_type.
parameters().push_back(otherparam);
401 string_equals_symbol.
type=std::move(string_equals_type);
The type of an expression.
irep_idt name
The unique identifier.
void java_bytecode_convert_method_lazy(const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet...
Linking: Zero Initialization.
character_refine_preprocesst character_preprocess
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
java_bytecode_parse_treet::fieldt fieldt
void java_root_class(symbolt &class_symbol)
typet java_boolean_type()
irep_idt mode
Language mode.
java_bytecode_parse_treet::classt classt
java_bytecode_convert_classt(symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, lazy_methodst &_lazy_methods, lazy_methods_modet _lazy_methods_mode, bool _string_refinement_enabled, const character_refine_preprocesst &_character_preprocess)
reference_typet java_reference_type(const typet &subtype)
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
exprt value
Initial value of symbol.
const componentst & components() const
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
reference_typet java_array_type(const char subtype)
bool java_bytecode_convert_class(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, bool string_refinement_enabled, const character_refine_preprocesst &character_preprocess)
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
An expression denoting infinity.
typet java_type_from_string(const std::string &src)
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
A reference into the symbol table.
void add_string_type()
Implements the java.lang.String type in the case that we provide an internal implementation.
JAVA Bytecode Language Conversion.
void set_access(const irep_idt &access)
typet java_type_from_char(char t)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void set_tag(const irep_idt &tag)
void operator()(const java_bytecode_parse_treet &parse_tree)
const size_t max_array_length
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
std::map< irep_idt, lazy_method_valuet > lazy_methodst
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
lazy_methodst & lazy_methods
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
bool string_refinement_enabled
message_handlert & get_message_handler()
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
void set_pretty_name(const irep_idt &name)
void convert(const classt &c)
symbol_tablet & symbol_table
bool has_symbol(const irep_idt &name) const
JAVA Bytecode Language Conversion.
lazy_methods_modet lazy_methods_mode
const typet & return_type() const
const irep_idt & get_identifier() const
void generate_class_stub(const irep_idt &class_name)
void add_base(const typet &base)
void set(const irep_namet &name, const irep_idt &value)
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.