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

Line
   1  package body Time
   2  is
   3  
   4     ------------------------------------------------------------------
   5     -- Types and constants
   6     --
   7     ------------------------------------------------------------------
   8        MilliSecsInMin : constant := 60 * MilliSecsInSec;
   9        MilliSecsInHr : constant := 60 * MilliSecsInMin;
  10  
  11     ------------------------------------------------------------------
  12     -- Private Operations
  13     ------------------------------------------------------------------
  14  
  15     ------------------------------------------------------------------
  16     -- SetStringSegment
  17     --
  18     -- Definition:
  19     --    Sets the section of the string S from SStart to SEnd with
  20     --    the String representation of the Value.
  21     --    Pads to the left with '0'.
  22     --    Truncates if Value is too big to fit.
  23     --
  24     -- Implementation Notes:
  25     --    None.
  26     --
  27     ------------------------------------------------------------------
  28     procedure SetStringSegment
  29       ( S      : in out String;
  30         Value  : in     Natural;
  31         SStart : in     Positive;
  32         SEnd   : in     Positive)
  33     --# derives S from *,
  34     --#                Value,
  35     --#                SEnd,
  36     --#                SStart;
  37     --# pre S'Last >= SEnd and S'First <= SStart;
  38     is
  39        V : Natural;
  40     begin
  41  
  42        V := Value;
  43  
  44        for I in reverse Positive range SStart .. SEnd loop
  45           --# assert I <= SEnd and I >= SStart
  46           --#        and I <= S'Last and I >= S'First
  47           --#        and V in Natural ;
  48           S(I) := Character'Val(Character'Pos('0') + (V mod 10));
  49           V    := V / 10;
  50        end loop;
  51  
  52     end SetStringSegment;

+++        Flow analysis of subprogram SetStringSegment 
           performed: no errors found.

  53  
  54        ------------------------------------------------------------------
  55     -- GreaterThan
  56     --
  57     -- Implementation Notes:
  58     --    None.
  59     --
  60     ------------------------------------------------------------------
  61  
  62     function GreaterThan ( Left, Right : T ) return Boolean
  63     is
  64     begin
  65        return Left.Year > Right.Year
  66          or (Left.Year = Right.Year
  67              and Left.Month > Right.Month )
  68          or (Left.Year = Right.Year
  69              and Left.Month = Right.Month
  70              and Left.Day > Right.Day)
  71          or (Left.Year = Right.Year
  72              and Left.Month = Right.Month
  73              and Left.Day = Right.Day
  74              and Left.MilliSec > Right.MilliSec);
  75     end GreaterThan;

+++        Flow analysis of subprogram GreaterThan 
           performed: no errors found.

  76  
  77     ------------------------------------------------------------------
  78     -- LessThan
  79     --
  80     -- Implementation Notes:
  81     --    None.
  82     --
  83     ------------------------------------------------------------------
  84  
  85     function LessThan ( Left, Right : T ) return Boolean
  86     is
  87     begin
  88        return Left.Year < Right.Year
  89          or (Left.Year = Right.Year
  90              and Left.Month < Right.Month )
  91          or (Left.Year = Right.Year
  92              and Left.Month = Right.Month
  93              and Left.Day < Right.Day)
  94          or (Left.Year= Right.Year
  95              and Left.Month = Right.Month
  96              and Left.Day = Right.Day
  97              and Left.MilliSec < Right.MilliSec);
  98     end LessThan;

+++        Flow analysis of subprogram LessThan performed: 
           no errors found.

  99  
 100     ------------------------------------------------------------------
 101     -- GreaterThanOrEqual
 102     --
 103     -- Implemention Notes:
 104     --    None.
 105     --
 106     ------------------------------------------------------------------
 107  
 108     function GreaterThanOrEqual ( Left, Right : T ) return Boolean
 109     is
 110     begin
 111         return GreaterThan (Left, Right) or Left = Right;
 112     end GreaterThanOrEqual;

+++        Flow analysis of subprogram GreaterThanOrEqual 
           performed: no errors found.

 113  
 114     ------------------------------------------------------------------
 115     -- LessThanOrEqual
 116     --
 117     -- Implemention Notes:
 118     --    None.
 119     --
 120     ------------------------------------------------------------------
 121  
 122     function LessThanOrEqual ( Left, Right : T ) return Boolean
 123     is
 124     begin
 125         return LessThan (Left, Right) or Left = Right;
 126     end LessThanOrEqual;

+++        Flow analysis of subprogram LessThanOrEqual 
           performed: no errors found.

 127  
 128  
 129  
 130     ------------------------------------------------------------------
 131     -- SplitTime
 132     --
 133     -- Implementation Notes:
 134     --    This always rounds down.
 135     --
 136     ------------------------------------------------------------------
 137     procedure SplitTime
 138       (TheTime : in     T;
 139        Year    :    out YearsT;
 140        Month   :    out MonthsT;
 141        Day     :    out DaysT;
 142        Hour    :    out HoursT;
 143        Min     :    out MinutesT)
 144     is
 145  
 146     begin
 147        Year  := TheTime.Year;
 148        Month := TheTime.Month;
 149        Day   := TheTime.Day;
 150        Hour  := HoursT (TheTime.MilliSec / MilliSecsInHr);
 151        Min   := MinutesT ((TheTime.MilliSec mod MilliSecsInHr )
 152                          / MilliSecsInMin);
 153     end SplitTime;

