******************************************************* Listing of SPARK Text SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 24-MAR-2010 12:06:13.35 Line 1 ------------------------------------------------------------------ 2 -- Tokeneer ID Station Core Software 3 -- 4 -- Copyright (2003) United States Government, as represented 5 -- by the Director, National Security Agency. All rights reserved. 6 -- 7 -- This material was originally developed by Praxis High Integrity 8 -- Systems Ltd. under contract to the National Security Agency. 9 ------------------------------------------------------------------ 10 11 ------------------------------------------------------------------ 12 -- Clock 13 -- 14 -- Description: 15 -- Provides a "current time" for each system cycle. 16 -- 17 ------------------------------------------------------------------ 18 with BasicTypes; 19 20 -- # inherit Clock.Interface; -- notare lo spazio! 21 --# inherit BasicTypes; 22 23 package Clock 24 --# own CurrentTime; 25 --# in Now; 26 is 27 28 ------------------------------------------------------------------ 29 -- Types 30 -- 31 ------------------------------------------------------------------ 32 33 ------------------------------------------------------------------ 34 -- Time 35 -- 36 -- Description: 37 -- Internal representation of time. 38 -- 39 -- Traceunit : C.Clock.Time 40 -- Traceto : FD.Types.Time 41 ------------------------------------------------------------------ 42 type TimeT is private; 43 44 ZeroTime : constant TimeT; 45 46 type YearsT is range 1901 .. 2099; 47 type MonthsT is range 1 .. 12; 48 type DaysT is range 1 .. 31; 49 type HoursT is range 0 .. 23; 50 type MinutesT is range 0 .. 59; 51 ------------------------------------------------------------------ 52 -- Duration 53 -- 54 -- Description: 55 -- Duration in 1/10 seconds. 56 -- The range allows 24 hours to be represented. 57 ------------------------------------------------------------------ 58 type DurationT is range 0 .. 864000; 59 60 ------------------------------------------------------------------ 61 -- TimeText 62 -- DurationText 63 -- 64 -- Description: 65 -- Textual representation of time used in audit records. 66 -- Times are displayed as "yyyy-mm-dd hh:mm:ss.s" 67 -- Durations are displayed as "hh:mm:ss.s" 68 ------------------------------------------------------------------ 69 subtype TimeTextI is Positive range 1 .. 21; 70 subtype TimeTextT is String(TimeTextI); 71 72 subtype DurationTextI is Positive range 1 .. 10; 73 subtype DurationTextT is String(DurationTextI); 74 75 ------------------------------------------------------------------ 76 -- Poll 77 -- 78 -- Description: 79 -- Reads the system clock, and updates the internal CurrentTime. 80 -- 81 -- Traceunit: C.Clock.Poll 82 -- Traceto: FD.Interface.PollTime 83 ------------------------------------------------------------------ 84 85 procedure Poll; 86 --# global in Now; 87 --# out CurrentTime; 88 --# derives CurrentTime from Now; 89 90 ------------------------------------------------------------------ 91 -- TheCurrentTime 92 -- 93 -- Description: 94 -- Returns CurrentTime recorded at the last poll. 95 -- 96 -- Traceunit: C.Clock.TheCurrentTime 97 -- Traceto: FD.RealWorld.State 98 ------------------------------------------------------------------ 99 100 function TheCurrentTime return TimeT; 101 --# global CurrentTime; 102 103 ------------------------------------------------------------------ 104 -- GetNow 105 -- 106 -- Description: 107 -- Returns the system time now. 108 -- 109 -- Traceunit: C.Clock.GetNow 110 -- Traceto: FD.MonitoredRealWorld.State 111 ------------------------------------------------------------------ 112 113 function GetNow return TimeT; 114 --# global Now; 115 116 117 ------------------------------------------------------------------ 118 -- GreaterThan 119 -- 120 -- Description: 121 -- Boolean function implementing > on the private Type Time. 122 -- 123 -- Traceunit: C.Clock.GreaterThan 124 -- 125 ------------------------------------------------------------------ 126 127 function GreaterThan ( Left, Right : TimeT ) return Boolean; 128 129 ------------------------------------------------------------------ 130 -- LessThan 131 -- 132 -- Description: 133 -- Boolean function implementing < on the private Type Time. 134 -- 135 -- Traceunit: C.Clock.LessThan 136 -- 137 ------------------------------------------------------------------ 138 139 function LessThan ( Left, Right : TimeT ) return Boolean; 140 141 ------------------------------------------------------------------ 142 -- GreaterThanOrEqual 143 -- 144 -- Description: 145 -- Boolean function implementing >= on the private Type Time. 146 -- 147 -- Traceunit: C.Clock.GreaterThanOrEqual 148 -- 149 ------------------------------------------------------------------ 150 151 function GreaterThanOrEqual ( Left, Right : TimeT ) return Boolean; 152 153 ------------------------------------------------------------------ 154 -- LessThanOrEqual 155 -- 156 -- Description: 157 -- Boolean function implementing <= on the private Type Time. 158 -- 159 -- Traceunit: C.Clock.LessThanOrEqual 160 -- 161 ------------------------------------------------------------------ 162 163 function LessThanOrEqual ( Left, Right : TimeT ) return Boolean; 164 165 ------------------------------------------------------------------ 166 -- ConstructTime 167 -- 168 -- Description: 169 -- Constructs a time from raw constituent parts. If the time is not 170 -- valid then the Success flag is set to false. 171 -- 172 -- Traceunit: C.Clock.ConstructTime 173 -- 174 ------------------------------------------------------------------ 175 procedure ConstructTime 176 (Year : in BasicTypes.Unsigned32T; 177 Month : in BasicTypes.Unsigned32T; 178 Day : in BasicTypes.Unsigned32T; 179 Hour : in BasicTypes.Unsigned32T; 180 Min : in BasicTypes.Unsigned32T; 181 TheTime : out TimeT; 182 Success : out Boolean); 183 --# derives TheTime, 184 --# Success from Year, 185 --# Month, 186 --# Day, 187 --# Hour, 188 --# Min; 189 190 ------------------------------------------------------------------ 191 -- SplitTime 192 -- 193 -- Description: 194 -- Decomposes a time into its constituent parts. 195 -- 196 -- Traceunit: C.Clock.SplitTime 197 -- 198 ------------------------------------------------------------------ 199 procedure SplitTime 200 (TheTime : in TimeT; 201 Year : out YearsT; 202 Month : out MonthsT; 203 Day : out DaysT; 204 Hour : out HoursT; 205 Min : out MinutesT); 206 --# derives Year, 207 --# Month, 208 --# Day, 209 --# Hour, 210 --# Min from TheTime; 211 212 ------------------------------------------------------------------ 213 -- StartOfDay 214 -- 215 -- Description: 216 -- Converts the time to the start of the day. 217 -- 218 -- Traceunit: C.Clock.StartOfDay 219 -- 220 ------------------------------------------------------------------ 221 function StartOfDay (TheTime : TimeT) return TimeT; 222 223 ------------------------------------------------------------------ 224 -- PrintDuration 225 -- 226 -- Description: 227 -- Converts a duration to Text for display. 228 -- 229 -- Traceunit: C.Clock.PrintDuration 230 -- 231 ------------------------------------------------------------------ 232 function PrintDuration (TheDuration : DurationT ) return DurationTextT; 233 234 ------------------------------------------------------------------ 235 -- PrintTime 236 -- 237 -- Description: 238 -- Converts a time to Text for display. 239 -- 240 -- Traceunit: C.Clock.PrintText 241 -- 242 ------------------------------------------------------------------ 243 function PrintTime (TheTime : TimeT ) return TimeTextT; 244 245 ------------------------------------------------------------------ 246 -- AddDuration 247 -- 248 -- Description: 249 -- Adds a duration to a time. 250 -- 251 -- Traceunit: C.Clock.AddDuration 252 -- 253 ------------------------------------------------------------------ 254 function AddDuration 255 (TheTime : TimeT; TheDuration : DurationT ) return TimeT; 256 257 private 258 259 MilliSecsInTenthSec : constant := 100; 260 MilliSecsInSec : constant := 1000; 261 262 type MilliSecsT is range 0 .. DurationT'Last * MilliSecsInTenthSec - 1 ; 263 264 type TimeT is record 265 Year : YearsT; 266 Month : MonthsT; 267 Day : DaysT; 268 MilliSec : MilliSecsT; 269 end record; 270 271 ZeroTime : constant TimeT := 272 TimeT'(Year => YearsT'First, 273 Month => MonthsT'First, 274 Day => DaysT'First, 275 MilliSec => MilliSecsT'First); 276 277 278 end Clock; 279 280 281 282 283 284 --End of file--------------------------------------------------