Merge pull request #3704 from diffblue/java_types

strengthen return types of java_*_type() functions

Author: tautschnig

jbmc/src/java_bytecode/java_types.cpp

@@ -29,47 +29,47 @@ std::vector<typet> parse_list_types(
   const char opening_bracket,
   const char closing_bracket);
 
-typet java_int_type()
+signedbv_typet java_int_type()
 {
   return signedbv_typet(32);
 }
 
-typet java_void_type()
+void_typet java_void_type()
 {
   return void_typet();
 }
 
-typet java_long_type()
+signedbv_typet java_long_type()
 {
   return signedbv_typet(64);
 }
 
-typet java_short_type()
+signedbv_typet java_short_type()
 {
   return signedbv_typet(16);
 }
 
-typet java_byte_type()
+signedbv_typet java_byte_type()
 {
   return signedbv_typet(8);
 }
 
-typet java_char_type()
+unsignedbv_typet java_char_type()
 {
   return unsignedbv_typet(16);
 }
 
-typet java_float_type()
+floatbv_typet java_float_type()
 {
   return ieee_float_spect::single_precision().to_type();
 }
 
-typet java_double_type()
+floatbv_typet java_double_type()
 {
   return ieee_float_spect::double_precision().to_type();
 }
 
-typet java_boolean_type()
+c_bool_typet java_boolean_type()
 {
   // The Java standard doesn't really prescribe the width
   // of a boolean. However, JNI suggests that it's 8 bits.
@@ -638,23 +638,23 @@ char java_char_from_type(const typet &type)
   if(id==ID_signedbv)
   {
     const size_t width=to_signedbv_type(type).get_width();
-    if(to_signedbv_type(java_int_type()).get_width()==width)
+    if(java_int_type().get_width() == width)
       return 'i';
-    else if(to_signedbv_type(java_long_type()).get_width()==width)
+    else if(java_long_type().get_width() == width)
       return 'l';
-    else if(to_signedbv_type(java_short_type()).get_width()==width)
+    else if(java_short_type().get_width() == width)
       return 's';
-    else if(to_signedbv_type(java_byte_type()).get_width()==width)
+    else if(java_byte_type().get_width() == width)
       return 'b';
   }
   else if(id==ID_unsignedbv)
     return 'c';
   else if(id==ID_floatbv)
   {
     const size_t width(to_floatbv_type(type).get_width());
-    if(to_floatbv_type(java_float_type()).get_width()==width)
+    if(java_float_type().get_width() == width)
       return 'f';
-    else if(to_floatbv_type(java_double_type()).get_width()==width)
+    else if(java_double_type().get_width() == width)
       return 'd';
   }
   else if(id==ID_c_bool)

jbmc/src/java_bytecode/java_types.h

@@ -359,15 +359,15 @@ inline java_method_typet &to_java_method_type(typet &type)
   return static_cast<java_method_typet &>(type);
 }
 
-typet java_int_type();
-typet java_long_type();
-typet java_short_type();
-typet java_byte_type();
-typet java_char_type();
-typet java_float_type();
-typet java_double_type();
-typet java_boolean_type();
-typet java_void_type();
+signedbv_typet java_int_type();
+signedbv_typet java_long_type();
+signedbv_typet java_short_type();
+signedbv_typet java_byte_type();
+unsignedbv_typet java_char_type();
+floatbv_typet java_float_type();
+floatbv_typet java_double_type();
+c_bool_typet java_boolean_type();
+void_typet java_void_type();
 reference_typet java_reference_type(const typet &subtype);
 reference_typet java_lang_object_type();
 struct_tag_typet java_classname(const std::string &);