[Ada] Revert "Global => null" on calendar routines that use timezones

Some routines from the Ada.Calendar package, i.e. Year, Month, Day,
Split and Time_Off, rely on OS-specific timezone databases that are kept
in files (e.g. /etc/localtime on Linux). In SPARK we want to model this
as a potential side-effect, so those routines can't have "Global =>
null".

2019-07-01  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* libgnat/a-calend.ads: Revert "Global => null" contracts on
	non-pure routines.

From-SVN: r272865

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9ef70a4..68a6828 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,10 @@
 2019-07-01  Piotr Trojanek  <trojanek@adacore.com>
 
+       * libgnat/a-calend.ads: Revert "Global => null" contracts on
+       non-pure routines.
+
+2019-07-01  Piotr Trojanek  <trojanek@adacore.com>
+
        * exp_attr.adb, libgnat/g-graphs.ads: Fix typos in comments:
        componant -> component.
 

diff --git a/gcc/ada/libgnat/a-calend.ads b/gcc/ada/libgnat/a-calend.ads
index 139c5fc..1b782f0 100644 (file)
--- a/gcc/ada/libgnat/a-calend.ads
+++ b/gcc/ada/libgnat/a-calend.ads
@@ -61,19 +61,20 @@ is
    --  the result will contain all elapsed leap seconds since the start of
    --  Ada time until now.
 
-   function Year    (Date : Time) return Year_Number  with Global => null;
-   function Month   (Date : Time) return Month_Number with Global => null;
-   function Day     (Date : Time) return Day_Number   with Global => null;
-   function Seconds (Date : Time) return Day_Duration with Global => null;
+   function Year    (Date : Time) return Year_Number;
+   function Month   (Date : Time) return Month_Number;
+   function Day     (Date : Time) return Day_Number;
+   function Seconds (Date : Time) return Day_Duration;
+   --  SPARK Note: These routines, just like Split and Time_Of below, might use
+   --  the OS-specific timezone database that is typically stored in a file.
+   --  This side effect needs to be modeled, so there is no Global => null.
 
    procedure Split
      (Date    : Time;
       Year    : out Year_Number;
       Month   : out Month_Number;
       Day     : out Day_Number;
-      Seconds : out Day_Duration)
-   with
-     Global => null;
+      Seconds : out Day_Duration);
    --  Break down a time value into its date components set in the current
    --  time zone. If Split is called on a time value created using Ada 2005
    --  Time_Of in some arbitrary time zone, the input value will always be
@@ -83,9 +84,7 @@ is
      (Year    : Year_Number;
       Month   : Month_Number;
       Day     : Day_Number;
-      Seconds : Day_Duration := 0.0) return Time
-   with
-     Global => null;
+      Seconds : Day_Duration := 0.0) return Time;
    --  GNAT Note: Normally when procedure Split is called on a Time value
    --  result of a call to function Time_Of, the out parameters of procedure
    --  Split are identical to the in parameters of function Time_Of. However,