/
doorapi.adb
99 lines (86 loc) · 3.02 KB
/
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;