Merge branch 'develop' of github.com:diffblue/cbmc into develop

regression/jbmc-strings/char_escape/Test.java

@@ -0,0 +1,19 @@
+public class Test {
+
+    public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6, char c7, char c8) {
+        StringBuilder sb = new StringBuilder("");
+        sb.append(c1);
+        sb.append(c2);
+        sb.append(c3);
+        sb.append(c4);
+        sb.append(c5);
+        sb.append(c6);
+        sb.append(c7);
+        sb.append(c8);
+        if (sb.toString().equals("\b\t\n\f\r\"\'\\"))
+            return true;
+        if (!sb.toString().equals("\b\t\n\f\r\"\'\\"))
+            return false;
+        return true;
+    }
+}

regression/jbmc-strings/char_escape/test.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --function Test.test --cover location --trace --json-ui
+^EXIT=0$
+^SIGNAL=0$
+20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)

src/java_bytecode/java_string_library_preprocess.cpp

@@ -902,10 +902,11 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   // Although we should not reach this code if rhs is null, the association
   // `pointer -> length` is added to the solver anyway, so we have to make sure
   // the length is set to something reasonable.
-  const auto rhs_length = if_exprt(
+  auto rhs_length = if_exprt(
     equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))),
     from_integer(0, lhs.length().type()),
     get_length(deref, symbol_table));
+  rhs_length.set(ID_mode, ID_java);
 
   // Assignments
   code.add(code_assignt(lhs.length(), rhs_length), loc);

src/pointer-analysis/value_set_dereference.cpp

@@ -153,6 +153,7 @@ exprt value_set_dereferencet::dereference(
       symbol.name="symex::invalid_object"+std::to_string(invalid_counter++);
       symbol.base_name="invalid_object";
       symbol.type=type;
+      symbol.mode = language_mode;
 
       // make it a lvalue, so we can assign to it
       symbol.is_lvalue=true;