Merge pull request #978 from romainbrenguier/feature/index-of-precise

Make String.indexOf and String.lastIndexOf precise

Author: forejtv

regression/strings-smoke-tests/java_index_of/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 test_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-Issue: cbmc/test-gen#77

regression/strings-smoke-tests/java_index_of/test_index_of.class

@@ -1,10 +1,13 @@
 public class test_index_of
 {
-   public static void main(/*String[] argv*/)
-   {
-      String s = "Abc";
-      String bc = "bc";
-      int i = s.indexOf(bc);
-      assert(i == 1);
-   }
+    public static void main(/*String[] argv*/)
+    {
+        String s = "Abc";
+        String bc = "bc";
+        String ab = "ab";
+        int i = s.indexOf(bc);
+        int j = s.indexOf(ab);
+        assert(i == 1);
+        assert(j == -1);
+    }
 }

regression/strings-smoke-tests/java_index_of/test_index_of.java

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 test_last_index_of.class
 --refine-strings
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
 --
-Issue: diffblue/test-gen#77

regression/strings-smoke-tests/java_last_index_of/test.desc

@@ -1,10 +1,11 @@
 public class test_last_index_of
 {
-   public static void main(/*String[] argv*/)
-   {
-      String s = "abcab";
-      String ab = "ab";
-      int i = s.lastIndexOf(ab);
-      assert(i == 3);
-   }
+    public static void main(/*String[] argv*/)
+    {
+        String s = "abcab";
+        String ab = "ab";
+        int i = s.lastIndexOf(ab);
+        assert(i == 3);
+        assert(i == 1);
+    }
 }

regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class

@@ -194,24 +194,18 @@ class string_constraint_generatort
     const exprt &from_index);
 
   // Add axioms corresponding to the String.indexOf:(String;I) java function
-  // TODO: the specifications are only partial:
-  // we add axioms stating that the returned value is either -1 or greater than
-  // from_index and the string beggining there has prefix substring
   exprt add_axioms_for_index_of_string(
-    const string_exprt &str,
-    const string_exprt &substring,
+    const string_exprt &haystack,
+    const string_exprt &needle,
     const exprt &from_index);
 
   // Add axioms corresponding to the String.indexOf java functions
-  // TODO: the specifications are only partial for the ones that look for
-  // strings
   exprt add_axioms_for_index_of(const function_application_exprt &f);
 
   // Add axioms corresponding to the String.lastIndexOf:(String;I) java function
-  // TODO: the specifications are only partial
   exprt add_axioms_for_last_index_of_string(
-    const string_exprt &str,
-    const string_exprt &substring,
+    const string_exprt &haystack,
+    const string_exprt &needle,
     const exprt &from_index);
 
   // Add axioms corresponding to the String.lastIndexOf:(CI) java function
@@ -221,7 +215,6 @@ class string_constraint_generatort
     const exprt &from_index);
 
   // Add axioms corresponding to the String.lastIndexOf java functions
-  // TODO: the specifications is only partial
   exprt add_axioms_for_last_index_of(const function_application_exprt &f);
 
   // TODO: the specifications of these functions is only partial