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
Environment: linux
Synopsis: Post condition violation in {UNIX_STREAM_SOCKET}.accept

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 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