gnatprove_13.2.1_28fc3583/share/examples/spark/tokeneer/alarmapi.adb

 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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
------------------------------------------------------------------
-- Tokeneer ID Station Support Software
--
-- Copyright (2003) United States Government, as represented
-- by the Director, National Security Agency.All rights reserved.
--
-- This material was originally developed by Praxis High Integrity
-- Systems Ltd.under contract to the National Security Agency.
------------------------------------------------------------------

------------------------------------------------------------------
-- AlarmAPI
--
-- Implementation Notes:
--    None
--
------------------------------------------------------------------
with TcpIp;
with MsgProc;
with Ada.Strings.Fixed;

package body AlarmAPI
  with SPARK_Mode => On
is

   ------------------------------------------------------------------
   -- Activate
   --
   -- Implementation Notes:
   --    Don't check whether alarm is activated or not.
   --
   ------------------------------------------------------------------
   procedure Activate
   is
      InMsg     : TcpIp.MessageT;
      OutMsg    : constant TcpIp.MessageT :=
        (Data   =>
           Ada.Strings.Fixed.Overwrite(Source   => TcpIp.NullMsg.Data,
                                       Position => 1,
                                       New_Item => "alarm.activate()"),
         Length => 16);



      CommsIsOK : Boolean;
   begin
      TcpIp.SendAndReceive (IsAdmin  => True,
                            Outgoing => OutMsg,
                            Incoming => InMsg,
                            Success  => CommsIsOk);
   end Activate;

   ------------------------------------------------------------------
   -- Deactivate
   --
   -- Implementation Notes:
   --    Don't check whether alarm is deactivated or not.
   --
   ------------------------------------------------------------------
   procedure Deactivate
   is
      InMsg     : TcpIp.MessageT;
      OutMsg    : constant TcpIp.MessageT :=
        (Data   =>
           Ada.Strings.Fixed.Overwrite(Source   => TcpIp.NullMsg.Data,
                                       Position => 1,
                                       New_Item => "alarm.deactivate()"),
         Length => 18);



      CommsIsOK : Boolean;
   begin
      TcpIp.SendAndReceive (IsAdmin  => True,
                            Outgoing => OutMsg,
                            Incoming => InMsg,
                            Success  => CommsIsOk);
   end Deactivate;

end AlarmAPI;