Add a model for String.hashCode

This is very similar to the original code.

Author: romainbrenguier

src/main/java/java/lang/String.java

@@ -1919,13 +1919,16 @@ public boolean endsWith(String suffix) {
      *
      * @return  a hash code value for this object.
      *
-     * @diffblue.limitedSupport
-     * We guarantee that two strings with different hash code have different
-     * content, but the exact value will not correspond to the actual one.
+     * @diffblue.limitedSupport length of the string is limited by unwind value
      */
     public int hashCode() {
-        // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
-        return CProver.nondetInt();
+        // DIFFBLUE MODEL LIBRARY
+        int len = length();
+        int h = 0;
+        for (int i = 0; i < len; i++) {
+            h = 31 * h + CProverString.charAt(this, i);
+        }
+        return h;
         // int h = hash;
         // if (h == 0 && value.length > 0) {
         //     char val[] = value;