type symbols now use ID_symbol_type

Author: kroening

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -628,7 +628,7 @@ void ci_lazy_methodst::gather_field_types(
   {
     // If class_type is not a symbol this may be a reference array,
     // but we can't tell what type.
-    if(class_type.id() == ID_symbol)
+    if(class_type.id() == ID_symbol_type)
     {
       const typet &element_type =
         java_array_element_type(to_symbol_type(class_type));
@@ -644,11 +644,11 @@ void ci_lazy_methodst::gather_field_types(
   {
     for(const auto &field : underlying_type.components())
     {
-      if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
+      if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
         gather_field_types(field.type(), ns, needed_lazy_methods);
       else if(field.type().id() == ID_pointer)
       {
-        if(field.type().subtype().id() == ID_symbol)
+        if(field.type().subtype().id() == ID_symbol_type)
         {
           initialize_all_instantiated_classes_from_pointer(
             to_pointer_type(field.type()), ns, needed_lazy_methods);

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1610,7 +1610,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const typecast_exprt pointer(op[0], java_array_type(statement[0]));
 
       dereference_exprt array(pointer, pointer.type().subtype());
-      assert(pointer.type().subtype().id()==ID_symbol);
+      assert(pointer.type().subtype().id()==ID_symbol_type);
       array.set(ID_java_member_access, true);
 
       const member_exprt length(array, "length", java_int_type());
@@ -2553,7 +2553,7 @@ codet java_bytecode_convert_methodt::convert_putstatic(
   const exprt::operandst &op,
   const symbol_exprt &symbol_expr)
 {
-  if(needed_lazy_methods && arg0.type().id() == ID_symbol)
+  if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
   {
     needed_lazy_methods->add_needed_class(
       to_symbol_type(arg0.type()).get_identifier());
@@ -2603,15 +2603,15 @@ void java_bytecode_convert_methodt::convert_getstatic(
 {
   if(needed_lazy_methods)
   {
-    if(arg0.type().id() == ID_symbol)
+    if(arg0.type().id() == ID_symbol_type)
     {
       needed_lazy_methods->add_needed_class(
         to_symbol_type(arg0.type()).get_identifier());
     }
     else if(arg0.type().id() == ID_pointer)
     {
       const auto &pointer_type = to_pointer_type(arg0.type());
-      if(pointer_type.subtype().id() == ID_symbol)
+      if(pointer_type.subtype().id() == ID_symbol_type)
       {
         needed_lazy_methods->add_needed_class(
           to_symbol_type(pointer_type.subtype()).get_identifier());

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -117,7 +117,7 @@ java_bytecode_parse_treet::find_annotation(
       if(annotation.type.id() != ID_pointer)
         return false;
       const typet &type = annotation.type.subtype();
-      return type.id() == ID_symbol &&
+      return type.id() == ID_symbol_type &&
              to_symbol_type(type).get_identifier() == annotation_type_name;
     });
   if(annotation_it == annotations.end())

jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 void java_bytecode_typecheckt::typecheck_type(typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
   {
     irep_idt identifier=to_symbol_type(type).get_identifier();
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1201,7 +1201,7 @@ void java_object_factoryt::gen_nondet_init(
     if(is_sub)
     {
       const typet &symbol = override_ ? override_type : expr.type();
-      PRECONDITION(symbol.id() == ID_symbol);
+      PRECONDITION(symbol.id() == ID_symbol_type);
       generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
         to_symbol_type(symbol), struct_type);
     }
@@ -1305,7 +1305,7 @@ void java_object_factoryt::gen_nondet_array_init(
   update_in_placet update_in_place)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
-  PRECONDITION(expr.type().subtype().id()==ID_symbol);
+  PRECONDITION(expr.type().subtype().id()==ID_symbol_type);
   PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
 
   const typet &type=ns.follow(expr.type().subtype());

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -36,7 +36,7 @@ Date:   April 2017
 irep_idt get_tag(const typet &type)
 {
   /// \todo Use follow instead of assuming tag to symbol relationship.
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
     return to_symbol_type(type).get_identifier();
   else if(type.id() == ID_struct)
     return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
@@ -393,11 +393,11 @@ java_string_library_preprocesst::process_equals_function_operands(
 /// \return type of the "data" component
 static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
 {
-  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
-  if(type.id()==ID_symbol)
+  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol_type);
+  if(type.id()==ID_symbol_type)
   {
     symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
-    CHECK_RETURN(sym.type.id()!=ID_symbol);
+    CHECK_RETURN(sym.type.id()!=ID_symbol_type);
     return get_data_type(sym.type, symbol_table);
   }
   // else type id is ID_struct
@@ -412,11 +412,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
 static typet
 get_length_type(const typet &type, const symbol_tablet &symbol_table)
 {
-  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
-  if(type.id()==ID_symbol)
+  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol_type);
+  if(type.id()==ID_symbol_type)
   {
     symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
-    CHECK_RETURN(sym.type.id()!=ID_symbol);
+    CHECK_RETURN(sym.type.id()!=ID_symbol_type);
     return get_length_type(sym.type, symbol_table);
   }
   // else type id is ID_struct
@@ -891,7 +891,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
 
   typet deref_type;
-  if(rhs.type().subtype().id()==ID_symbol)
+  if(rhs.type().subtype().id()==ID_symbol_type)
     deref_type=symbol_table.lookup_ref(
       to_symbol_type(rhs.type().subtype()).get_identifier()).type;
   else

jbmc/src/java_bytecode/java_types.cpp

@@ -735,7 +735,7 @@ bool equal_java_types(const typet &type1, const typet &type2)
   bool arrays_with_same_element_type = true;
   if(
     type1.id() == ID_pointer && type2.id() == ID_pointer &&
-    type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
+    type1.subtype().id() == ID_symbol_type && type2.subtype().id() == ID_symbol_type)
   {
     const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
     const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
@@ -782,7 +782,7 @@ void get_dependencies_from_generic_parameters_rec(
   }
 
   // symbol type
-  else if(t.id() == ID_symbol)
+  else if(t.id() == ID_symbol_type)
   {
     const symbol_typet &symbol_type = to_symbol_type(t);
     const irep_idt class_name(symbol_type.get_identifier());
@@ -916,7 +916,7 @@ std::string pretty_java_type(const typet &type)
     return "byte";
   else if(is_reference(type))
   {
-    if(type.subtype().id() == ID_symbol)
+    if(type.subtype().id() == ID_symbol_type)
     {
       const auto &symbol_type = to_symbol_type(type.subtype());
       const irep_idt &id = symbol_type.get_identifier();

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -80,7 +80,7 @@ std::size_t remove_instanceoft::lower_instanceof(
 
   // Find all types we know about that satisfy the given requirement:
   INVARIANT(
-    target_type.id()==ID_symbol,
+    target_type.id()==ID_symbol_type,
     "instanceof second operand should have a simple type");
   const irep_idt &target_name=
     to_symbol_type(target_type).get_identifier();

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -107,7 +107,7 @@ pointer_typet select_pointer_typet::specialize_generics(
     visited_nodes.erase(parameter_name);
     return returned_type;
   }
-  else if(pointer_type.subtype().id() == ID_symbol)
+  else if(pointer_type.subtype().id() == ID_symbol_type)
   {
     // if the pointer is an array, recursively specialize its element type
     const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());

src/analyses/invariant_propagation.cpp

@@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const
     return false;
   else if(type.id()==ID_array)
     return false;
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
     return check_type(ns.follow(type));
   else if(type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)