Improve DHCP example app

Ref. #292, #704
AdaCore · Jul 28, 2021 · 4ab5440 · 4ab5440
1 parent 9f22021
commit 4ab5440
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 28 deletions.
diff --git a/examples/apps/dhcp_client/specs/dhcp.rflx b/examples/apps/dhcp_client/specs/dhcp.rflx
@@ -6,7 +6,7 @@ package DHCP is
 
    --  DHCP Options and BOOTP Vendor Extensions (RFC 1533)
 
-   --  ISSUE: Componolit/RecordFlux-specifications#58
+   --  ISSUE: Componolit/RecordFlux-specifications#70
    --  The full list of Codes is defined in
    --  https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#options.
    type Code is
@@ -74,7 +74,7 @@ package DHCP is
        File_And_Sname_Overload => 3)
    with Size => 8;
 
-   --  ISSUE: Componolit/RecordFlux-specifications#58
+   --  ISSUE: Componolit/RecordFlux-specifications#70
    --  The full list of Codes is defined in
    --  https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#message-type-53.
    type DHCP_Message_Type is
@@ -179,7 +179,7 @@ package DHCP is
    --  DHCP Message (RFC 2131, 2)
 
    type Message_Op_Code is (BOOTREQUEST => 1, BOOTREPLY => 2) with Size => 8;
-   --  ISSUE: Componolit/RecordFlux-specifications#58
+   --  ISSUE: Componolit/RecordFlux-specifications#70
    --  The full list of Hardware Types is defined in
    --  https://www.iana.org/assignments/arp-parameters/arp-parameters.xml#arp-parameters-2.
    type Hardware_Address_Type is (HT_Reserved => 0, HT_Ethernet_10 => 1) with Size => 8, Always_Valid;

diff --git a/examples/apps/dhcp_client/specs/dhcp_client.rflx b/examples/apps/dhcp_client/specs/dhcp_client.rflx
@@ -57,7 +57,7 @@ package DHCP_Client is
             Yiaddr => 0,
             Siaddr => 0,
             Giaddr => 0,
-            Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
+            Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],  --  ISSUE: Componolit/RecordFlux#485
             Sname => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                       0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
             File => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
@@ -118,7 +118,7 @@ package DHCP_Client is
             Yiaddr => 0,
             Siaddr => Offer_Siaddr,
             Giaddr => 0,
-            Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
+            Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],  --  ISSUE: Componolit/RecordFlux#485
             Sname => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                       0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
             File => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,

diff --git a/examples/apps/dhcp_client/src/channel.adb b/examples/apps/dhcp_client/src/channel.adb
@@ -5,6 +5,9 @@ package body Channel is
    use type RFLX.RFLX_Builtin_Types.Index;
    use type Ada.Streams.Stream_Element_Offset;
 
+   --  ISSUE: Componolit/RecordFlux#482
+   --  Ada.Streams.Stream_Element_Array is not yet supported as buffer type and thus a conversion is needed.
+
    function To_Ada_Stream (Buffer : RFLX.RFLX_Builtin_Types.Bytes) return Ada.Streams.Stream_Element_Array with
      Pre => Buffer'First = 1
    is
@@ -33,20 +36,19 @@ package body Channel is
       Last : Ada.Streams.Stream_Element_Offset;
    begin
       pragma Unreferenced (Last);
-      GNAT.Sockets.Send_Socket (Socket => Send_Socket,
+      GNAT.Sockets.Send_Socket (Socket => Socket,
                                 Item => Data,
                                 Last => Last,
                                 To => GNAT.Sockets.Sock_Addr_Type'(Family => GNAT.Sockets.Family_Inet,
                                                                    Addr => GNAT.Sockets.Inet_Addr ("255.255.255.255"),
                                                                    Port => 67));
-      Network := True;
    end Send;
 
    procedure Receive (Buffer : out RFLX.RFLX_Builtin_Types.Bytes; Length : out RFLX.RFLX_Builtin_Types.Length) is
       Data : Ada.Streams.Stream_Element_Array (1 .. Buffer'Length);
       Last : Ada.Streams.Stream_Element_Offset;
    begin
-      GNAT.Sockets.Receive_Socket (Socket => Receive_Socket,
+      GNAT.Sockets.Receive_Socket (Socket => Socket,
                                    Item => Data,
                                    Last => Last);
       Buffer := To_RFLX_Bytes (Data);
@@ -57,29 +59,19 @@ package body Channel is
       Request : GNAT.Sockets.Request_Type := GNAT.Sockets.Request_Type'(Name => GNAT.Sockets.N_Bytes_To_Read,
                                                                         Size => 0);
    begin
-      GNAT.Sockets.Control_Socket (Socket => Receive_Socket, Request => Request);
+      GNAT.Sockets.Control_Socket (Socket => Socket, Request => Request);
       return Request.Size > 0;
    end Has_Data;
 
 begin
 
-   GNAT.Sockets.Create_Socket (Socket => Send_Socket,
-                               Family => GNAT.Sockets.Family_Inet,
-                               Mode => GNAT.Sockets.Socket_Datagram);
-   GNAT.Sockets.Set_Socket_Option (Socket => Send_Socket,
-                                   Level => GNAT.Sockets.Socket_Level,
-                                   Option => (GNAT.Sockets.Broadcast, True));
-   GNAT.Sockets.Create_Socket (Socket => Receive_Socket,
+   GNAT.Sockets.Create_Socket (Socket => Socket,
                                Family => GNAT.Sockets.Family_Inet,
                                Mode => GNAT.Sockets.Socket_Datagram);
-   GNAT.Sockets.Set_Socket_Option (Socket => Receive_Socket,
+   GNAT.Sockets.Set_Socket_Option (Socket => Socket,
                                    Level => GNAT.Sockets.Socket_Level,
                                    Option => (GNAT.Sockets.Broadcast, True));
-   GNAT.Sockets.Set_Socket_Option (Socket => Receive_Socket,
-                                   Level => GNAT.Sockets.Socket_Level,
-                                   Option => (Name    => GNAT.Sockets.Receive_Timeout,
-                                              Timeout => GNAT.Sockets.Timeval_Duration (5)));
-   GNAT.Sockets.Bind_Socket (Socket  => Receive_Socket,
+   GNAT.Sockets.Bind_Socket (Socket  => Socket,
                              Address => (Family => GNAT.Sockets.Family_Inet,
                                          Addr => GNAT.Sockets.Any_Inet_Addr,
                                          Port => 68));

diff --git a/examples/apps/dhcp_client/src/channel.ads b/examples/apps/dhcp_client/src/channel.ads
@@ -5,15 +5,11 @@ package Channel with
   SPARK_Mode
 is
 
-   Network : Boolean with Volatile;
-
-   Send_Socket : GNAT.Sockets.Socket_Type;
-
-   Receive_Socket : GNAT.Sockets.Socket_Type;
+   Socket : GNAT.Sockets.Socket_Type;
 
    procedure Send (Buffer : RFLX.RFLX_Builtin_Types.Bytes) with
       Global =>
-         (Output => Network);
+         (Output => Socket);
 
    use type RFLX.RFLX_Builtin_Types.Length;