Correct tests for String.indexOf

These were using String.charAt which is no longer supported by CBMC and
we should use CProverString.charAt instead (the two differ in that
CProverString.charAt does not throw exceptions).

This problem was undecteted before because the constant "hello" was
interferring with the string-max-length value.
So this parameter is replaced by string-max-input-length which only
constrain inputs.

Author: romainbrenguier

regression/jbmc-strings/StringIndexOf/Test.class

@@ -1,3 +1,6 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+
 public class Test {
 
     public boolean check(String input_String, char input_char, int input_int) {
@@ -14,13 +17,13 @@ public boolean check(String input_String, char input_char, int input_int) {
 
         if (i == -1) {
             for (int j = lower_bound; j < input_String.length(); j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         } else {
             assert i >= lower_bound;
-            assert input_String.charAt(i) == input_char;
+            assert org.cprover.CProverString.charAt(input_String, i) == input_char;
 
             for (int j = lower_bound; j < i; j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         }
         return true;
     }

regression/jbmc-strings/StringIndexOf/Test.java

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null
+--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/jbmc-strings/StringIndexOf/test.desc

@@ -3,12 +3,12 @@ Test.class
 --refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 32 .* SUCCESS
-assertion at file Test.java line 34 .* SUCCESS
-assertion at file Test.java line 36 .* SUCCESS
-assertion at file Test.java line 38 .* SUCCESS
-assertion at file Test.java line 40 .* SUCCESS
-assertion at file Test.java line 42 .* SUCCESS
-assertion at file Test.java line 43 .* FAILURE
+assertion at file Test.java line 35 .* SUCCESS
+assertion at file Test.java line 37 .* SUCCESS
+assertion at file Test.java line 39 .* SUCCESS
+assertion at file Test.java line 41 .* SUCCESS
+assertion at file Test.java line 43 .* SUCCESS
+assertion at file Test.java line 45 .* SUCCESS
+assertion at file Test.java line 46 .* FAILURE
 ^VERIFICATION FAILED$
 --