Re: [PATCH] ada/9535: Do not loop when writing/reading on datagram socket

[Laurent GUERBY <laurent at guerby dot net>]

On Wed, 2008-04-16 at 07:22 +0200, Samuel Tardieu wrote:
> On 16/04, Laurent GUERBY wrote:
> 
> | > +      Send_Socket
> | > +        (Stream.Socket,
> | > +         Item,
> | > +         Last,
> | > +         Stream.To);
> [...]
> | > +      if Last /= Item'Last then
> | >           raise Socket_Error;
> | >        end if;
> | 
> | IIRC the data payload of an UDP datagram can be zero (to be checked I
> | might be wrong), in this case Send_Socket will set Last to Item'First
> | and the "if" above will erroneously raise Socket_Error because Last =
> | Item'First /= Item'Last by construction of empty array bounds in Ada.
> | 
> | Might be a thing to try out as there might be similar handling
> | of zero elsewhere.
> 
> I don't think so: in "Send_Socket", "Last" is set to
>       Item'First + Ada.Streams.Stream_Element_Offset (Res - 1);
> where "Res" is the number of bytes sent; this will correctly give
> "Item'First - 1" if an empty payload has been succesfully sent.
> 
> Where did you see that "Send_Socket" would set "Last" to "Item'First"?

I skiped the "-1" :). I might be wrong again but in the case of null
arrays I don't believe the language guarantee Item'Last = Item'First - 1
just that Item'First > Item'Last, although here the GNAT implementation
might satisfy the property.

Laurent