Skip to content

Fix to java_bytecode_convert_classt.add_array_types #1401

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 26, 2017
Merged

Fix to java_bytecode_convert_classt.add_array_types #1401

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 8 additions & 18 deletions src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,11 +75,6 @@ class java_bytecode_convert_classt:public messaget
lazy_methods_modet lazy_methods_mode;
java_string_library_preprocesst &string_preprocess;

/// This field will be initialized to false, and set to true when
/// add_array_types() is executed. It serves as a sentinel to make sure that
/// the code using this class calls add_array_types() at least once.
static bool add_array_types_executed;

// conversion
void convert(const classt &c);
void convert(symbolt &class_symbol, const fieldt &f);
Expand All @@ -88,9 +83,6 @@ class java_bytecode_convert_classt:public messaget
static void add_array_types(symbol_tablet &symbol_table);
};

// initialization of static field
bool java_bytecode_convert_classt::add_array_types_executed=false;

void java_bytecode_convert_classt::convert(const classt &c)
{
std::string qualified_classname="java::"+id2string(c.name);
Expand Down Expand Up @@ -256,23 +248,21 @@ void java_bytecode_convert_classt::convert(
/// java::array[X] where X is byte, float, int, char...
void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
{
// this method only adds stuff to the symbol table, no need to execute it more
// than once
if(add_array_types_executed)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this condition is no longer required as we check symbols are new?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, there is now check if symbol is in symbol table.

return;
add_array_types_executed=true;

const std::string letters="ijsbcfdza";

for(const char l : letters)
{
symbol_typet symbol_type=
to_symbol_type(java_array_type(l).subtype());

const irep_idt &symbol_type_identifier=symbol_type.get_identifier();
if(symbol_table.has_symbol(symbol_type_identifier))
return;

struct_typet struct_type;
// we have the base class, java.lang.Object, length and data
// of appropriate type
struct_type.set_tag(symbol_type.get_identifier());
struct_type.set_tag(symbol_type_identifier);

struct_type.components().reserve(3);
struct_typet::componentt
Expand All @@ -298,7 +288,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
"object that doesn't match expectations");

symbolt symbol;
symbol.name=symbol_type.get_identifier();
symbol.name=symbol_type_identifier;
symbol.base_name=symbol_type.get(ID_C_base_name);
symbol.is_type=true;
symbol.type=struct_type;
Expand All @@ -308,7 +298,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
// ----------------------------

const irep_idt clone_name=
id2string(symbol_type.get_identifier())+".clone:()Ljava/lang/Object;";
id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
code_typet clone_type;
clone_type.return_type()=
java_reference_type(symbol_typet("java::java.lang.Object"));
Expand Down Expand Up @@ -413,7 +403,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
symbolt clone_symbol;
clone_symbol.name=clone_name;
clone_symbol.pretty_name=
id2string(symbol_type.get_identifier())+".clone:()";
id2string(symbol_type_identifier)+".clone:()";
clone_symbol.base_name="clone";
clone_symbol.type=clone_type;
clone_symbol.value=clone_body;
Expand Down