gnat_riscv64_elf_11.2.4_f4a370b5/riscv64-elf/lib/gnat/ravenscar-full-unleashed/gnat/a-calend.ads

  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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
------------------------------------------------------------------------------
--                                                                          --
--                         GNAT RUN-TIME COMPONENTS                         --
--                                                                          --
--                         A D A . C A L E N D A R                          --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--                     Copyright (C) 2004-2020, AdaCore                     --
--                                                                          --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the  contents of the part following the private keyword. --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
--                                                                          --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception,   --
-- version 3.1, as published by the Free Software Foundation.               --
--                                                                          --
-- You should have received a copy of the GNU General Public License and    --
-- a copy of the GCC Runtime Library Exception along with this program;     --
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
-- <http://www.gnu.org/licenses/>.                                          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

--  This is the cert and bare metal Ravenscar runtime version of this package

--  This version assumes type Duration is represented in 64-bits.

--  RQ 0: Provide the language-defined library package Ada.Calendar.

--  RQ 1: Provide the specification of the Ada.Calendar package.

package Ada.Calendar with
  SPARK_Mode,
  Abstract_State => (Clock_Time with Synchronous),
  Initializes    => Clock_Time
is

   type Time is private;
   --  RQ 1-1: Time must allow representation of any point in time between
   --  January 1st 1901 and December 31st 2099 with the precision of at
   --  least System.Tick seconds.
   --
   --  Note: Time type is represented as a Modified Julian Day Number (MJDN).
   --  MJDN is a number of days elapsed since midnight of November 16th/17th,
   --  1858, so day 0 in the system of MJDN is the day 17th November 1858.

   --  Declarations representing limits of allowed local time values. Note that
   --  these do NOT constrain the possible stored values of time which may well
   --  permit a larger range of times (this is explicitly allowed in Ada 95).

   subtype Year_Number  is Integer range 1901 .. 2099;
   subtype Month_Number is Integer range 1 .. 12;
   subtype Day_Number   is Integer range 1 .. 31;

   subtype Day_Duration is Duration range 0.0 .. 86_400.0;

   function Clock return Time with
     Volatile_Function,
     Global => Clock_Time;
   --  RQ 2.9: This function shall return the current time in days which
   --  elapsed since 17'th November 1858.

   function Year    (Date : Time) return Year_Number;
   --  RQ 2.19: This function shall return year of the specified time.

   function Month   (Date : Time) return Month_Number;
   --  RQ 2.11: This function shall return month of the specified time.

   function Day     (Date : Time) return Day_Number;
   --  RQ 2.10: This function shall return day of the specified time.

   function Seconds (Date : Time) return Day_Duration;
   --  RQ 2.12: This function shall return seconds of the specified time.

   procedure Split
     (Date    : Time;
      Year    : out Year_Number;
      Month   : out Month_Number;
      Day     : out Day_Number;
      Seconds : out Day_Duration);
   --  RQ 2.13: This function shall get a Gregorian date (year number, month
   --  number, day number and duration) corresponding to the specified value
   --  of the Time type.
   --  Note: Algorithm used to convert modified Julian day number to Gregorian
   --  date has been adopted from the one described by the Jean Meeus in
   --  "Astronomical Algorithms" p. 63-4.

   function Time_Of
     (Year    : Year_Number;
      Month   : Month_Number;
      Day     : Day_Number;
      Seconds : Day_Duration := 0.0)
     return    Time;
   --  RQ 2.14: This function shall convert the specified Greogorian date into
   --  a value of type Time.
   --  RQ 2.14.1: If the specified values do not represent a valid Gregorian
   --  calendar date, then raise the Time_Error.

   function "+" (Left : Time;     Right : Duration) return Time;
   --  RQ 2.1: This function shall add the specified duration to the given
   --  point in time.
   --  RQ 2.1-1: If the result is not representable in the type Time, then
   --  raise the Time_Error.

   function "+" (Left : Duration; Right : Time)     return Time;
   --  RQ 2.2: This function shall add the specified duration to the given
   --  point in time.
   --  RQ 2.2-1: If the result is not representable in the type Time, then
   --  raise the Time_Error.

   function "-" (Left : Time;     Right : Duration) return Time;
   --  RQ 2.3: This function shall subtract the specified duration from the
   --  given point in time.
   --  RQ 2.3-1: If the result is not representable in the type Time, then
   --  raise the Time_Error.

   function "-" (Left : Time;     Right : Time)     return Duration;
   --  RQ 2.4: This function shall determine the amount of time which elapsed
   --  since <Left> point in time till <Right>.
   --  RQ 2.4-1: If the result is not representable in the type Duration, then
   --  raise the Time_Error.

   function "<"  (Left, Right : Time) return Boolean;
   --  RQ 2.5: This function shall return True if the <Left> point in time is
   --  before the <Right> point in time, False otherwise.

   function "<=" (Left, Right : Time) return Boolean;
   --  RQ 2.6: This function shall return True if both times are equal or the
   --  <Left> point in time is before the <Right> point in time, False
   --  otherwise.

   function ">"  (Left, Right : Time) return Boolean;
   --  RQ 2.7: This function shall return True if the <Left> point in time is
   --  after the <Right> point in time, False otherwise.

   function ">=" (Left, Right : Time) return Boolean;
   --  RQ 2.8: This function shall return True if both times are equal or the
   --  <Left> point in time is after the <Right> point in time, False
   --  otherwise.

   Time_Error : exception;

private
   pragma SPARK_Mode (Off);

   pragma Inline (Year);
   pragma Inline (Month);
   pragma Inline (Day);

   pragma Inline ("<");
   pragma Inline ("<=");
   pragma Inline (">");
   pragma Inline (">=");

   --  Time is represented as a Modified Julian Day number plus fraction of a
   --  day within the range of dates defined for Ada.Calendar.Time.  The small
   --  of the type preserves the precision of type Duration (64 bits).

   --  We introduce type Modified_Julian_Day so that expressions will be
   --  cleaner when we want the operations from Standard as opposed to those
   --  defined in Ada.Calendar on type Time.

   --  The Julian Day approach simplifies Time_Of and Split substantially, as
   --  well as being well-known algorithms.  The use of the Modified Julian Day
   --  number allows us to preserve the precision of type Duration.

   --  Time zones are not supported in this implementation

   --  Modified Julian Day.  The range is exactly that of the dates supported
   --  within the constraints on the components that make up a date.

   type Constrained_Modified_Julian_Day is delta Duration'Small / 86_400.0
      range 15_385.0 .. 88_069.0;
   for Constrained_Modified_Julian_Day'Small use Duration'Small / 86_400.0;

   subtype Modified_Julian_Day is Constrained_Modified_Julian_Day'Base;

   type Time is new Modified_Julian_Day;

   Radix_Time : Time;
   --  This is the zero point for time values. Time_Of returns 1 Jan 1970,
   --  0 UTC for this value. The time at which the board boots is given this
   --  conventional Time value. The BSP can adjust the initial real time
   --  relative to this value.

end Ada.Calendar;