+++        Flow analysis of subprogram SplitTime performed: 
           no errors found.

 154  
 155     ------------------------------------------------------------------
 156     -- StartOfDay
 157     --
 158     -- Implementation Notes:
 159     --    None.
 160     --
 161     ------------------------------------------------------------------
 162     function StartOfDay (TheTime : T) return T
 163     is
 164     begin
 165        return T'(Year => TheTime.Year,
 166                      Month => TheTime.Month,
 167                      Day => TheTime.Day,
 168                      MilliSec => MilliSecsT'First);
 169     end StartOfDay;

+++        Flow analysis of subprogram StartOfDay 
           performed: no errors found.

 170  
 171  
 172     ------------------------------------------------------------------
 173     -- PrintDuration
 174     --
 175     -- Implementation Notes:
 176     --    None.
 177     --
 178     ------------------------------------------------------------------
 179     function PrintDuration (TheDuration : DurationT ) return DurationTextT
 180     is
 181        LocalText : DurationTextT := "hh:mm:ss.s";
 182        FirstHourIndex    : constant TextI := 1;
 183        LastHourIndex     : constant TextI := 2;
 184  
 185        FirstMinIndex     : constant TextI := 4;
 186        LastMinIndex      : constant TextI := 5;
 187  
 188        FirstSecIndex     : constant TextI := 7;
 189        LastSecIndex      : constant TextI := 8;
 190  
 191        TenthSecIndex     : constant TextI := 10;
 192  
 193        TenthSecsInSec     : constant := 10;
 194        TenthSecsInMin     : constant := 60 * TenthSecsInSec;
 195        TenthSecsInHr      : constant := 60 * TenthSecsInMin;
 196     begin
 197  
 198        SetStringSegment(LocalText,
 199                         Natural(TheDuration / TenthSecsInHr),
 200                         FirstHourIndex,
 201                         LastHourIndex);
 202  
 203        SetStringSegment(LocalText,
 204                         Natural((TheDuration mod TenthSecsInHr)
 205                                 / TenthSecsInMin),
 206                         FirstMinIndex,
 207                         LastMinIndex);
 208  
 209        SetStringSegment(LocalText,
 210                         Natural((TheDuration mod TenthSecsInMin)
 211                                 / TenthSecsInSec),
 212                         FirstSecIndex,
 213                         LastSecIndex);
 214  
 215        SetStringSegment(LocalText,
 216                         Natural(TheDuration mod TenthSecsInSec),
 217                         TenthSecIndex,
 218                         TenthSecIndex);
 219  
 220        return LocalText;
 221     end PrintDuration;

+++        Flow analysis of subprogram PrintDuration 
           performed: no errors found.

 222  
 223     ------------------------------------------------------------------
 224     -- PrintTime
 225     --
 226     -- Implementation Notes:
 227     --    None.
 228     --
 229     ------------------------------------------------------------------
 230     function PrintTime (TheTime : T ) return TextT
 231     is
 232        LocalText : TextT := "yyyy-mm-dd hh:mm:ss.s";
 233  
 234        FirstYearIndex    : constant TextI := 1;
 235        LastYearIndex     : constant TextI := 4;
 236  
 237        FirstMonthIndex   : constant TextI := 6;
 238        LastMonthIndex    : constant TextI := 7;
 239  
 240        FirstDayIndex     : constant TextI := 9;
 241        LastDayIndex      : constant TextI := 10;
 242  
 243        FirstHourIndex    : constant TextI := 12;
 244        LastHourIndex     : constant TextI := 13;
 245  
 246        FirstMinIndex     : constant TextI := 15;
 247        LastMinIndex      : constant TextI := 16;
 248  
 249        FirstSecIndex     : constant TextI := 18;
 250        LastSecIndex      : constant TextI := 19;
 251  
 252        TenthSecIndex     : constant TextI := 21;
 253  
 254     begin
 255        --# assert LocalText'First = TextI'First and
 256        --#        LocalText'Last = TextI'Last;
 257  
 258        SetStringSegment(LocalText,
 259                         Natural(TheTime.Year),
 260                         FirstYearIndex,
 261                         LastYearIndex);
 262  
 263        SetStringSegment(LocalText,
 264                         Natural(TheTime.Month),
 265                         FirstMonthIndex,
 266                         LastMonthIndex);
 267  
 268        SetStringSegment(LocalText,
 269                         Natural(TheTime.Day),
 270                         FirstDayIndex,
 271                         LastDayIndex);
 272  
 273        SetStringSegment(LocalText,
 274                         Natural(TheTime.MilliSec / MilliSecsInHr),
 275                         FirstHourIndex,
 276                         LastHourIndex);
 277  
 278        SetStringSegment(LocalText,
 279                         Natural((TheTime.MilliSec mod MilliSecsInHr)
 280                                 / MilliSecsInMin),
 281                         FirstMinIndex,
 282                         LastMinIndex);
 283  
 284        SetStringSegment(LocalText,
 285                         Natural((TheTime.MilliSec mod MilliSecsInMin)
 286                                 / MilliSecsInSec),
 287                         FirstSecIndex,
 288                         LastSecIndex);
 289  
 290        SetStringSegment(LocalText,
 291                         Natural((TheTime.MilliSec mod MilliSecsInSec)
 292                                 / MilliSecsInTenthSec),
 293                         TenthSecIndex,
 294                         TenthSecIndex);
 295  
 296        return LocalText;
 297     end PrintTime;

+++        Flow analysis of subprogram PrintTime performed: 
           no errors found.

 298  
 299  end Time;
No summarized warnings



--End of file--------------------------------------------------