Commit bf56eac5 authored by yoogx's avatar yoogx

* polyorb_hi-messages.ad?: code reorganization and

          simplification to suppress potential runtime errors as
          spotted by GNATProve GPL 2013

        * Updates other packages accordingly
parent adf6c07a
...@@ -218,7 +218,7 @@ package body PolyORB_HI_Drivers_GRSPW is ...@@ -218,7 +218,7 @@ package body PolyORB_HI_Drivers_GRSPW is
PolyORB_HI_Generated.Transport.Deliver PolyORB_HI_Generated.Transport.Deliver
(Corresponding_Entity (Corresponding_Entity
(Integer_8 (SEA (Message_Length_Size + 1))), (Unsigned_8 (SEA (Message_Length_Size + 1))),
To_PO_HI_Full_Stream (SEA) To_PO_HI_Full_Stream (SEA)
(1 .. Stream_Element_Offset (SEO))); (1 .. Stream_Element_Offset (SEO)));
end loop Main_Loop; end loop Main_Loop;
......
...@@ -304,7 +304,7 @@ package body PolyORB_HI_Drivers_GRUART is ...@@ -304,7 +304,7 @@ package body PolyORB_HI_Drivers_GRUART is
PolyORB_HI_Generated.Transport.Deliver PolyORB_HI_Generated.Transport.Deliver
(Corresponding_Entity (Corresponding_Entity
(Integer_8 (SEA (Message_Length_Size + 1))), (Unsigned_8 (SEA (Message_Length_Size + 1))),
To_PO_HI_Full_Stream (SEA) To_PO_HI_Full_Stream (SEA)
(1 .. Stream_Element_Offset (SEO))); (1 .. Stream_Element_Offset (SEO)));
else else
......
...@@ -276,7 +276,7 @@ package body PolyORB_HI_Drivers_Native_TCP_IP is ...@@ -276,7 +276,7 @@ package body PolyORB_HI_Drivers_Native_TCP_IP is
-- Identify peer node -- Identify peer node
Node := Corresponding_Node (Integer_8 (SEC (SEC'First))); Node := Corresponding_Node (Unsigned_8 (SEC (SEC'First)));
Nodes (Node).Socket_Receive := Socket; Nodes (Node).Socket_Receive := Socket;
pragma Debug (Put_Line (Verbose, "Connection from node " pragma Debug (Put_Line (Verbose, "Connection from node "
& Node_Type'Image (Node))); & Node_Type'Image (Node)));
...@@ -365,7 +365,7 @@ package body PolyORB_HI_Drivers_Native_TCP_IP is ...@@ -365,7 +365,7 @@ package body PolyORB_HI_Drivers_Native_TCP_IP is
PolyORB_HI_Generated.Transport.Deliver PolyORB_HI_Generated.Transport.Deliver
(Corresponding_Entity (Corresponding_Entity
(Integer_8 (SEA (Message_Length_Size + 1))), (Unsigned_8 (SEA (Message_Length_Size + 1))),
To_PO_HI_Full_Stream (SEA) To_PO_HI_Full_Stream (SEA)
(1 .. Stream_Element_Offset (SEO))); (1 .. Stream_Element_Offset (SEO)));
end if; end if;
......
...@@ -324,7 +324,7 @@ package body PolyORB_HI_Drivers_Native_UART is ...@@ -324,7 +324,7 @@ package body PolyORB_HI_Drivers_Native_UART is
begin begin
PolyORB_HI_Generated.Transport.Deliver PolyORB_HI_Generated.Transport.Deliver
(Corresponding_Entity (Corresponding_Entity
(Integer_8 (SEA (Message_Length_Size + 1))), (Unsigned_8 (SEA (Message_Length_Size + 1))),
To_PO_HI_Full_Stream (SEA) To_PO_HI_Full_Stream (SEA)
(1 .. Stream_Element_Offset (SEO))); (1 .. Stream_Element_Offset (SEO)));
exception exception
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. -- -- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- -- -- --
-- PolyORB HI is free software; you can redistribute it and/or modify it -- -- PolyORB HI is free software; you can redistribute it and/or modify it --
-- under terms of the GNU General Public License as published by the Free -- -- under terms of the GNU General Public License as published by the Free --
...@@ -61,6 +61,9 @@ package body PolyORB_HI.Messages is ...@@ -61,6 +61,9 @@ package body PolyORB_HI.Messages is
Receiver_Offset : constant Stream_Element_Offset := Message_Length_Size + 1; Receiver_Offset : constant Stream_Element_Offset := Message_Length_Size + 1;
Sender_Offset : constant Stream_Element_Offset := Message_Length_Size + 2; Sender_Offset : constant Stream_Element_Offset := Message_Length_Size + 2;
function Length (M : Message_Type) return PDU_Index;
-- Return length of message M
----------------- -----------------
-- Encapsulate -- -- Encapsulate --
----------------- -----------------
...@@ -71,16 +74,14 @@ package body PolyORB_HI.Messages is ...@@ -71,16 +74,14 @@ package body PolyORB_HI.Messages is
Entity : Entity_Type) Entity : Entity_Type)
return Stream_Element_Array return Stream_Element_Array
is is
L : constant Stream_Element_Count := Length (Message) + Header_Size; L : constant Stream_Element_Count := Message.Last + Header_Size;
R : Stream_Element_Array (1 .. L); R : Stream_Element_Array (1 .. L);
begin begin
R (1 .. Message_Length_Size) := To_Buffer (L - 1); R (1 .. Message_Length_Size) := To_Buffer (L - 1);
R (Receiver_Offset) := Stream_Element (Internal_Code (Entity)); R (Receiver_Offset) := Stream_Element (Internal_Code (Entity));
R (Sender_Offset) := Stream_Element (Internal_Code (From)); R (Sender_Offset) := Stream_Element (Internal_Code (From));
R (Header_Size + 1 .. Header_Size + Message.Last)
for J in 1 .. Length (Message) loop := Message.Content (Message.First .. Message.Last);
R (Header_Size + J) := Message.Content (J);
end loop;
return R; return R;
end Encapsulate; end Encapsulate;
...@@ -89,9 +90,15 @@ package body PolyORB_HI.Messages is ...@@ -89,9 +90,15 @@ package body PolyORB_HI.Messages is
-- Length -- -- Length --
------------ ------------
function Length (M : Message_Type) return Stream_Element_Count is function Length (M : Message_Type) return PDU_Index is
begin begin
return M.Last + 1 - M.First; if M.First >= 1
and then M.Last - M.First >= 0
then
return M.Last - M.First + 1;
else
return 0; -- XXX defensive
end if;
end Length; end Length;
------------- -------------
...@@ -99,13 +106,8 @@ package body PolyORB_HI.Messages is ...@@ -99,13 +106,8 @@ package body PolyORB_HI.Messages is
------------- -------------
function Payload (M : Message_Type) return Stream_Element_Array is function Payload (M : Message_Type) return Stream_Element_Array is
Payload : Stream_Element_Array (M.First .. M.Last);
begin begin
for J in M.First .. M.Last loop return M.Content (M.First .. M.Last);
Payload (J) := M.Content (J);
end loop;
return Payload;
end Payload; end Payload;
------------ ------------
...@@ -117,13 +119,9 @@ package body PolyORB_HI.Messages is ...@@ -117,13 +119,9 @@ package body PolyORB_HI.Messages is
return Sender (M.Content (M.First .. M.Last)); return Sender (M.Content (M.First .. M.Last));
end Sender; end Sender;
------------
-- Sender --
------------
function Sender (M : Stream_Element_Array) return Entity_Type is function Sender (M : Stream_Element_Array) return Entity_Type is
begin begin
return Corresponding_Entity (Integer_8 (M (Sender_Offset))); return Corresponding_Entity (Unsigned_8 (M (Sender_Offset)));
end Sender; end Sender;
---------- ----------
...@@ -135,19 +133,27 @@ package body PolyORB_HI.Messages is ...@@ -135,19 +133,27 @@ package body PolyORB_HI.Messages is
Item : out Stream_Element_Array; Item : out Stream_Element_Array;
Last : out Stream_Element_Offset) Last : out Stream_Element_Offset)
is is
L1 : constant Stream_Element_Count := Item'Length; Read_Elts : constant Stream_Element_Count
L2 : Stream_Element_Count := Length (Stream); := Stream_Element_Count'Min (Item'Length, Length (Stream));
begin begin
if L1 < L2 then if Read_Elts < 1 then
L2 := L1; -- We have nothing to read, exit
Last := 0;
return;
elsif Read_Elts = Item'Length then
Last := Item'Last;
else
Last := Item'First + Read_Elts - 1;
end if; end if;
for J in 0 .. L2 - 1 loop Item (Item'First .. Last)
Item (Item'First + J) := Stream.Content (Stream.First + J); := Stream.Content (Stream.First .. Stream.First + Read_Elts - 1);
end loop;
Last := Item'First + L2 - 1; if Stream.First + Read_Elts < Stream.Content'Last then
Stream.First := Stream.First + L2; Stream.First := Stream.First + Read_Elts;
else
Stream.First := 0;
end if;
end Read; end Read;
---------------- ----------------
...@@ -170,16 +176,17 @@ package body PolyORB_HI.Messages is ...@@ -170,16 +176,17 @@ package body PolyORB_HI.Messages is
is is
begin begin
if Stream.First > Stream.Last then if Stream.First > Stream.Last then
-- The message is invalid, we reset it
Stream.First := 1; Stream.First := 1;
Stream.Last := 0; Stream.Last := 0;
end if; end if;
for J in Item'Range loop if Item'Length > Stream.Content'Last - Stream.Last then
Stream.Content (Stream.Last raise Program_Error;
+ Stream_Element_Offset (J - Item'First + 1)) end if;
:= Item (J);
end loop;
Stream.Content (Stream.Last + 1 .. Stream.Last + Item'Length) := Item;
Stream.Last := Stream.Last + Item'Length; Stream.Last := Stream.Last + Item'Length;
end Write; end Write;
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. -- -- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- -- -- --
-- PolyORB HI is free software; you can redistribute it and/or modify it -- -- PolyORB HI is free software; you can redistribute it and/or modify it --
-- under terms of the GNU General Public License as published by the Free -- -- under terms of the GNU General Public License as published by the Free --
...@@ -46,8 +46,6 @@ package PolyORB_HI.Messages is ...@@ -46,8 +46,6 @@ package PolyORB_HI.Messages is
type Message_Type is private; type Message_Type is private;
-- Base type of messages exchanged between nodes -- Base type of messages exchanged between nodes
Invalid_Message : constant Message_Type;
Message_Length_Size : constant := 2; Message_Length_Size : constant := 2;
-- Number of bytes to store a message size -- Number of bytes to store a message size
...@@ -83,9 +81,6 @@ package PolyORB_HI.Messages is ...@@ -83,9 +81,6 @@ package PolyORB_HI.Messages is
procedure Reallocate (M : in out Message_Type); procedure Reallocate (M : in out Message_Type);
-- Reset M -- Reset M
function Length (M : Message_Type) return Stream_Element_Count;
-- Return length of message M
function Payload (M : Message_Type) return Stream_Element_Array; function Payload (M : Message_Type) return Stream_Element_Array;
-- Return the remaining payload of message M -- Return the remaining payload of message M
...@@ -103,17 +98,15 @@ package PolyORB_HI.Messages is ...@@ -103,17 +98,15 @@ package PolyORB_HI.Messages is
private private
subtype PDU_Index is Stream_Element_Count range 0 .. PDU_Size;
subtype PDU is Stream_Element_Array (1 .. PDU_Index'Last);
type Message_Type is record type Message_Type is record
Content : Stream_Element_Array (1 .. PDU_Size); Content : PDU;
First : Stream_Element_Count := 1; First : PDU_Index := 1;
Last : Stream_Element_Count := 0; Last : PDU_Index := 0;
end record; end record;
Invalid_Message : constant Message_Type :=
(Content => (1 .. PDU_Size => Stream_Element (0)),
First => 1,
Last => 0);
pragma Inline (To_Length); pragma Inline (To_Length);
pragma Inline (To_Buffer); pragma Inline (To_Buffer);
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. -- -- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- -- -- --
-- PolyORB HI is free software; you can redistribute it and/or modify it -- -- PolyORB HI is free software; you can redistribute it and/or modify it --
-- under terms of the GNU General Public License as published by the Free -- -- under terms of the GNU General Public License as published by the Free --
...@@ -259,7 +259,7 @@ package body PolyORB_HI.Transport_Low_Level is ...@@ -259,7 +259,7 @@ package body PolyORB_HI.Transport_Low_Level is
-- Identify peer node -- Identify peer node
Node := Corresponding_Node (Integer_8 (SEC (SEC'First))); Node := Corresponding_Node (Unsigned_8 (SEC (SEC'First)));
Nodes (Node).Socket_Receive := Socket; Nodes (Node).Socket_Receive := Socket;
pragma Debug (Put_Line (Verbose, "Connection from node " pragma Debug (Put_Line (Verbose, "Connection from node "
& Node_Image (Node))); & Node_Image (Node)));
...@@ -304,8 +304,9 @@ package body PolyORB_HI.Transport_Low_Level is ...@@ -304,8 +304,9 @@ package body PolyORB_HI.Transport_Low_Level is
-- Receive message length -- Receive message length
Receive_Socket (Nodes (N).Socket_Receive, SEL, SEO); Receive_Socket (Nodes (N).Socket_Receive, SEL, SEO);
pragma Debug (Put_Line (Verbose, "SEL " & SEL'Length'Img
-- Receive zero bytes means that peer is dead & "MLS" & Message_Length_Size'Img));
-- Receiving zero byte means that peer is dead
if SEO = 0 then if SEO = 0 then
pragma Debug (Put_Line pragma Debug (Put_Line
...@@ -334,7 +335,7 @@ package body PolyORB_HI.Transport_Low_Level is ...@@ -334,7 +335,7 @@ package body PolyORB_HI.Transport_Low_Level is
PolyORB_HI_Generated.Transport.Deliver PolyORB_HI_Generated.Transport.Deliver
(Corresponding_Entity (Corresponding_Entity
(Integer_8 (SEA (Message_Length_Size + 1))), (Unsigned_8 (SEA (Message_Length_Size + 1))),
To_PO_HI_Full_Stream (SEA) To_PO_HI_Full_Stream (SEA)
(1 .. Stream_Element_Offset (SEO))); (1 .. Stream_Element_Offset (SEO)));
end if; end if;
...@@ -361,24 +362,20 @@ package body PolyORB_HI.Transport_Low_Level is ...@@ -361,24 +362,20 @@ package body PolyORB_HI.Transport_Low_Level is
return Error_Kind return Error_Kind
is is
L : AS.Stream_Element_Offset; L : AS.Stream_Element_Offset;
pragma Unreferenced (L);
-- We cannot cast both array types using -- We cannot cast both array types using Unchecked_Conversion
-- Ada.Unchecked_Conversion because they are unconstrained -- because they are unconstrained types. We cannot either use
-- types. We cannot either use direct casting because component -- direct casting because component types are incompatible. The
-- types are incompatible. The only time efficient manner to do -- only time efficient manner to do the casting is to use
-- the casting is to use representation clauses. -- representation clauses.
Msg : AS.Stream_Element_Array (1 .. Message'Length); Msg : AS.Stream_Element_Array (1 .. Message'Length);
pragma Import (Ada, Msg); pragma Import (Ada, Msg);
for Msg'Address use Message'Address; for Msg'Address use Message'Address;
begin begin
pragma Warnings (Off); pragma Debug (Put_Line (Verbose, "Sending message, size:" & L'Img));
Send_Socket (Nodes (Node).Socket_Send, Send_Socket (Nodes (Node).Socket_Send, Msg, L);
Msg,
L);
-- WAG: GPL 2007
pragma Warnings (On);
return Error_Kind'(Error_None); return Error_Kind'(Error_None);
exception exception
when E : others => when E : others =>
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 2007-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. -- -- Copyright (C) 2007-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- -- -- --
-- PolyORB HI is free software; you can redistribute it and/or modify it -- -- PolyORB HI is free software; you can redistribute it and/or modify it --
-- under terms of the GNU General Public License as published by the Free -- -- under terms of the GNU General Public License as published by the Free --
...@@ -62,14 +62,14 @@ package PolyORB_HI.Utils is ...@@ -62,14 +62,14 @@ package PolyORB_HI.Utils is
-- 2) these converters must be endianness-independent -- 2) these converters must be endianness-independent
function Internal_Code is new Ada.Unchecked_Conversion function Internal_Code is new Ada.Unchecked_Conversion
(Entity_Type, Integer_8); (Entity_Type, Unsigned_8);
function Corresponding_Entity is new Ada.Unchecked_Conversion function Corresponding_Entity is new Ada.Unchecked_Conversion
(Integer_8, Entity_Type); (Unsigned_8, Entity_Type);
function Internal_Code is new Ada.Unchecked_Conversion function Internal_Code is new Ada.Unchecked_Conversion
(Node_Type, Integer_8); (Node_Type, Unsigned_8);
function Corresponding_Node is new Ada.Unchecked_Conversion function Corresponding_Node is new Ada.Unchecked_Conversion
(Integer_8, Node_Type); (Unsigned_8, Node_Type);
function Internal_Code (P : Port_Type) return Unsigned_16; function Internal_Code (P : Port_Type) return Unsigned_16;
function Corresponding_Port (I : Unsigned_16) return Port_Type; function Corresponding_Port (I : Unsigned_16) return Port_Type;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment