Rename utf16_constant_array_to_ascii to utf16_constant_array_to_java

Author: Lukasz A.J. Wrona

src/solvers/refinement/string_constraint_generator.h

@@ -375,7 +375,7 @@ exprt get_numeric_value_from_character(
   unsigned long radix=36ul);
 size_t max_printed_string_length(const typet &type, unsigned long radix);
 unsigned long to_integer_or_default(const exprt &expr, unsigned long def);
-std::string utf16_constant_array_to_ascii(
+std::string utf16_constant_array_to_java(
   const array_exprt &arr, unsigned length);
 
 #endif

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -386,7 +386,7 @@ string_exprt string_constraint_generatort::add_axioms_for_format(
 /// \param length: an unsigned value representing the length of the array
 /// \return String of length `length` represented by the array assuming each
 ///   field in `arr` represents a character.
-std::string utf16_constant_array_to_ascii(
+std::string utf16_constant_array_to_java(
   const array_exprt &arr, unsigned int length)
 {
   std::wstring out(length, '?');
@@ -399,7 +399,7 @@ std::string utf16_constant_array_to_ascii(
     INVARIANT(!conversion_failed, "constant should be convertible to unsigned");
     out[i]=c;
   }
-  return utf16_little_endian_to_ascii(out);
+  return utf16_little_endian_to_java(out);
 }
 
 /// Add axioms to specify the Java String.format function.
@@ -423,7 +423,7 @@ string_exprt string_constraint_generatort::add_axioms_for_format(
      s1.content().id()==ID_array &&
      !to_unsigned_integer(to_constant_expr(s1.length()), length))
   {
-    std::string s=utf16_constant_array_to_ascii(
+    std::string s=utf16_constant_array_to_java(
       to_array_expr(s1.content()), length);
     // List of arguments after s
     std::vector<exprt> args(

src/solvers/refinement/string_refinement.cpp

@@ -799,7 +799,7 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
   exprt size_expr=to_array_type(arr.type()).size();
   PRECONDITION(size_expr.id()==ID_constant);
   to_unsigned_integer(to_constant_expr(size_expr), n);
-  return utf16_constant_array_to_ascii(arr, n);
+  return utf16_constant_array_to_java(arr, n);
 }
 
 /// Display part of the current model by mapping the variables created by the

src/util/unicode.cpp

@@ -288,7 +288,7 @@ std::wstring utf8_to_utf16_little_endian(const std::string &in)
 
 /// \par parameters: String in UTF-16LE format
 /// \return String in US-ASCII format, with \uxxxx escapes for other characters
-std::string utf16_little_endian_to_ascii(const std::wstring &in)
+std::string utf16_little_endian_to_java(const std::wstring &in)
 {
   std::ostringstream result;
   const std::locale loc;

src/util/unicode.h

@@ -24,7 +24,7 @@ std::string utf32_to_utf8(const std::basic_string<unsigned int> &s);
 
 std::wstring utf8_to_utf16_big_endian(const std::string &);
 std::wstring utf8_to_utf16_little_endian(const std::string &);
-std::string utf16_little_endian_to_ascii(const std::wstring &in);
+std::string utf16_little_endian_to_java(const std::wstring &in);
 
 const char **narrow_argv(int argc, const wchar_t **argv_wide);