From 0dd01f76d6a401e73ab4e08ba99152d828eca107 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 Aug 2018 07:16:32 +0100
Subject: [PATCH] Add a model for String.hashCode

This is very similar to the original code.
---
 src/main/java/java/lang/String.java | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java
index f38b3f8..d6fe046 100644
--- a/src/main/java/java/lang/String.java
+++ b/src/main/java/java/lang/String.java
@@ -2087,13 +2087,10 @@ 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.fullSupport 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 h = hash;
         // if (h == 0 && value.length > 0) {
         //     char val[] = value;
@@ -2104,6 +2101,12 @@ public int hashCode() {
         //     hash = h;
         // }
         // return h;
+        int len = length();
+        int h = 0;
+        for (int i = 0; i < len; i++) {
+            h = 31 * h + CProverString.charAt(this, i);
+        }
+        return h;
     }
 
     /**