Add String.substring() and StringBuilder.substring() regression error tests

Add regression tests that check that the constant propagator does not simplify
substring() invocations with only constant arguments when the indices are out of
bounds.

Author: danpoe

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.class

@@ -0,0 +1,16 @@
+public class Main {
+  public void test1() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(-1);
+  }
+
+  public void test2() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(4);
+  }
+
+  public void test3() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(-1, 4);
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.java

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

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

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

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

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test3.desc

@@ -0,0 +1,16 @@
+public class Main {
+  public void test1() {
+    String s1 = "abc";
+    s1.substring(-1);
+  }
+
+  public void test2() {
+    String s1 = "abc";
+    s1.substring(4);
+  }
+
+  public void test3() {
+    String s1 = "abc";
+    s1.substring(-1, 4);
+  }
+}

jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.class

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.java

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--