gnatprove_13.2.1_28fc3583/share/examples/spark/tokeneer/doorapi.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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
------------------------------------------------------------------
-- 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.
------------------------------------------------------------------

------------------------------------------------------------------
-- DoorAPI
--
-- Implementation Notes:
--    None.
--
------------------------------------------------------------------

with Ada.Strings.Fixed;
with TcpIp;
with MsgProc;

package body DoorAPI is

   function GetDoorStateRaw return DoorStateT
     with Global => null;
   --  Same as GetDoorState, compatible with SPARK (no exception handler)

   function GetDoorStateRaw return DoorStateT is
      InMsg     : TcpIp.MessageT;
      OutMsg    : constant TcpIp.MessageT :=
        (Data   =>
           Ada.Strings.Fixed.Overwrite(Source   => TcpIp.NullMsg.Data,
                                       Position => 1,
                                       New_Item => "door.getState()"),
         Length => 15);



      DoorState : DoorStateT := Error;
      IsOp,
      IsClosed,
      CommsIsOK : Boolean;
   begin
      TcpIp.SendAndReceive
        (IsAdmin  => False,
         Outgoing => OutMsg,
         Incoming => InMsg,
         Success  => CommsIsOK);

      if CommsIsOK then
         declare
            Msg       : String := MsgProc.GetResponseFromMsg (InMsg);
            StateDict : MsgProc.DictionaryT :=
               MsgProc.GetDictionary (Msg => Msg, Arg => 1);
         begin
            IsOp := Boolean'Value
              (MsgProc.GetStringByKey
                (Dic => StateDict, Key => "operational?"));
            pragma Annotate (GNATprove, Intentional,
                             "precondition might fail",
                             "Malformed input should trigger an exception here");
            IsClosed := Boolean'Value
              (MsgProc.GetStringByKey (Dic => StateDict, Key => "closed?"));
            pragma Annotate (GNATprove, Intentional,
                             "precondition might fail",
                             "Malformed input should trigger an exception here");
         end;

         if IsOp then
            if IsClosed then
               DoorState := Closed;
            else
               DoorState := Open;
            end if;
         end if;
      end if;

      return DoorState;
   end GetDoorStateRaw;

   ------------------------------------------------------------------
   -- GetDoorState
   --
   -- Implementation Notes:
   --    Set return value to Error if door state cannot be determined.
   --
   ------------------------------------------------------------------
   function GetDoorState return DoorStateT
     with SPARK_Mode => Off  --  exception handlers
   is
   begin
      return GetDoorStateRaw;
   exception
      when others =>
         return Error;
   end GetDoorState;

end DoorAPI;