Merge pull request #4785 from diffblue/string-format-percent-and-newline

Tests for percent and newline format specifiers TG-7657

Author: Joel Allred

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

@@ -0,0 +1,38 @@
+public class Test {
+  public static String percent() {
+    String u = String.format("%s %% %s", "foo", "bar");
+    if (u.equals("foo % bar"))
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String percentLength() {
+    String u = String.format("%s %% %s", "foo", "bar");
+    if (u.length() == 9)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String newline() {
+    String u = String.format("%s %n %s", "foo", "bar");
+    if (u.equals("foo \n bar"))
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String newlineLength() {
+    String u = String.format("%s %% %s", "foo", "bar");
+    if (u.length() == 9)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+}

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

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc

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

jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc

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