Merge pull request #2813 from diffblue/java-char-literals-are-char

no need for cast for Java char literals

Author: Daniel Kroening

jbmc/src/java_bytecode/expr2java.cpp

@@ -201,7 +201,9 @@ std::string expr2javat::convert_constant(
     if(to_integer(src, int_value))
       UNREACHABLE;
 
-    dest += "(char)'" + utf16_native_endian_to_java(int_value.to_long()) + '\'';
+    // Character literals in Java have type 'char', thus no cast is needed.
+    // This is different from C, where charater literals have type 'int'.
+    dest += '\'' + utf16_native_endian_to_java(int_value.to_long()) + '\'';
     return dest;
   }
   else if(src.type()==java_byte_type())