From ed7dc1d7a315d82c44b94ed858e4e71b03b48ff5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 22 Aug 2018 11:32:56 +0100 Subject: [PATCH] no need for cast for Java char literals --- jbmc/src/java_bytecode/expr2java.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index edd196ff53a..f042e15ff2a 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/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())