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.
smowton · Jan 19, 2018 · bcb076b · bcb076b
1 parent 8360233
commit bcb076b
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 11 deletions.
diff --git a/regression/jbmc-strings/StringIndexOf/Test.class b/regression/jbmc-strings/StringIndexOf/Test.class
diff --git a/regression/jbmc-strings/StringIndexOf/Test.java b/regression/jbmc-strings/StringIndexOf/Test.java
@@ -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;
     }

diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc
@@ -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$

diff --git a/regression/jbmc-strings/StringIndexOf/test2.desc b/regression/jbmc-strings/StringIndexOf/test2.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$
 --