replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

no need for cast for Java char literals

This commit is contained in:
Daniel Kroening 2018-08-22 11:32:56 +01:00
parent 78d22fb05c
commit ed7dc1d7a3
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
jbmc/src/java_bytecode/expr2java.cpp
View File

@ -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())