Add test for String.hashCode

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringHashCode/Test.class

@@ -0,0 +1,26 @@
+public class Test {
+
+    public static int check(String s, int nondet) {
+        if(s == null)
+            return -1;
+
+        if(nondet == 0) {
+            // This is always true
+            assert "foo".hashCode() == 101574;
+        } else if(nondet == 1) {
+            // This is always false
+            assert "foo".hashCode() != 101574;
+        } else if(nondet == 2) {
+            // This is sometimes false
+            assert !s.startsWith("foo") && s.hashCode() == 101574;
+        } else if(nondet == 3) {
+            // This is always true
+            assert s.hashCode() == 101574 || !(s.startsWith("foo") && s.length() == 3);
+        } else {
+            // This is always false
+            assert "bar".hashCode() == 101574;
+        }
+
+        return s.hashCode();
+    }
+}

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

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--max-nondet-string-length 1000 --function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 8 function .*: SUCCESS
+assertion at file Test.java line 11 function .*: FAILURE
+assertion at file Test.java line 14 function .*: FAILURE
+assertion at file Test.java line 17 function .*: SUCCESS
+assertion at file Test.java line 20 function .*: FAILURE
+