Test comparing jbmc lastIndexOf with loop version

Author: romainbrenguier

regression/jbmc-strings/VerifStringLastIndexOf/Test.class

@@ -0,0 +1,28 @@
+public class Test {
+  // This compares the model of indexOf to an implementation
+  // using loops
+
+  public int math_min(int i, int j) {
+    if (i < j)
+      return i;
+    else
+      return j;
+  }
+
+  public int referenceLastIndexOf(String s, char ch, int fromIndex) {
+    int i = math_min(fromIndex, s.length() - 1);
+    for (; i >= 0; i--) {
+      if (s.charAt(i) == ch) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  public int check(String s, char ch, int fromIndex) {
+    int reference = referenceLastIndexOf(s, ch, fromIndex);
+    int jbmc_result = s.lastIndexOf(ch, fromIndex);
+    assert(reference == jbmc_result);
+    return jbmc_result;
+  }
+}

regression/jbmc-strings/VerifStringLastIndexOf/Test.java

@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--function Test.check --refine-strings --string-max-length 50 --unwind 50 --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 32 .* SUCCESS$
+assertion at file Test.java line 34 .* FAILURE$