Test for verification of the indexOf method

One of these is exhaustive and too slow to run so it is marked as
THOROUGH and should be run every time axioms for the indexOf methods are touched.

Author: romainbrenguier

regression/jbmc-strings/StringIndexOf/Test.class

@@ -0,0 +1,46 @@
+public class Test {
+
+    public boolean check(String input_String, char input_char, int input_int) {
+        // Verify indexOf is conform to its specification
+        int i = input_String.indexOf(input_char, input_int);
+
+        assert i < input_String.length();
+
+        int lower_bound;
+        if (input_int < 0)
+            lower_bound = 0;
+        else
+            lower_bound = input_int;
+
+        if (i == -1) {
+            for (int j = lower_bound; j < input_String.length(); j++)
+                assert input_String.charAt(j) != input_char;
+        } else {
+            assert i >= lower_bound;
+            assert input_String.charAt(i) == input_char;
+
+            for (int j = lower_bound; j < i; j++)
+                assert input_String.charAt(j) != input_char;
+        }
+        return true;
+    }
+
+    public boolean check2() {
+        // Verification should fail, this is to check the solver does
+        // not get a contradiction
+        int i = "hello".indexOf('o', 1);
+        assert i == 4;
+        i = "hello".indexOf('h', 1);
+        assert i == -1;
+        i = "hello".indexOf('e', 4);
+        assert i == -1;
+        i = "hello".indexOf('e', 8);
+        assert i == -1;
+        i = "hello".indexOf('x', 0);
+        assert i == -1;
+        i = "hello".indexOf('h', -1000);
+        assert i == 0;
+        assert false;
+        return true;
+    }
+}

regression/jbmc-strings/StringIndexOf/Test.java

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

regression/jbmc-strings/StringIndexOf/test.desc

@@ -0,0 +1,14 @@
+CORE
+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
+^VERIFICATION FAILED$
+--

regression/jbmc-strings/StringIndexOf/test2.desc

@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--