jbmc-strings/VerifStringLastIndexOf: ensure index is within String

The reference implementation and the built-in function disagree in case
the index is out of bounds.

Author: tautschnig

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/Test.class

@@ -19,6 +19,8 @@ public int referenceLastIndexOf(String s, char ch, int fromIndex) {
   }
 
   public int check(String s, char ch, int fromIndex) {
+    if(s.length() <= fromIndex)
+      return -1;
     int reference = referenceLastIndexOf(s, ch, fromIndex);
     int jbmc_result = s.lastIndexOf(ch, fromIndex);
     assert(reference == jbmc_result);