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