Separate tests String.regionMatches

These are all skipped for now, as String.regionMatches() is not
implemented.

Author: Joel Allred

jbmc/regression/jbmc-strings/RegionMatches/RegionMatches.class

@@ -0,0 +1,19 @@
+public class RegionMatches
+{
+    public static void constant(int in)
+    {
+        String s3 = "Automatic Test Generation";
+        String s4 = "automatic test generation";
+        String s4 = "automatic test generationn";
+
+        // test regionMatches (case sensitive)
+        if (in == 0)
+            assert s3.regionMatches(0, s3, 0, 5); // should succeed
+        else if (in == 1)
+            assert !s3.regionMatches(0, s4, 0, 5); // should fail
+        else if (in == 2)
+            assert s3.regionMatches(true, 0, s4, 0, 5); // should succeed (ignore case)
+        else if (in == 3)
+            assert s3.regionMatches(true, 0, s5, 0, 5); // should fail (ignore case)
+    }
+}

jbmc/regression/jbmc-strings/RegionMatches/RegionMatches.java

@@ -0,0 +1,9 @@
+FUTURE
+RegionMatches.class
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.1"
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Fails because String.regionMatches is not implemented

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

@@ -0,0 +1,9 @@
+FUTURE
+RegionMatches.class
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Fails because String.regionMatches is not implemented

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

@@ -0,0 +1,9 @@
+FUTURE
+RegionMatches.class
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Fails because String.regionMatches is not implemented

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

@@ -0,0 +1,9 @@
+FUTURE
+RegionMatches.class
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.4"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Fails because String.regionMatches is not implemented

jbmc/regression/jbmc-strings/RegionMatches/test4.desc

@@ -31,17 +31,5 @@ public static void main(String[] args)
       assert s3.compareTo(s4)==-32; //true
 
       assert s4.compareTo(s3)==32; //true
-
-      // test regionMatches (case sensitive)
-      if (!s3.regionMatches(0, s4, 0, 5)) //true
-         assert true;
-      else
-         assert false;
-
-      // test regionMatches (ignore case)
-      if (s3.regionMatches(true, 0, s4, 0, 5)) //true
-         assert true;
-      else
-         assert false;
    }
 }