PR# 19898 Possibly unnecessary precondition in {ARRAYED_SET}.move_item
Problem Report Summary
Submitter: rosivaldo
Category: EiffelBase
Priority: Low
Date: 2023/08/09
Class: Bug
Severity: Non-critical
Number: 19898
Release: 22.12 (22.12.10.6463 - win64)
Confidential: No
Status: Closed
Responsible:
Environment: win64
Synopsis: Possibly unnecessary precondition in {ARRAYED_SET}.move_item
Description
{ARRAYED_SET}.move_item feature keeps a possibly unnecessary, and annoying, precondition: item_exists: v /= Void. Nothing prevents, say, an ARRAYED_SET [detachable...] of inserting Void items; besides, {ARRAYED_SET}.move_item implementation works perfectly (as it should, I think) with a Void argument, regardless of {ARRAYED_SET}.object_comparison status, i.e. it is safe to compare Void with both = and ~ operators.
To Reproduce
- Extract all files from st.7z (attached).
- Open and compile st_bugs.ecf project, targeted to reproduce_arrayed_set_move_item_bug_item_exists.
- Target EiffelStudio editor to {APPLICATION}.reproduce_arrayed_set_move_item_bug_item_exists.
- Please take a look at lines 88 and 94: one can see that the very same implementation of {ARRAYED_SET}.move_item can accept Void arguments with no problem.
- Run the system (press F5).
- The exception below will raise, despite the fact that a Void argument would cause no harm (line 88, which compares Void by reference, has run with no problem).
- Please continue to the steps after the reproduced exception.
item_exists: PRECONDITION_VIOLATION raised (PRECONDITION_VIOLATION)
******************************** Thread exception *****************************
In thread Root thread 0x0 (thread id)
*******************************************************************************
-------------------------------------------------------------------------------
Class / Object Routine Nature of exception Effect
-------------------------------------------------------------------------------
ARRAYED_SET move_item @1 item_exists:
<00000000041F8938> (From LINEAR_SUBSET) Precondition violated. Fail
-------------------------------------------------------------------------------
APPLICATION reproduce_arrayed_set_move_item_bug_item_exists @16
<00000000041F85A8> Routine failure. Fail
-------------------------------------------------------------------------------
APPLICATION root's creation
<00000000041F85A8> Routine failure. Exit
-------------------------------------------------------------------------------
- (Continue).
- Press F5 to resume system execution.
- Go to system console and press Return to finish system execution.
- Target EiffelStudio editor to {APPLICATION}.reproduce_arrayed_set_move_item_bug_item_exists.
- Comment out line 100 (which reads s2.move_item (Void) -- Precondition violated: item_exists: v /= Void).
- Recompile the system.
- Run the system again (press F5).
- The exception below will raise, despite the fact that a Void argument would cause no harm (line 94, which compares Void by value, has run with no problem).
item_exists: PRECONDITION_VIOLATION raised (PRECONDITION_VIOLATION)
******************************** Thread exception *****************************
In thread Root thread 0x0 (thread id)
*******************************************************************************
-------------------------------------------------------------------------------
Class / Object Routine Nature of exception Effect
-------------------------------------------------------------------------------
ARRAYED_SET move_item @1 item_exists:
<00000000042C6938> (From LINEAR_SUBSET) Precondition violated. Fail
-------------------------------------------------------------------------------
APPLICATION reproduce_arrayed_set_move_item_bug_item_exists @21
<00000000042C65A8> Routine failure. Fail
-------------------------------------------------------------------------------
APPLICATION root's creation
<00000000042C65A8> Routine failure. Exit
-------------------------------------------------------------------------------