PR# 19428 Post condition violation in {UNIX_STREAM_SOCKET}.accept
Problem Report Summary
Submitter: finnianr
Category: EiffelNet
Priority: Low
Date: 2018/02/07
Class: Bug
Severity: Non-critical
Number: 19428
Release: 16.05
Confidential: No
Status: Open
Responsible:
Environment: linux
Synopsis: Post condition violation in {UNIX_STREAM_SOCKET}.accept
Description
The routine {UNIX_STREAM_SOCKET}.accept uses the creation procedure `create_from_descriptor' to make the `accepted' socket. This is problematic as is does nothing to ensure that `is_blocking' is the same value in the listening socket as the `accepted' socket, thus violating the post-condition `same_blocking_status'. UNIX_STREAM_SOCKET.is_blocking is True after calling `make_server', but with `create_from_descriptor` the default value is False. Hence the problem. accept -- Accept a new connection on listen socket. -- Accepted service socket available in accepted. require -- from STREAM_SOCKET socket_exists: exists address_attached: address /= Void ensure -- from STREAM_SOCKET same_blocking_status: attached accepted as l_accepted implies l_accepted.is_blocking = is_blocking
To Reproduce
Problem Report Interactions