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

Change utf16_native_endian_to_java to consume char16_t 

Java chars are fixed to be 16 bits by the standard.
This commit is contained in:
Michael Tautschnig 2018-11-05 16:00:09 +00:00
parent 52bc0a8563
commit c2380e8f6e
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/util/unicode.cpp
View File

@ -295,7 +295,7 @@ static void utf16_native_endian_to_java(
/// \param ch: UTF-16 character in architecture-native endianness encoding
/// \return String in US-ASCII format, with \\uxxxx escapes for other characters
std::string utf16_native_endian_to_java(const wchar_t ch)
std::string utf16_native_endian_to_java(const char16_t ch)
{
std::ostringstream result;
const std::locale loc;

2
src/util/unicode.h
View File

@ -26,7 +26,7 @@ std::string
utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s);
std::wstring utf8_to_utf16_native_endian(const std::string &in);
std::string utf16_native_endian_to_java(const wchar_t ch);
std::string utf16_native_endian_to_java(const char16_t ch);
std::string utf16_native_endian_to_java(const std::wstring &in);
std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);