PR# 19652 Postcondition violation in SPECIAL.copy

Problem Report Summary
Submitter: gobobe
Category: EiffelBase
Priority: Medium
Date: 2020/06/12
Class: Bug
Severity: Non-critical
Number: 19652
Release: 20.05
Confidential: No
Status: Open
Responsible:
Environment: win
Synopsis: Postcondition violation in SPECIAL.copy

Description
The implementation of SPECIAL.copy violates its postcondition "is_equal":

		local
			sp1, sp2: SPECIAL [CHARACTER]
		do
				-- `sp1' has more items than `sp2'.
				-- All items of `sp2' will be copied to `sp1'.
				-- The other items in `sp1' will not be changed.
				-- The 'count' and 'capacity' in `sp1' will not change.
			create sp1.make_empty (10)
			sp1.extend ('a')
			sp1.extend ('b')
			sp1.extend ('c')
			create sp2.make_empty (5)
			sp2.extend ('x')
			sp2.extend ('y')
			sp1.copy (sp2)

--
Eric Bezault
To Reproduce

										
Problem Report Interactions