* [Ada] Add "Global => null" contracts to Ada.Calendar routines
@ 2018-12-11 11:37 Pierre-Marie de Rodat
2018-12-11 11:49 ` Florian Weimer
0 siblings, 1 reply; 3+ messages in thread
From: Pierre-Marie de Rodat @ 2018-12-11 11:37 UTC (permalink / raw)
To: gcc-patches; +Cc: Piotr Trojanek
[-- Attachment #1: Type: text/plain, Size: 421 bytes --]
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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-12-11 Piotr Trojanek <trojanek@adacore.com>
gcc/ada/
* libgnat/a-calend.ads: Add "Global => null" contracts to pure
routines.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 3313 bytes --]
--- gcc/ada/libgnat/a-calend.ads
+++ 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;
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [Ada] Add "Global => null" contracts to Ada.Calendar routines
2018-12-11 11:37 [Ada] Add "Global => null" contracts to Ada.Calendar routines Pierre-Marie de Rodat
@ 2018-12-11 11:49 ` Florian Weimer
2018-12-11 12:16 ` Piotr Trojanek
0 siblings, 1 reply; 3+ messages in thread
From: Florian Weimer @ 2018-12-11 11:49 UTC (permalink / raw)
To: Pierre-Marie de Rodat; +Cc: gcc-patches, Piotr Trojanek
* Pierre-Marie de Rodat:
> 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;
Is this really correct? Doesn't this call UTC_Time_Offset eventually,
via Formatting_Operations.Split with Use_TZ => False?
Thanks,
Florian
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [Ada] Add "Global => null" contracts to Ada.Calendar routines
2018-12-11 11:49 ` Florian Weimer
@ 2018-12-11 12:16 ` Piotr Trojanek
0 siblings, 0 replies; 3+ messages in thread
From: Piotr Trojanek @ 2018-12-11 12:16 UTC (permalink / raw)
To: Florian Weimer; +Cc: Pierre-Marie de Rodat, gcc-patches, Piotr Trojanek
On Tue, 11 Dec 2018 12:48:15 +0100, Florian Weimer wrote:
> * Pierre-Marie de Rodat:
>
> > 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;
>
> Is this really correct? Doesn't this call UTC_Time_Offset eventually, via
> Formatting_Operations.Split with Use_TZ => False?
You are right. I will remove the Global contracts from non-arithmetic routines.
Thanks for noticing this!
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2018-12-11 12:16 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-11 11:37 [Ada] Add "Global => null" contracts to Ada.Calendar routines Pierre-Marie de Rodat
2018-12-11 11:49 ` Florian Weimer
2018-12-11 12:16 ` Piotr Trojanek
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).