gnatprove_11.2.3_f7ece6d3/share/examples/spark/spark_book/Chapter-07/messages.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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;