indexing
description: "A datagram socket."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2007-01-26 09:09:11 -0800 (Fri, 26 Jan 2007) $"
revision: "$Revision: 66294 $"
deferred class interface
DATAGRAM_SOCKET
feature
create_from_descriptor (fd: INTEGER_32)
`fd'
SOCKET
ensure SOCKET
family_valid: family = address.family
opened_all: is_open_write and is_open_read
feature
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
retrieved: ANY
Retrieve_exception
SOCKET
require IO_MEDIUM
is_readable: readable
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
support_storable: support_storable
ensure IO_MEDIUM
result_exists: Result /= Void
feature
frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
frozen is_deep_equal (other: DATAGRAM_SOCKET): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: DATAGRAM_SOCKET): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: DATAGRAM_SOCKET): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
address_in_use: BOOLEAN
SOCKET_RESOURCES
address_not_readable: BOOLEAN
SOCKET_RESOURCES
already_bound: BOOLEAN
SOCKET_RESOURCES
bad_socket_handle: BOOLEAN
SOCKET_RESOURCES
bound: BOOLEAN
bytes_read: INTEGER_32
read_to_managed_pointer
IO_MEDIUM
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
connect_in_progress: BOOLEAN
SOCKET_RESOURCES
connection_refused: BOOLEAN
SOCKET_RESOURCES
dtable_full: BOOLEAN
SOCKET_RESOURCES
error: STRING_8
SOCKET_RESOURCES
error_number: INTEGER_32
SOCKET_RESOURCES
expired_socket: BOOLEAN
SOCKET_RESOURCES
invalid_address: BOOLEAN
SOCKET_RESOURCES
invalid_socket_handle: BOOLEAN
SOCKET_RESOURCES
is_plain_text: BOOLEAN
IO_MEDIUM
is_valid_peer_address (addr: SOCKET_ADDRESS): BOOLEAN
`addr'
SOCKET
require SOCKET
address_exists: addr /= Void
last_character: CHARACTER_8
read_character
IO_MEDIUM
last_double: REAL_64
read_double
IO_MEDIUM
last_integer: INTEGER_32
read_integer
IO_MEDIUM
last_integer_16: INTEGER_16
read_integer_16
IO_MEDIUM
last_integer_32: INTEGER_32
last_integer
IO_MEDIUM
last_integer_64: INTEGER_64
read_integer_64
IO_MEDIUM
last_integer_8: INTEGER_8
read_integer_8
IO_MEDIUM
last_natural: NATURAL_32
read_natural
IO_MEDIUM
last_natural_16: NATURAL_16
read_natural_16
IO_MEDIUM
last_natural_32: NATURAL_32
last_natural
IO_MEDIUM
last_natural_64: NATURAL_64
read_natural_64
IO_MEDIUM
last_natural_8: NATURAL_8
read_natural_8
IO_MEDIUM
last_real: REAL_32
read_real
IO_MEDIUM
last_string: ?STRING_8
IO_MEDIUM
network: BOOLEAN
SOCKET_RESOURCES
no_buffers: BOOLEAN
SOCKET_RESOURCES
no_permission: BOOLEAN
SOCKET_RESOURCES
not_connected: BOOLEAN
SOCKET_RESOURCES
protected_address: BOOLEAN
SOCKET_RESOURCES
protocol_not_supported: BOOLEAN
SOCKET_RESOURCES
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
socket_family_not_supported: BOOLEAN
SOCKET_RESOURCES
socket_in_use: BOOLEAN
SOCKET_RESOURCES
socket_ok: BOOLEAN
SOCKET_RESOURCES
socket_would_block: BOOLEAN
SOCKET_RESOURCES
support_storable: BOOLEAN
SOCKET
zero_option: BOOLEAN
SOCKET_RESOURCES
feature
basic_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
general_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
independent_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
feature
dispose
IO_MEDIUM
feature
copy (other: DATAGRAM_SOCKET)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: DATAGRAM_SOCKET)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: DATAGRAM_SOCKET
ANY
ensure ANY
deep_twin_not_void: Result /= Void
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: DATAGRAM_SOCKET)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: DATAGRAM_SOCKET
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: DATAGRAM_SOCKET
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
name: STRING_8
SOCKET
require IO_MEDIUM
True
require else SOCKET
socket_exists: exists
feature
bind
close
connect_to_peer (a_peer_address: like address)
`a_peer_address'
require
socket_exists: exists
frozen default: ?DATAGRAM_SOCKET
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
lastchar: CHARACTER_8
read_character
IO_MEDIUM
lastdouble: REAL_64
read_double
IO_MEDIUM
lastint: INTEGER_32
read_integer
IO_MEDIUM
lastreal: REAL_32
read_real
IO_MEDIUM
laststring: ?STRING_8
IO_MEDIUM
feature
address: SOCKET_ADDRESS
SOCKET
socket_bind
address
SOCKET
require SOCKET
socket_exists: exists
valid_local_address: address /= Void
cleanup
SOCKET
socket_close
SOCKET
require IO_MEDIUM
medium_is_open: not is_closed
require else SOCKET
socket_exists: exists
close_socket
SOCKET
require SOCKET
socket_exists: exists
is_open: is_open_read or is_open_write
ensure SOCKET
is_closed: is_closed
not_is_open: not is_open_read and not is_open_write
connect
SOCKET
require SOCKET
socket_exists: exists
valid_peer_address: peer_address /= Void
descriptor: INTEGER_32
SOCKET
descriptor_available: BOOLEAN
SOCKET
family: INTEGER_32
SOCKET
is_closed: BOOLEAN
SOCKET
make_socket
SOCKET
require SOCKET
valid_family: family >= 0
valid_type: type >= 0
valid_protocol: protocol >= 0
peer_address: like address
SOCKET
protocol: INTEGER_32
`udp'`tcp'
SOCKET
set_address (addr: like address)
`addr'
SOCKET
require SOCKET
same_type: addr.family = family
ensure SOCKET
address_set: address = addr
set_peer_address (addr: like address)
`addr'
SOCKET
require SOCKET
address_exists: addr /= Void
address_valid: is_valid_peer_address (addr)
ensure SOCKET
address_set: peer_address = addr
type: INTEGER_32
SOCKET
feature
make
make_bound_to_address (a_local_address: like address)
`local_address'
make_connected_to_peer (a_peer_address: like address)
peer_address
feature
c_msgdontroute: INTEGER_32
SOCKET_RESOURCES
c_oobmsg: INTEGER_32
SOCKET_RESOURCES
c_peekmsg: INTEGER_32
SOCKET_RESOURCES
feature
last_boolean: BOOLEAN
SOCKET
read (size: INTEGER_32): PACKET
`size'
SOCKET
require SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_boolean
last_boolean
SOCKETreadbool
SOCKET
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_character
last_character
SOCKETreadchar
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_double
last_double
SOCKETreaddouble
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer
last_integer
SOCKETreadintread_integer_32
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer_16
last_integer_16
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer_32
last_integer
SOCKETread_integerreadint
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer_64
last_integer_64
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer_8
last_integer_8
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_line
SOCKETreadline
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
ensure IO_MEDIUM
last_string_not_void: last_string /= Void
read_natural
last_natural
SOCKETread_natural_32
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_natural_16
last_natural_16
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_natural_32
last_natural
SOCKETread_natural
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_natural_64
last_natural_64
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_natural_8
last_natural_8
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_real
last_real
SOCKETreadreal
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_stream (nb_char: INTEGER_32)
`nb_char'
last_string
SOCKETreadstream
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
ensure IO_MEDIUM
last_string_not_void: last_string /= Void
read_to_managed_pointer (p: MANAGED_POINTER; start_pos, nb_bytes: INTEGER_32)
`nb_bytes'
`p'`start_pos'
SOCKET
require IO_MEDIUM
p_not_void: p /= Void
p_large_enough: p.count >= nb_bytes + start_pos
nb_bytes_non_negative: nb_bytes >= 0
is_readable: readable
require else SOCKET
p_not_void: p /= Void
p_large_enough: p.count >= nb_bytes + start_pos
nb_bytes_non_negative: nb_bytes >= 0
socket_exists: exists
opened_for_read: is_open_read
ensure IO_MEDIUM
bytes_read_non_negative