Index: java/util/WeakHashMap.java
===================================================================
RCS file: /cvsroot/classpath/classpath/java/util/WeakHashMap.java,v
retrieving revision 1.19
diff -u -r1.19 WeakHashMap.java
--- java/util/WeakHashMap.java	2 Jul 2005 20:32:42 -0000	1.19
+++ java/util/WeakHashMap.java	26 Oct 2005 08:25:26 -0000
@@ -241,7 +241,8 @@
           // This method will get inlined.
           cleanQueue();
           if (knownMod != modCount)
-            throw new ConcurrentModificationException();
+            throw new ConcurrentModificationException(knownMod + " != "
+                                                      + modCount);
         }
 
         /**
@@ -590,7 +591,8 @@
   void cleanQueue()
   {
     Object bucket = queue.poll();
-    while (bucket != null)
+    // Use instanceof to automatically proof correctness of cast.
+    while (bucket instanceof WeakBucket)
       {
         internalRemove((WeakBucket) bucket);
         bucket = queue.poll();
@@ -698,21 +700,23 @@
     // 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 = 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;
+
+    // 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 proofen automatically.
+    WeakBucket prev = null;
+    WeakBucket next = buckets[slot];
+    while (next != bucket)
+      {
+         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--;
   }