use java_reference_typet

Auxiliary methods now return java_reference_typet; this is strictly stronger
than reference_typet.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_types.cpp

@@ -86,12 +86,13 @@ c_bool_typet java_boolean_type()
   return result;
 }
 
-reference_typet java_reference_type(const typet &subtype)
+java_reference_typet java_reference_type(const typet &subtype)
 {
-  return reference_type(subtype);
+  PRECONDITION(subtype.id() == ID_struct_tag);
+  return to_java_reference_type(reference_type(subtype));
 }
 
-reference_typet java_lang_object_type()
+java_reference_typet java_lang_object_type()
 {
   static const auto result =
     java_reference_type(struct_tag_typet("java::java.lang.Object"));
@@ -102,7 +103,7 @@ reference_typet java_lang_object_type()
 /// 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)
+java_reference_typet java_array_type(const char subtype)
 {
   std::string subtype_str;
 

jbmc/src/java_bytecode/java_types.h

@@ -411,11 +411,11 @@ floatbv_typet java_float_type();
 floatbv_typet java_double_type();
 c_bool_typet java_boolean_type();
 empty_typet java_void_type();
-reference_typet java_reference_type(const typet &subtype);
-reference_typet java_lang_object_type();
+java_reference_typet java_reference_type(const typet &subtype);
+java_reference_typet java_lang_object_type();
 struct_tag_typet java_classname(const std::string &);
 
-reference_typet java_array_type(const char subtype);
+java_reference_typet java_array_type(const char subtype);
 const typet &java_array_element_type(const struct_tag_typet &array_symbol);
 typet &java_array_element_type(struct_tag_typet &array_symbol);
 bool is_java_array_type(const typet &type);