PR# 19277 Post condition in {HASH_TABLE_ITERATION_CURSOR}.forth fails under certain conditions

Problem Report Summary
Submitter: finnianr
Category: EiffelBase
Priority: Low
Date: 2016/09/29
Class: Bug
Severity: Serious
Number: 19277
Release: 15.01.9.6535
Confidential: No
Status: Closed
Responsible: alexk_es
Environment: linux
Synopsis: Post condition in {HASH_TABLE_ITERATION_CURSOR}.forth fails under certain conditions

Description
The following postcondition in HASH_TABLE_ITERATION_CURSOR fails for the attached routine which is a perfectly legitimate use of a HASH_TABLE. 

ensure then -- from INDEXABLE_ITERATION_CURSOR
   cursor_index_advanced: cursor_index = old cursor_index + 1
end
To Reproduce
Run attached routine
Problem Report Interactions
From:alexk_es    Date:2017/02/26    Status: Closed    Download   
The issue is fixed in rev#99869 of EiffelStudio 17.05 intermediate release.

From:alexk_es    Date:2017/02/26    Status: Analyzed    Download   
Added test#lib044.

From:finnianr    Date:2016/09/30    Status: Open    Download   
I have noticed that if even one element is removed from the table, the iterator post condition fails

From:finnianr    Date:2016/09/29    Download   
Attachments for problem report #19277

Attachment: hash_table-bug.e     Size:450