with Interfaces.C;
package Messages
with Spark_Mode => On
is
type Node_Id_Type is new Interfaces.C.unsigned_short;
type Sequence_Number_Type is new Interfaces.C.unsigned_long;
function Compute_Fletcher_Checksum
(Buffer : in Interfaces.C.char_array;
Size : in Interfaces.C.size_t) return Interfaces.C.unsigned_short
with
Global => null,
Import => True,
Convention => C,
Pre => Size = Buffer'Length,
External_Name => "compute_fletcher_checksum";
type Packet_Header_Type is
record
Source_Node : Node_Id_Type;
Destination_Node : Node_Id_Type;
Sequence_Number : Sequence_Number_Type;
end record
with Convention => C;
type Error_Code is (Success, Invalid_Destination, Insufficient_Space)
with Convention => C;
for Error_Code use (1, 2, 3);
-- function Install_Header
-- (Buffer : in out Interfaces.C.char_array;
-- Size : in Interfaces.C.size_t;
-- Header : in Packet_Header_Type) return Error_Code
-- with
-- Global => null,
-- Import => True,
-- Convention => C,
-- External_Name => "install_header";
-- Needed to make operators used in postcondition directly visible.
use type Interfaces.C.size_t;
use type Interfaces.C.char;
use type Interfaces.C.char_array;
procedure Install_Header (Buffer : in out Interfaces.C.char_array;
Size : in Interfaces.C.size_t;
Header : in Packet_Header_Type;
Status : out Error_Code)
with
Global => null,
Depends => (Buffer =>+ (Size, Header), Status => (Size, Header)),
Post => (if Status /= Success then
Buffer = Buffer'Old
else
(for all J in Buffer'First + 12 .. Buffer'Last =>
Buffer(J) = Buffer'Old (J))),
Import => True,
Convention => C,
External_Name => "install_header_helper";
end Messages;