Test with array of strings

This checks that jbmc correctly analyze functions that take arrays of
strings as inputs.
With the changes assigning strings directly at malloc site, this example
can be analyzed by jbmc approximately 15 times faster.

Author: romainbrenguier

regression/jbmc-strings/StringArray/Test.class

@@ -0,0 +1,26 @@
+public class Test {
+
+    public static String check(String[] array) {
+	// Filter
+	if(array == null)
+	    return "null array";
+	if(array.length < 2)
+	    return "too short";
+	if(array[0] == null)
+	    return "null string";
+
+	// Arrange
+        String s0 = array[0];
+        String s1 = array[1];
+
+	// Act
+	boolean b = s0.equals(s1);
+	
+	// Assert
+	assert(s0 != null);
+	assert(!b);
+	
+	// Return
+	return s0 + s1;
+    }
+}

regression/jbmc-strings/StringArray/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --function Test.check --string-max-input-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion\.1\].* line 20.* SUCCESS$
+^\[.*assertion\.2\].* line 21.* FAILURE$
+--