diff mbox series

[Ada] Add "Global => null" contracts to Ada.Calendar routines

Message ID 20181211113724.GA106120@adacore.com
State New
Headers show
Series [Ada] Add "Global => null" contracts to Ada.Calendar routines | expand

Commit Message

Pierre-Marie de Rodat Dec. 11, 2018, 11:37 a.m. UTC
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.

Comments

Florian Weimer Dec. 11, 2018, 11:48 a.m. UTC | #1
* 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
Piotr Trojanek Dec. 11, 2018, 12:16 p.m. UTC | #2
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!
diff mbox series

Patch

--- 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;