Test for String.lastIndexOf with empty argument

Author: romainbrenguier

regression/jbmc-strings/StringLastIndexOf/Test.class

@@ -0,0 +1,24 @@
+public class Test {
+    int fromIndex;
+
+    public void check(String input_String1, String input_String2, int i) {
+        if(input_String1 != null && input_String2 != null) {
+            if (i == 0) {
+                // The last occurrence of the empty string "" is considered to
+                // occur at the index value this.length()
+                int lio = input_String1.lastIndexOf(input_String2);
+                if (input_String2.length() == 0)
+                    assert lio == input_String1.length();
+            } else if (i == 1) {
+                // Contradiction with the previous condition (should fail).
+                assert "foo".lastIndexOf("") != 3;
+            } else if (i == 2 && input_String2.length() > 0) {
+                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                if (input_String2.length() == 0)
+                    assert lio == fromIndex;
+            } else if (i == 3) {
+                assert "foo".lastIndexOf("", 2) != 2;
+            }
+        }
+    }
+}

regression/jbmc-strings/StringLastIndexOf/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check --refine-strings --string-max-length 100
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 11 .* SUCCESS$
+assertion at file Test.java line 14 .* FAILURE$
+assertion at file Test.java line 18 .* SUCCESS$
+assertion at file Test.java line 20 .* FAILURE$