Commit 493f2900 authored by yoogx's avatar yoogx

* Partial proofs using GNATProve GPL2014

parent 4503f49b
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- 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 --
......@@ -61,7 +61,9 @@ package body PolyORB_HI.Messages is
Receiver_Offset : constant Stream_Element_Offset := Message_Length_Size + 1;
Sender_Offset : constant Stream_Element_Offset := Message_Length_Size + 2;
function Length (M : Message_Type) return PDU_Index;
function Length (M : Message_Type) return PDU_Index is
(M.Last - M.First + 1)
with Pre => (Valid (M));
-- Return length of message M
-----------------
......@@ -75,50 +77,23 @@ package body PolyORB_HI.Messages is
return Stream_Element_Array
is
L : constant Stream_Element_Count := Message.Last + Header_Size;
R : Stream_Element_Array (1 .. L);
R : Stream_Element_Array (1 .. L) := (others => 0);
P : constant Stream_Element_Array (1 .. Length (Message))
:= Payload (Message);
begin
R (1 .. Message_Length_Size) := To_Buffer (L - 1);
R (Receiver_Offset) := Stream_Element (Internal_Code (Entity));
R (Sender_Offset) := Stream_Element (Internal_Code (From));
R (Header_Size + 1 .. Header_Size + Message.Last)
:= Message.Content (Message.First .. Message.Last);
R (Header_Size + 1 .. Header_Size + Length (Message)) := P;
-- XXX GNATProve GPL 2014 limitation ?
return R;
end Encapsulate;
------------
-- Length --
------------
function Length (M : Message_Type) return PDU_Index is
begin
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;
-------------
-- Payload --
-------------
function Payload (M : Message_Type) return Stream_Element_Array is
begin
return M.Content (M.First .. M.Last);
end Payload;
------------
-- Sender --
------------
function Sender (M : Message_Type) return Entity_Type is
begin
return Sender (M.Content (M.First .. M.Last));
end Sender;
function Sender (M : Stream_Element_Array) return Entity_Type is
begin
return Corresponding_Entity (Unsigned_8 (M (Sender_Offset)));
......@@ -136,6 +111,8 @@ package body PolyORB_HI.Messages is
Read_Elts : constant Stream_Element_Count
:= Stream_Element_Count'Min (Item'Length, Length (Stream));
begin
Item := (others => 0);
if Read_Elts < 1 then
-- We have nothing to read, exit
Last := 0;
......@@ -176,10 +153,9 @@ package body PolyORB_HI.Messages is
is
begin
if Stream.First > Stream.Last then
Reallocate (Stream);
-- The message is invalid, we reset it
Stream.First := 1;
Stream.Last := 0;
-- XXX Do we need to do that ???
end if;
if Item'Length <= Stream.Content'Last - Stream.Last then
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- 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 --
......@@ -61,13 +61,15 @@ package PolyORB_HI.Messages is
-- The sub-buffer that holds the message length
function To_Length (B : Message_Size_Buffer) return Stream_Element_Count;
function To_Buffer (L : Stream_Element_Count) return Message_Size_Buffer;
function To_Buffer (L : Stream_Element_Count) return Message_Size_Buffer
with Pre => (L < 2**16 -1); -- XXX Provide a better bound for L
-- Conversion functions to store/extract a length in/from a sub-buffer.
procedure Read
(Stream : in out Message_Type;
Item : out Stream_Element_Array;
Last : out Stream_Element_Offset);
Last : out Stream_Element_Offset)
with Pre => (Valid (Stream));
-- Move Item'Length stream elements from the specified stream to
-- fill the array Item. The index of the last stream element
-- transferred is returned in Last. Last is less than Item'Last
......@@ -75,16 +77,19 @@ package PolyORB_HI.Messages is
procedure Write
(Stream : in out Message_Type;
Item : Stream_Element_Array);
Item : Stream_Element_Array)
with Pre => (Valid (Stream));
-- Append Item to the specified stream
procedure Reallocate (M : in out Message_Type);
-- Reset M
function Payload (M : Message_Type) return Stream_Element_Array;
function Payload (M : Message_Type) return Stream_Element_Array
with Pre => (Valid (M));
-- Return the remaining payload of message M
function Sender (M : Message_Type) return Entity_Type;
function Sender (M : Message_Type) return Entity_Type
with Pre => (Valid (M));
function Sender (M : Stream_Element_Array) return Entity_Type;
-- Return the sender of the message M
......@@ -92,21 +97,36 @@ package PolyORB_HI.Messages is
(Message : Message_Type;
From : Entity_Type;
Entity : Entity_Type)
return Stream_Element_Array;
return Stream_Element_Array
with Pre => (Valid (Message));
-- Return a byte array including a two byte header (length and
-- originator entity) and Message payload.
function Valid (Message : Message_Type) return Boolean;
private
subtype PDU_Index is Stream_Element_Count range 0 .. PDU_Size;
subtype PDU is Stream_Element_Array (1 .. PDU_Index'Last);
Empty_PDU : constant PDU := (others => 0);
type Message_Type is record
Content : PDU;
Content : PDU := Empty_PDU;
First : PDU_Index := 1;
Last : PDU_Index := 0;
end record;
function Valid (Message : Message_Type) return Boolean is
(Message.First >= Message.Content'First and then Message.First < Message.Last
and then Message.Last <= Message.Content'Last);
function Payload (M : Message_Type) return Stream_Element_Array is
(M.Content (M.First .. M.Last));
function Sender (M : Message_Type) return Entity_Type is
(Sender (Payload (M)));
pragma Inline (To_Length);
pragma Inline (To_Buffer);
......
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