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