remove symbol_typet() constructor, which produces an incomplete object

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1185,7 +1185,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       if(cur_pc==it->handler_pc)
       {
-        if(catch_type!=typet() || it->catch_type==symbol_typet())
+        if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
         {
           catch_type=symbol_typet("java::java.lang.Throwable");
           break;

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -105,6 +105,11 @@ class java_bytecode_parse_treet
     struct exceptiont
     {
     public:
+      exceptiont()
+        : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
+      {
+      }
+
       std::size_t start_pc;
       std::size_t end_pc;
       std::size_t handler_pc;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1249,7 +1249,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  symbol_typet object_type;
+  optionalt<symbol_typet> object_type;
+
   typet value_type;
   if(type_name==ID_boolean)
   {
@@ -1296,6 +1297,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   else
     UNREACHABLE;
 
+  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
+
   // declare tmp_type_name to hold the value
   std::string aux_name="tmp_"+id2string(type_name);
   symbolt symbol=get_fresh_aux_symbol(
@@ -1304,7 +1307,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
 
   // Check that the type of the object is in the symbol table,
   // otherwise there is no safe way of finding its value.
-  if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier()))
+  if(
+    const auto maybe_symbol =
+      symbol_table.lookup(object_type->get_identifier()))
   {
     struct_typet struct_type=to_struct_type(maybe_symbol->type);
     // Check that the type has a value field
@@ -1321,7 +1326,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
     }
   }
 
-  warning() << object_type.get_identifier()
+  warning() << object_type->get_identifier()
             << " not available to format function" << eom;
   code.add(code_declt(value), loc);
   return value;

jbmc/unit/java_bytecode/java_types/generic_type_index.cpp

@@ -17,9 +17,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
     const auto symbol_type = symbol_typet("java::GenericClass");
     const auto generic_symbol_type = java_generic_symbol_typet(
       symbol_type, "LGenericClass<TX;Tvalue;>;", "PrefixClassName");
-    java_generic_parametert paramX("PrefixClassName::X", symbol_typet());
-    java_generic_parametert value("PrefixClassName::value", symbol_typet());
-    java_generic_parametert paramZ("PrefixClassName::Z", symbol_typet());
+    java_generic_parametert paramX(
+      "PrefixClassName::X", symbol_typet(irep_idt()));
+    java_generic_parametert value(
+      "PrefixClassName::value", symbol_typet(irep_idt()));
+    java_generic_parametert paramZ(
+      "PrefixClassName::Z", symbol_typet(irep_idt()));
 
     WHEN("Looking for parameter indexes")
     {
@@ -43,9 +46,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
     const auto symbol_type = symbol_typet("java::java.util.Map");
     const auto generic_symbol_type = java_generic_symbol_typet(
       symbol_type, "Ljava/util/Map<TK;TV;>;", "java.util.HashMap");
-    java_generic_parametert param0("java.util.HashMap::K", symbol_typet());
-    java_generic_parametert param1("java.util.HashMap::V", symbol_typet());
-    java_generic_parametert param2("java.util.HashMap::T", symbol_typet());
+    java_generic_parametert param0(
+      "java.util.HashMap::K", symbol_typet(irep_idt()));
+    java_generic_parametert param1(
+      "java.util.HashMap::V", symbol_typet(irep_idt()));
+    java_generic_parametert param2(
+      "java.util.HashMap::T", symbol_typet(irep_idt()));
 
     WHEN("Looking for parameter indexes")
     {

src/ansi-c/c_typecheck_type.cpp

@@ -792,9 +792,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     }
   }
 
-  symbol_typet symbol_type;
+  symbol_typet symbol_type(identifier);
   symbol_type.add_source_location()=type.source_location();
-  symbol_type.set_identifier(identifier);
 
   c_qualifierst original_qualifiers(type);
   type.swap(symbol_type);

src/goto-programs/remove_virtual_functions.cpp

@@ -177,7 +177,7 @@ void remove_virtual_functionst::remove_virtual_function(
   // So long as `this` is already not `void*` typed, the second parameter
   // is ignored:
   exprt this_class_identifier =
-    get_class_identifier_field(this_expr, symbol_typet(), ns);
+    get_class_identifier_field(this_expr, symbol_typet(irep_idt()), ns);
 
   // If instructed, add an ASSUME(FALSE) to handle the case where we don't
   // match any expected type:

src/util/std_types.h

@@ -110,10 +110,6 @@ class real_typet:public typet
 class symbol_typet:public typet
 {
 public:
-  symbol_typet():typet(ID_symbol)
-  {
-  }
-
   explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
   {
     set_identifier(identifier);