Overwrite String type

String classes that are present in a loaded model will generate a type
that may be different from the internal type constructed for Java
strings in cbmc. Thus we now create a String type and write it in the
table, possibly overwriting a pre-existing Java string type.

Author: Joel Allred

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -45,13 +45,14 @@ class java_bytecode_convert_classt:public messaget
   {
     add_array_types();
 
-    if(parse_tree.loading_successful)
+    bool loading_success=parse_tree.loading_successful;
+    if(loading_success)
       convert(parse_tree.parsed_class);
-    else if(string_preprocess.is_known_string_type(
-              parse_tree.parsed_class.name))
+
+    if(string_preprocess.is_known_string_type(parse_tree.parsed_class.name))
       string_preprocess.add_string_type(
         parse_tree.parsed_class.name, symbol_table);
-    else
+    else if(!loading_success)
       generate_class_stub(parse_tree.parsed_class.name);
   }
 

src/java_bytecode/java_string_library_preprocess.cpp

@@ -319,7 +319,10 @@ void java_string_library_preprocesst::add_string_type(
   string_symbol.type=string_type;
   string_symbol.is_type=true;
 
-  symbol_table.add(string_symbol);
+  // Overwrite any pre-existing symbol in the table, e.g. created by
+  // a loaded model.
+  symbol_table.remove(string_symbol.name);
+  assert(!symbol_table.add(string_symbol));
 }
 
 /*******************************************************************\