aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2019-07-01 13:35:32 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-07-01 13:35:32 +0000
commit25feb37fc665e0c46ee2deec9f47f5ffd4cdd702 (patch)
tree2e980af8e7ff3f1d5c5a43d9036339fe2187cfbd /gcc
parentb108c2ed65e8fe89acf0845358658a2e0ed07971 (diff)
downloadgcc-25feb37fc665e0c46ee2deec9f47f5ffd4cdd702.zip
gcc-25feb37fc665e0c46ee2deec9f47f5ffd4cdd702.tar.gz
gcc-25feb37fc665e0c46ee2deec9f47f5ffd4cdd702.tar.bz2
[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
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/libgnat/a-calend.ads19
2 files changed, 14 insertions, 10 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9ef70a4..68a6828 100644
--- 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
--- 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,