*******************************************************
                            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--------------------------------------------------