From c47fb5d9da9b60987babba6d05d5f97d03d0246b Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 11 Dec 2018 11:12:41 +0000 Subject: [PATCH] [Ada] Add "Global => null" contracts to Ada.Calendar routines Routines in Ada.Real_Time are already annotated with Global => null contracts to suppress spurious warnings from the flow analysis in GNATprove. This patch adds such contracts to Ada.Calendar. No change in runtime behavior expected. 2018-12-11 Piotr Trojanek gcc/ada/ * libgnat/a-calend.ads: Add "Global => null" contracts to pure routines. From-SVN: r267018 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/libgnat/a-calend.ads | 40 +++++++++++++++++++++++------------- 2 files changed, 31 insertions(+), 14 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c08199bbcf5..c0ba34a874f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-12-11 Piotr Trojanek + + * libgnat/a-calend.ads: Add "Global => null" contracts to pure + routines. + 2018-12-11 Hristian Kirtchev * freeze.adb (Check_Pragma_Thread_Local_Storage): Use the diff --git a/gcc/ada/libgnat/a-calend.ads b/gcc/ada/libgnat/a-calend.ads index b1243804cb1..02accbd17eb 100644 --- a/gcc/ada/libgnat/a-calend.ads +++ b/gcc/ada/libgnat/a-calend.ads @@ -61,17 +61,19 @@ is -- the result will contain all elapsed leap seconds since the start of -- Ada time until now. - 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; + 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; procedure Split (Date : Time; Year : out Year_Number; Month : out Month_Number; Day : out Day_Number; - Seconds : out Day_Duration); + Seconds : out Day_Duration) + with + Global => null; -- 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 @@ -81,7 +83,9 @@ is (Year : Year_Number; Month : Month_Number; Day : Day_Number; - Seconds : Day_Duration := 0.0) return Time; + Seconds : Day_Duration := 0.0) return Time + with + Global => null; -- 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, @@ -97,19 +101,27 @@ is -- Seconds may be 14340.0 (3:59:00) instead of 10740.0 (2:59:00 being -- a time that not exist). - function "+" (Left : Time; Right : Duration) return Time; - function "+" (Left : Duration; Right : Time) return Time; - function "-" (Left : Time; Right : Duration) return Time; - function "-" (Left : Time; Right : Time) return Duration; + function "+" (Left : Time; Right : Duration) return Time + with + Global => null; + function "+" (Left : Duration; Right : Time) return Time + with + Global => null; + function "-" (Left : Time; Right : Duration) return Time + with + Global => null; + function "-" (Left : Time; Right : Time) return Duration + with + Global => null; -- The first three functions will raise Time_Error if the resulting time -- value is less than the start of Ada time in UTC or greater than the -- end of Ada time in UTC. The last function will raise Time_Error if the -- resulting difference cannot fit into a duration value. - function "<" (Left, Right : Time) return Boolean; - function "<=" (Left, Right : Time) return Boolean; - function ">" (Left, Right : Time) return Boolean; - function ">=" (Left, Right : Time) return Boolean; + function "<" (Left, Right : Time) return Boolean with Global => null; + function "<=" (Left, Right : Time) return Boolean with Global => null; + function ">" (Left, Right : Time) return Boolean with Global => null; + function ">=" (Left, Right : Time) return Boolean with Global => null; Time_Error : exception;