From b9dfda9f9e9a0fb0faa8664aad7099f4923d0242 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Mon, 18 Sep 2017 15:56:07 +0100 Subject: [PATCH] Fix to java_bytecode_convert_classt.add_array_types Fix to the problem with multiple execution of java_bytecode_convert_classt::add_array_types(symbol_tablet &) It replaces static member variable with check of the symbol table. --- .../java_bytecode_convert_class.cpp | 26 ++++++------------- 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 71d742c247f..0942b52fbf7 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -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); @@ -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); @@ -256,12 +248,6 @@ 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) - return; - add_array_types_executed=true; - const std::string letters="ijsbcfdza"; for(const char l : letters) @@ -269,10 +255,14 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) 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 @@ -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; @@ -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")); @@ -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;