diff --git a/regression/jbmc-strings/literal-length/Test.class b/regression/jbmc-strings/literal-length/Test.class new file mode 100644 index 00000000000..c05034ce3ea Binary files /dev/null and b/regression/jbmc-strings/literal-length/Test.class differ diff --git a/regression/jbmc-strings/literal-length/Test.java b/regression/jbmc-strings/literal-length/Test.java new file mode 100644 index 00000000000..14edc379387 --- /dev/null +++ b/regression/jbmc-strings/literal-length/Test.java @@ -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(); + } +} diff --git a/regression/jbmc-strings/literal-length/test.desc b/regression/jbmc-strings/literal-length/test.desc new file mode 100644 index 00000000000..c9e7816e08c --- /dev/null +++ b/regression/jbmc-strings/literal-length/test.desc @@ -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$ diff --git a/src/java_bytecode/java_string_literals.cpp b/src/java_bytecode/java_string_literals.cpp index 5ec35ac0d6e..ca6832b4f2c 100644 --- a/src/java_bytecode/java_string_literals.cpp +++ b/src/java_bytecode/java_string_literals.cpp @@ -106,6 +106,9 @@ 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"); @@ -113,7 +116,7 @@ symbol_exprt get_or_create_string_literal_symbol( 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))