Add verification test for String.equals

We add tests which compare the internal String.equals with a reference
implementation which loops over the characters of the string.

Author: romainbrenguier

regression/jbmc-strings/StringEquals/Test.class

@@ -1,3 +1,6 @@
+// Uses CProverString, must be compiled with ../cprover/CProverString.java
+import org.cprover.*;
+
 public class Test {
     public static void check(int i, String s) {
         String t = "Hello World";
@@ -15,4 +18,51 @@ else if (i==4)
         else if (i==5)
             assert(s.equals(x));
     }
+
+    public static boolean referenceImplementation(String s, Object o) {
+        if (s == null)
+            return o == null;
+        if (! (o instanceof String))
+            return false;
+
+        String s2 = (String) o;
+        if (s.length() != s2.length())
+            return false;
+
+        for (int i = 0; i < s.length(); i++) {
+            if (CProverString.charAt(s, i) != CProverString.charAt(s2, i))
+                return false;
+        }
+
+        return true;
+    }
+
+    public static boolean verifyNonNull(String s, Object o) {
+        // Filter
+        if (s == null || o == null)
+            return false;
+
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
+    public static boolean verify(String s, Object o) {
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
 }

regression/jbmc-strings/StringEquals/Test.java

@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+ --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verify
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 62 .* SUCCESS
+--
+--
+Our current implementation does not handle the null case
+TG-2179

regression/jbmc-strings/StringEquals/test_verify.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+ --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 50 .* SUCCESS
+--