Skip to content

Commit abd3947

Browse files
committed
[socket.acceptor.cons] Add postcondition for native_handle()
Fixes NB GB-17 (PDTS)
1 parent 480302e commit abd3947

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/sockets.tex

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3611,6 +3611,8 @@
36113611
\item
36123612
\tcode{enable_connection_aborted()} returns the same value as \tcode{rhs.enable_connection_aborted()} prior to the constructor invocation.
36133613
\item
3614+
\tcode{native_handle()} returns the same value as \tcode{rhs.native_handle()} prior to the constructor invocation.
3615+
\item
36143616
\tcode{protocol_} is equal to the prior value of \tcode{rhs.protocol_}.
36153617
\item
36163618
\tcode{rhs.is_open() == false}.

0 commit comments

Comments
 (0)