PR# 19895 Wrong post-condition of {ARRAYED_SET}.valid_index
Problem Report Summary
Submitter: rosivaldo
Category: EiffelBase
Priority: Low
Date: 2023/07/11
Class: Bug
Severity: Serious
Number: 19895
Release: 22.12 (22.12.10.6463 - win64)
Confidential: No
Status: Closed
Responsible:
Environment: win64
Synopsis: Wrong post-condition of {ARRAYED_SET}.valid_index
Description
{ARRAYED_SET}.valid_index's post-condition index_valid: 0 <= i and i <= count + 1 (inherited from LINEAR_SUBSET) is violated whenever i is outside valid indices' range. It seems that the post-condition should read index_valid: Result = (0 <= i and i <= count + 1).
To Reproduce
- Extract files within st.7z.
- Open st_bugs.ecf project.
- Select reproduce_arrayed_set_valid_index_bug target.
- Compile and run the system.
- Eventually the exception below will raise.
index_valid: POSTCONDITION_VIOLATION raised (POSTCONDITION_VIOLATION)
******************************** Thread exception *****************************
In thread Root thread 0x0 (thread id)
*******************************************************************************
-------------------------------------------------------------------------------
Class / Object Routine Nature of exception Effect
-------------------------------------------------------------------------------
ANNOTATED_ARRAYED_SET
valid_index @4 index_valid:
<0000000003AB85E8> Postcondition violated. Fail
-------------------------------------------------------------------------------
ANNOTATED_ARRAYED_SET
valid_index @4
<0000000003AB85E8> Routine failure. Fail
-------------------------------------------------------------------------------
APPLICATION reproduce_arrayed_set_valid_index_bug @3
not s.valid_index (5):
<0000000003AB85A8> Assertion violated. Fail
-------------------------------------------------------------------------------
APPLICATION reproduce_arrayed_set_valid_index_bug @3
<0000000003AB85A8> Routine failure. Fail
-------------------------------------------------------------------------------
APPLICATION root's creation
<0000000003AB85A8> Routine failure. Exit
-------------------------------------------------------------------------------