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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123 | ------------------------------------------------------------------
-- Tokeneer ID Station Core 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.
------------------------------------------------------------------
------------------------------------------------------------------
-- Clock.Interfac
--
-- Description:
-- Interfac to the system clock.
--
-- Implementation Notes:
-- This packge body is not presented to the SPARK Examiner.
------------------------------------------------------------------
with Ada.Calendar;
use Ada.Calendar;
package body Clock.Interfac
with SPARK_Mode => Off
is
------------------------------------------------------------------
-- Convert
--
-- Description:
-- Converts Calendar.Time to Clock.TimeT
--
-- Implementation Notes:
-- None.
--
------------------------------------------------------------------
function Convert (T : Ada.Calendar.Time) return Clock.TimeT is
Year : Ada.Calendar.Year_Number;
Month : Ada.Calendar.Month_Number;
Day : Ada.Calendar.Day_Number;
Sec : Duration;
begin
Ada.Calendar.Split
(Date => T,
Year => Year,
Month => Month,
Day => Day,
Seconds => Sec);
-- force truncating not rounding to ensure MilliSec doesn't overflow
if Sec > 0.0005 then
Sec := Sec - 0.0005;
end if;
return Clock.TimeT'
(Year => Clock.YearsT(Year),
Month => Clock.MonthsT(Month),
Day => Clock.DaysT(Day),
MilliSec => Clock.MillisecsT(Sec * Clock.MilliSecsInSec));
end Convert;
------------------------------------------------------------------
-- TheTime
--
-- Implementation Notes:
-- None.
--
------------------------------------------------------------------
function TheTime return Clock.TimeT is (Convert (Ada.Calendar.Clock));
------------------------------------------------------------------
-- AddDuration
--
-- Implementation Notes:
-- If the time is not valid the duration is not added.
-- If the addition causes an overflow then the duration is not added.
--
------------------------------------------------------------------
function AddDuration (T : Clock.TimeT ; D : Clock.DurationT)
return Clock.TimeT
is
LocalTime : Ada.Calendar.Time;
begin
LocalTime := (Duration(D) / 10) +
Ada.Calendar.Time_Of
(Year => Ada.Calendar.Year_Number(T.Year),
Month => Ada.Calendar.Month_Number(T.Month),
Day => Ada.Calendar.Day_Number(T.Day),
Seconds => Ada.Calendar.Day_Duration
(Duration(T.MilliSec) / 1000));
return Convert(LocalTime);
exception
when Ada.Calendar.Time_Error =>
return T;
end AddDuration;
------------------------------------------------------------------
-- IsValidTime
--
-- Description:
-- If the time can be converted to a system time then it is valid.
--
------------------------------------------------------------------
function IsValidTime (T : Clock.TimeT) return Boolean is
LocalTime : Ada.Calendar.Time;
begin
LocalTime :=
Ada.Calendar.Time_Of
(Year => Ada.Calendar.Year_Number(T.Year),
Month => Ada.Calendar.Month_Number(T.Month),
Day => Ada.Calendar.Day_Number(T.Day),
Seconds => Ada.Calendar.Day_Duration( Duration(T.MilliSec) / 1000));
return True;
exception
when Ada.Calendar.Time_Error =>
return False;
end IsValidTime;
end Clock.Interfac;
|