Merge pull request #1756 from romainbrenguier/tests/index-of-corrections#TG-2246

Correct tests for String.indexOf

Author: tautschnig

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$
 --