Merge pull request #4477 from romainbrenguier/feature/cprover-string-format

Use CProverString.format as interface to the solver builtin function

Author: romainbrenguier

jbmc/lib/java-models-library

@@ -0,0 +1,52 @@
+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.class

@@ -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 5 assertion at file Test.java .*: FAILURE

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.2"
+^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 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 9 assertion at file Test.java .*: SUCCESS

jbmc/regression/jbmc-strings/StringFormat/test-hex2.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 16 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-hex3.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 18 assertion at file Test.java .*: SUCCESS

jbmc/regression/jbmc-strings/StringFormat/test-int1.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 20 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormat/test-int2.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 29 assertion at file Test.java .*: FAILURE
+line 31 assertion at file Test.java .*: SUCCESS
+line 33 assertion at file Test.java .*: FAILURE

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

@@ -0,0 +1,6 @@
+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 41 assertion at file Test.java .*: SUCCESS

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

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