Add tests for String.format

This tests the new implementation of String.format using the java models.

Author: romainbrenguier

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

@@ -0,0 +1,59 @@
+public class Test
+{
+    public static String testHex(int i)
+    {
+	String u=String.format("di%xlue", i);
+	if(u.equals("diffblue"))
+            assert(false);
+	else if(u.startsWith("di"))
+            assert(false);
+        else
+            assert(false);
+        return u;
+    }
+    
+    public static String testInt(int i)
+    {
+	String u=String.format("Hello %d !", i);
+	if(u.equals("Hello 10 !"))
+            assert(false);
+	else if (!u.startsWith("Hello"))
+            assert(false);
+        else
+            assert(false);
+        return u;
+    }
+
+    public static String string1(String s)
+    {
+        if(s == null)
+            return "null!";
+        String u=String.format("Hello %s !", s);
+        if(u.equals("Hello world !"))
+            assert(false);
+        else if(u.startsWith("impossible!"))
+            assert(false);
+        else
+            assert(false);
+        return u;
+    }
+
+    public static String string2(String s, String t)
+    {
+        if(s == null || t == null)
+            return "null null";
+        String u=String.format("%s %s", s, t);
+        assert(!u.equals("ab"));
+        return u;
+    }
+
+    public static String string3(String s, String t)
+    {
+        if(s == null || t == null)
+            return "null null";
+        String u=String.format("%s%s%s", s, t, s);
+        assert(s.length() != 1 || u.charAt(0) == u.charAt(u.length() - 1));
+        return u;
+    }
+
+}

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

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+line 7 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-hex1.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+line 9 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-hex2.desc

@@ -0,0 +1,6 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+line 11 assertion at file Test.java .*: SUCCESS

jbmc/regression/jbmc-strings/StringFormat/test-hex3.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+line 19 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-int1.desc

@@ -0,0 +1,6 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.2"
+^EXIT=0$
+^SIGNAL=0$
+line 21 assertion at file Test.java .*: SUCCESS

jbmc/regression/jbmc-strings/StringFormat/test-int2.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.3"
+^EXIT=10$
+^SIGNAL=0$
+line 23 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-int3.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.string1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+line 33 assertion at file Test.java .*: FAILURE
+line 35 assertion at file Test.java .*: SUCCESS
+line 37 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-string1.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.string2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 20 --property "java::Test.string2:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1"
+^EXIT=0$
+^SIGNAL=0$
+line 46 assertion at file Test.java .*: SUCCESS
+
+