Compatibility with GNAT.Sockets

[treiher]

GNAT.Sockets cannot be directly used with the generated SPARK code, as the buffer type Ada.Streams.Stream_Element_Array is incompatible.

   type Stream_Element is mod 2 ** Standard'Storage_Unit;

   type Stream_Element_Offset is new Long_Long_Integer;

   subtype Stream_Element_Count is
      Stream_Element_Offset range 0 .. Stream_Element_Offset'Last;

   type Stream_Element_Array is
      array (Stream_Element_Offset range <>) of aliased Stream_Element;

Ada.Streams.Stream_Element_Array does not fulfill all requirements of the current generic buffer type:

• The index type Stream_Element_Offset does not start at 1.
• It is not possible to create a bit length type with a 'Last equal to Stream_Element_Offset'Last * 8.