******************************************************* Listing of SPARK Text SPARK Examiner GPL Edition, Version 8.1.1, Build Date 20090505, Build 13202 Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K. ******************************************************* DATE : 15-APR-2010 10:29:08.68 Line 1 with Ada.Calendar; 2 package body Time.Interface 3 is --# hide Time.Interface; 4 5 function GetNow return T 6 is 7 T : Ada.Calendar.Time := Ada.Calendar.Clock; 8 9 Year : Ada.Calendar.Year_Number; 10 Month : Ada.Calendar.Month_Number; 11 Day : Ada.Calendar.Day_Number; 12 Sec : Duration; 13 14 Ret : Time.T; 15 16 begin 17 Ada.Calendar.Split 18 (Date => T, 19 Year => Year, 20 Month => Month, 21 Day => Day, 22 Seconds => Sec); 23 24 -- -- force truncating not rounding to ensure MilliSec doesn't overflow 25 -- if Sec > 0.0005 then -- ? che vuol dire ? 26 -- Sec := Sec - 0.0005; 27 -- end if; 28 Ret := Time.T'(Year => YearsT(Year), 29 Month => MonthsT(Month), 30 Day => DaysT(Day), 31 MilliSec => MilliSecsT(Sec) * MilliSecsInSec); 32 return Ret; 33 end GetNow; 34 35 function ValidTimeData 36 (Year : in BasicTypes.Unsigned32T; 37 Month : in BasicTypes.Unsigned32T; 38 Day : in BasicTypes.Unsigned32T; 39 TimeOfDay : in DurationT) return Boolean 40 is 41 TheTime : Ada.Calendar.Time ; 42 begin 43 TheTime := 44 Ada.Calendar.Time_Of 45 (Year => Ada.Calendar.Year_Number(Year), 46 Month => Ada.Calendar.Month_Number(Month), 47 Day => Ada.Calendar.Day_Number(Day), 48 Seconds => Ada.Calendar.Day_Duration( Duration(TimeOfDay) / 1000)); 49 50 return True; 51 52 exception when Ada.Calendar.Time_Error => 53 return False; 54 end ValidTimeData; 55 56 ------------------------------------------------------------------ 57 -- ConstructTimeFromDuration 58 -- 59 -- Implementation Notes: 60 -- None. 61 -- 62 ------------------------------------------------------------------ 63 procedure ConstructTimeFromDuration 64 (Year : in BasicTypes.Unsigned32T; 65 Month : in BasicTypes.Unsigned32T; 66 Day : in BasicTypes.Unsigned32T; 67 TimeOfDay : in DurationT; 68 TheTime : out T; 69 Success : out Boolean) 70 71 is 72 begin 73 if Interface.ValidTimeData(Year, Month, Day, TimeOfDay) then 74 TheTime := T'(Year => YearsT(Year), 75 Month => MonthsT(Month), 76 Day => DaysT(Day), 77 MilliSec => MilliSecsT(TimeOfDay*MilliSecsInTenthSec)); 78 Success := True; 79 else 80 TheTime := ZeroTime; 81 Success := False; 82 end if; 83 end ConstructTimeFromDuration; 84 ------------------------------------------------------------------ 85 -- AddDuration 86 -- 87 -- Implementation Notes: 88 -- None. 89 -- 90 ------------------------------------------------------------------ 91 -- function AddDuration 92 -- (TheTime : T; TheDuration : DurationT ) return T 93 -- is 94 -- begin 95 -- return SparkInterface.AddDuration(TheTime, TheDuration); 96 end Time.Interface; 5 summarized warning(s), comprising: 1 hidden part(s)* 1 with clause(s) lacking a supporting inherit 3 use(s) of Ada2005 reserved words (*Note: the above warnings may affect the validity of the analysis.) --End of file--------------------------------------------------