Merge pull request diffblue#1975 from romainbrenguier/bugfix/literal-length-TG2878

[TG-2878] Fix bug in literal lengths

Author: romainbrenguier

regression/jbmc-strings/literal-length/Test.class

@@ -0,0 +1,12 @@
+public class Test {
+    public static int check(int i) {
+        String s = "\u0000";
+
+        if (i == 0)
+            assert(s.length() == 1);
+        else if (i == 1)
+            assert(s.length() != 1);
+
+        return s.length();
+    }
+}

regression/jbmc-strings/literal-length/Test.java

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings  --function Test.check
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$

regression/jbmc-strings/literal-length/test.desc

@@ -106,14 +106,17 @@ symbol_exprt get_or_create_string_literal_symbol(
   // contents as well:
   if(string_refinement_enabled)
   {
+    const array_exprt data =
+      utf16_to_array(utf8_to_utf16_little_endian(id2string(value)));
+
     struct_exprt literal_init(new_symbol.type);
     literal_init.operands().resize(jls_struct.components().size());
     const std::size_t jlo_nb = jls_struct.component_number("@java.lang.Object");
     literal_init.operands()[jlo_nb] = jlo_init;
 
     const std::size_t length_nb = jls_struct.component_number("length");
     const typet &length_type = jls_struct.components()[length_nb].type();
-    const exprt length = from_integer(id2string(value).size(), length_type);
+    const exprt length = from_integer(data.operands().size(), length_type);
     literal_init.operands()[length_nb] = length;
 
     // Initialize the string with a constant utf-16 array:
@@ -127,8 +130,7 @@ symbol_exprt get_or_create_string_literal_symbol(
     // These are basically const global data:
     array_symbol.is_static_lifetime = true;
     array_symbol.is_state_var = true;
-    array_symbol.value =
-      utf16_to_array(utf8_to_utf16_little_endian(id2string(value)));
+    array_symbol.value = data;
     array_symbol.type = array_symbol.value.type();
 
     if(symbol_table.add(array_symbol))