Merge pull request #2639 from thk123/array-element-type

Make array element type be not a comment

Author: Thomas Kiley

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -621,8 +621,8 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
     irep_idt name=src.get(ID_C_base_name);
     if(has_prefix(id2string(name), "array["))
     {
-      const typet &element_type=
-        static_cast<const typet &>(src.find(ID_C_element_type));
+      const typet &element_type =
+        static_cast<const typet &>(src.find(ID_element_type));
       get_class_refs_rec(element_type);
     }
     else

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1253,7 +1253,7 @@ void java_object_factoryt::allocate_nondet_length_array(
   side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
   java_new_array.copy_to_operands(length_sym_expr);
   java_new_array.set(ID_length_upper_bound, max_length_expr);
-  java_new_array.type().subtype().set(ID_C_element_type, element_type);
+  java_new_array.type().subtype().set(ID_element_type, element_type);
   code_assignt assign(lhs, java_new_array);
   assign.add_source_location()=loc;
   assignments.copy_to_operands(assign);
@@ -1277,8 +1277,8 @@ void java_object_factoryt::gen_nondet_array_init(
 
   const typet &type=ns.follow(expr.type().subtype());
   const struct_typet &struct_type=to_struct_type(type);
-  const typet &element_type=
-    static_cast<const typet &>(expr.type().subtype().find(ID_C_element_type));
+  const typet &element_type =
+    static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
 
   auto max_length_expr=from_integer(
     object_factory_parameters.max_nondet_array_length, java_int_type());

jbmc/src/java_bytecode/java_types.cpp

@@ -88,7 +88,7 @@ reference_typet java_lang_object_type()
 }
 
 /// Construct an array pointer type. It is a pointer to a symbol with identifier
-/// java::array[]. Its ID_C_element_type is set to the corresponding primitive
+/// java::array[]. Its ID_element_type is set to the corresponding primitive
 /// type, or void* for arrays of references.
 /// \param subtype Character indicating the type of array
 reference_typet java_array_type(const char subtype)
@@ -119,7 +119,7 @@ reference_typet java_array_type(const char subtype)
 
   symbol_typet symbol_type("java::"+id2string(class_name));
   symbol_type.set(ID_C_base_name, class_name);
-  symbol_type.set(ID_C_element_type, java_type_from_char(subtype));
+  symbol_type.set(ID_element_type, java_type_from_char(subtype));
 
   return java_reference_type(symbol_type);
 }
@@ -131,7 +131,7 @@ const typet &java_array_element_type(const symbol_typet &array_symbol)
   DATA_INVARIANT(
     is_java_array_tag(array_symbol.get_identifier()),
     "Symbol should have array tag");
-  return array_symbol.find_type(ID_C_element_type);
+  return array_symbol.find_type(ID_element_type);
 }
 
 /// Return a non-const reference to the element type of a given java array type
@@ -141,7 +141,7 @@ typet &java_array_element_type(symbol_typet &array_symbol)
   DATA_INVARIANT(
     is_java_array_tag(array_symbol.get_identifier()),
     "Symbol should have array tag");
-  return array_symbol.add_type(ID_C_element_type);
+  return array_symbol.add_type(ID_element_type);
 }
 
 /// Checks whether the given type is an array pointer type
@@ -555,7 +555,7 @@ typet java_type_from_string(
   case '[': // array type
     {
       // If this is a reference array, we generate a plain array[reference]
-      // with void* members, but note the real type in ID_C_element_type.
+      // with void* members, but note the real type in ID_element_type.
       if(src.size()<=1)
         return nil_typet();
       char subtype_letter=src[1];
@@ -567,7 +567,7 @@ typet java_type_from_string(
          subtype_letter=='T')   // Array of generic types
         subtype_letter='A';
       typet tmp=java_array_type(std::tolower(subtype_letter));
-      tmp.subtype().set(ID_C_element_type, subtype);
+      tmp.subtype().set(ID_element_type, subtype);
       return tmp;
     }
 

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -177,7 +177,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     struct_type.components()[2].type());
 
   // Allocate a (struct realtype**) instead of a (void**) if possible.
-  const irept &given_element_type = object_type.find(ID_C_element_type);
+  const irept &given_element_type = object_type.find(ID_element_type);
   typet allocate_data_type;
   if(given_element_type.is_not_nil())
   {
@@ -272,7 +272,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     // we already know that rhs has pointer type
     typet sub_type =
-      static_cast<const typet &>(rhs.type().subtype().find("#element_type"));
+      static_cast<const typet &>(rhs.type().subtype().find(ID_element_type));
     CHECK_RETURN(sub_type.id() == ID_pointer);
     sub_java_new.type() = sub_type;
 

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -122,7 +122,7 @@ pointer_typet select_pointer_typet::specialize_generics(
           visited_nodes);
 
         pointer_typet replacement_array_type = java_array_type('a');
-        replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
+        replacement_array_type.subtype().set(ID_element_type, new_array_type);
         return replacement_array_type;
       }
     }

jbmc/unit/java-testing-utils/require_type.cpp

@@ -10,6 +10,8 @@
 
 #include <testing-utils/catch.hpp>
 #include <util/base_type.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
 
 /// Checks a type is a pointer type optionally with a specific subtype
 /// \param type: The type to check
@@ -25,8 +27,8 @@ pointer_typet require_type::require_pointer(
 
   if(subtype)
   {
-    // TODO: use base_type_eq
-    REQUIRE(pointer.subtype() == subtype.value());
+    namespacet ns{symbol_tablet{}};
+    base_type_eq(pointer.subtype(), subtype.value(), ns);
   }
   return pointer;
 }

src/util/irep_ids.def

@@ -571,7 +571,7 @@ IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
 IREP_ID_TWO(C_spec_requires, #spec_requires)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
 IREP_ID_ONE(virtual_function)
-IREP_ID_TWO(C_element_type, #element_type)
+IREP_ID_TWO(element_type, element_type)
 IREP_ID_ONE(working_directory)
 IREP_ID_ONE(section)
 IREP_ID_ONE(bswap)