Merge pull request #4862 from allredj/clean-up/enable-string-test

Clean up/enable StringBuilder.append tests

Author: Joel Allred

jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class

@@ -0,0 +1,16 @@
+public class test
+{
+    public static void nondet(String stringArg)
+    {
+        StringBuilder sb = new StringBuilder(stringArg);
+        sb.append("Z");
+        String s = sb.toString();
+        if (s.startsWith("fg")) {
+            assert false;
+        } else if (s.endsWith("Z")) {
+            assert false;
+        } else {
+            assert false;
+        }
+    }
+}

jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java

@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.1\] .* line 9 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.

jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.2\] .* line 11.* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.

jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+\[.*assertion\.3\] .* line 13.* SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.