Add a test for the string solver

This is an example for which a branch with changes to
symex (field-sensitivity) caused failure in the string solver because a
nil expression got into the model.

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringConcat/Test.class

@@ -312,4 +312,15 @@ public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data
         assert(false);
         return sb.toString();
     }
+
+    static boolean fromNonDetArray(String[] argv)
+    {
+        String s = argv[0];
+        String u = s.concat("llo");
+        if(u.equals("Hello")) {
+            return true;
+        }
+        return false;
+    }
+
 }

jbmc/regression/jbmc-strings/StringConcat/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.fromNonDetArray --depth 10000 --unwind 5 --throw-runtime-exceptions  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+line 318 no uncaught exception: FAILURE
+java.lang.ArrayIndexOutOfBoundsException|java.lang.NullPointerException