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.

Author: janmroczkowski

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,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)
-    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
@@ -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;