2005-10-26 Roman Kennke <kennke@aicas.com>

	Reported by Friedjof Siebert  <siebert@aicas.com>
	* java/util/WeakHashMap.java
	(WeakEntrySet.Iterator.checkMod): Improved exception message.
	(internalRemove): Removed redundant reads of buckets[slot] and
	prev.next and added checks to ensure that no null pointer
	exception may occur and that this can be proved automatically.

1 files changed, 14 insertions, 14 deletions

diff --git a/java/util/WeakHashMap.java b/java/util/WeakHashMap.java
index 7593f7e33..514ad8cd2 100644
--- a/java/util/WeakHashMap.java
+++ b/java/util/WeakHashMap.java
@@ -241,7 +241,8 @@ public class WeakHashMap extends AbstractMap implements Map
           // This method will get inlined.
           cleanQueue();
           if (knownMod != modCount)
-            throw new ConcurrentModificationException();
+            throw new ConcurrentModificationException(knownMod + " != "
+                                                      + modCount);
         }
 
         /**
@@ -698,21 +699,20 @@ public class WeakHashMap extends AbstractMap implements Map
     // bucket may be enqueued later by the garbage collection, and
     // internalRemove will be called a second time.
     bucket.slot = -1;
-    if (buckets[slot] == bucket)
-      buckets[slot] = bucket.next;
-    else
+
+    WeakBucket prev = null;
+    WeakBucket next = buckets[slot];
+    while (next != bucket)
       {
-        WeakBucket prev = buckets[slot];
-        /* This may throw a NullPointerException.  It shouldn't but if
-         * a race condition occurred (two threads removing the same
-         * bucket at the same time) it may happen.  <br>
-         * But with race condition many much worse things may happen
-         * anyway.
-         */
-        while (prev.next != bucket)
-          prev = prev.next;
-        prev.next = bucket.next;
+         if (next == null) throw new InternalError("WeakHashMap in incosistent state");
+         prev = next; 
+         next = prev.next;
       }
+    if (prev == null)
+      buckets[slot] = bucket.next;
+    else 
+      prev.next = bucket.next;
+
     size--;
   }