Add test for StartsWith

One of this test is an exhaustive comparison with the result of a
reference implementation.

jbmc/regression/jbmc-strings/StartsWith/Test.java

@@ -0,0 +1,72 @@
+// Must be compiled with CProverString:
+// javac Test.java ../cprover/CProverString.java
+public class Test {
+
+    // Reference implementation
+    public static boolean referenceStartsWith(String s, String prefix, int offset) {
+        if (offset < 0 || offset > s.length() - prefix.length()) {
+            return false;
+        }
+
+        for (int i = 0; i < prefix.length(); i++) {
+            if (org.cprover.CProverString.charAt(s, offset + i)
+                    != org.cprover.CProverString.charAt(prefix, i)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    public static boolean check(String s, String t, int offset) {
+        // Filter out null strings
+        if(s == null || t == null) {
+            return false;
+        }
+
+        // Act
+        final boolean result = s.startsWith(t, offset);
+
+        // Assert
+        final boolean referenceResult = referenceStartsWith(s, t, offset);
+        assert(result == referenceResult);
+
+        // Check reachability
+        assert(result == false);
+        return result;
+    }
+
+    public static boolean checkDet() {
+        boolean result = false;
+        result = "foo".startsWith("foo", 0);
+        assert(result);
+        result = "foo".startsWith("f", -1);
+        assert(!result);
+        result = "foo".startsWith("oo", 1);
+        assert(result);
+        result = "foo".startsWith("f", 1);
+        assert(!result);
+        result = "foo".startsWith("bar", 0);
+        assert(!result);
+        result = "foo".startsWith("oo", 2);
+        assert(!result);
+        assert(false);
+        return result;
+    }
+
+    public static boolean checkNonDet(String s) {
+        // Filter
+        if (s == null) {
+            return false;
+        }
+
+        // Act
+        final boolean result = s.startsWith(s, 1);
+
+        // Assert
+        assert(!result);
+
+        // Check reachability
+        assert(false);
+        return result;
+    }
+}

jbmc/regression/jbmc-strings/StartsWith/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 10 --unwind 10 --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 31 .*: SUCCESS
+assertion at file Test.java line 34 .*: FAILURE
+--

jbmc/regression/jbmc-strings/StartsWith/test_det.desc

@@ -0,0 +1,13 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkDet
+^EXIT=10$
+^SIGNAL=0$
+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 47 .*: SUCCESS
+assertion at file Test.java line 49 .*: SUCCESS
+assertion at file Test.java line 51 .*: SUCCESS
+assertion at file Test.java line 52 .*: FAILURE
+--

jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkNonDet
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 66 .*: SUCCESS
+assertion at file Test.java line 69 .*: FAILURE
+--

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -21,14 +21,14 @@ Author: Romain Brenguier, [email protected]
 /// These axioms are:
 ///   1. \f$ {\tt isprefix} \Rightarrow {\tt offset_within_bounds}\f$
 ///   2. \f$ \forall 0 \le qvar<|{\tt prefix}|.\ {\tt isprefix}
-///          \Rightarrow s0[witness+{\tt offset}]=s2[witness] \f$
+///          \Rightarrow s0[qvar+{\tt offset}]=s2[qvar] \f$
 ///   3. \f$ (\lnot {\tt isprefix} \Rightarrow
 ///          \lnot {\tt offset_within_bounds}
 ///          \lor (0 \le witness<|{\tt prefix}|
 ///          \land {\tt str}[witness+{\tt offset}] \ne {\tt prefix}[witness])\f$
 /// where  \f$ {\tt offset_within_bounds} \f$ is
-///    \f$ offset \ge 0 \land offset < |str| \land
-///        |str| - |{\tt prefix}| \ge offset \f$
+///    \f$ offset \ge 0 \land offset \le |str| \land
+///        |str| - offset \ge |{\tt prefix}| \f$
 /// \param prefix: an array of characters
 /// \param str: an array of characters
 /// \param offset: an integer