diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2019-07-01 13:35:32 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-01 13:35:32 +0000 |
commit | 25feb37fc665e0c46ee2deec9f47f5ffd4cdd702 (patch) | |
tree | 2e980af8e7ff3f1d5c5a43d9036339fe2187cfbd /gcc | |
parent | b108c2ed65e8fe89acf0845358658a2e0ed07971 (diff) | |
download | gcc-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/ChangeLog | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/a-calend.ads | 19 |
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, |