Check initialization of variable

Question

In the following code example the variable Time_Two is not initialized. This results into a random output like:

Time one: 2019-06-27 16:18:21
Time two: 2150-01-02 16:01:18

Does Ada offers a function to check during runtime if a variable of the type Ada.Calendar.Time is initialized?

with Ada.Calendar;
with Ada.Text_IO;

with GNAT.Calendar.Time_IO;

procedure Main is
   Time_One : Ada.Calendar.Time := Ada.Calendar.Clock;
   Time_Two : Ada.Calendar.Time;

   Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";
begin
   Ada.Text_IO.Put_Line ("Time one: " & GNAT.Calendar.Time_IO.Image
        (Date    => Time_One,
         Picture => Format));

   Ada.Text_IO.Put_Line ("Time two: " & GNAT.Calendar.Time_IO.Image
        (Date    => Time_Two,
         Picture => Format));
end Main;

Answer 1

Well, GNAT does emit a warning:

warning: variable "Time_Two" is read but never assigned

The warning can be converted into an error by placing the configuration pragma Warning_As_Error either at the very top of main.adb or in a configuration file gnat.adc [GNAT RM 2.205]

pragma Warning_As_Error ("*never assigned");

Dealing with uninitialized variables is a common source of errors and some additional background information on this topic (with a particular a focus on using run-time checks, as asked) is available in the paper

Exposing Uninitialized Variables: Strengthening and Extending Run-Time Checks in Ada

Interestingly, placing the configuration pragma Initialize_Scalars [GNAT RM 2.88] at the very top of main.adb yields (for this particular case) a run-time exception as Times_Two is initialized with Long_Long_Integer'First which appears to be invalid for Ada.Calendar.Time (In GNAT, Long_Long_Integer is the underlying type of Ada.Calendar.Time, see a-calend.ads):

$ /main
Time one: 2019-06-27 19:46:54

raised ADA.CALENDAR.TIME_ERROR : a-calend.adb:611

Of course, an invalid value may not exist or may have a different value. See the link to GNAT RM and the paper for more info on the usage of Initialize_Scalars. See also the related pragma Normalize_Scalars [GNAT RM 2.122].

An alternative (static) method to detect uninitialized variables is to use SPARK. An attempt to proof the correctness of main.adb yields:

high: "Time_Two" is not initialized.

---

UPDATE 1

Here's a minimal example of how one can use the pragma Initialize_Scalars together with GNAT compiler switches that insert data valdiation checkers at particular points in the code:

main.adb

--  Ignore compile time warning for the sake of demonstration.
pragma Warnings (Off, "*never assigned");
pragma Initialize_Scalars;

with Ada.Text_IO;

procedure Main is      

   package Foo is

      type Bar is private;

      procedure Put_Bar (B : Bar);

   private

      type Bar is new Integer range -20 .. 20;

   end Foo;


   package body Foo is

      procedure Put_Bar (B : Bar) is
      begin

         --  (2) Constraint_Error is raised if switch "-gnatVDo" (Validate 
         --  Operator and Attribute Operands) is used during compilation. 
         --  This switch effectively inserts the code 
         --
         --     if not B'Valid then
         --        raise Constraint_Error with "invalid data";
         --     end if;
         --
         --  just before B'Image is evaluated. As the value Integer'First
         --  is not in Bar'Range, B'Valid returns False and the
         --  exception is raised.
         --
         --  See also in GPS IDE:
         --
         --    Edit > Project Properties... > Build > Switches > Ada
         --       and then "Validity Checking Mode".

         Ada.Text_IO.Put_Line (B'Image);

      end Put_Bar;

   end Foo;   


   --  (1) Because pragma "Initialize_Scalars" is used, B is deterministically
   --  initialized to Integer'First. This behavior is inherited from the
   --  configuration pragma "Normalize_Scalars" (see GNAT RM). Here, 
   --  Integer'First happens to be invalid as it falls outside the 
   --  range of subtype Foo.Bar (which is -20 .. 20).

   B : Foo.Bar;   

begin
   Foo.Put_Bar (B);
end Main;

---

UPDATE 2

Second example in response to the feedback in the comments below (I misinterpreted the question):

main.adb

with Ada.Calendar;
with Ada.Text_IO;

with GNAT.Calendar.Time_IO;

procedure Main is

   type Optional_Time (Valid : Boolean := False) is
      record
         case Valid is
            when False =>
               null;
            when True =>
               Value : Ada.Calendar.Time;
         end case;
      end record; 

   -----------
   -- Image --
   -----------

   function Image (OT : Optional_Time) return String is
      Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";   
   begin
      if OT.Valid then
         return GNAT.Calendar.Time_IO.Image (OT.Value, Format);
      else
         return "<Invalid>";
      end if;
   end Image;


   Time : Optional_Time;

begin

   Ada.Text_IO.Put_Line (Image (Time));

   Time := (Valid => True, Value => Ada.Calendar.Clock);
   Ada.Text_IO.Put_Line (Image (Time));

   Time := (Valid => False);
   Ada.Text_IO.Put_Line (Image (Time));

end Main;

Answer 2

Using a Boolean discriminant for a wrapper type as suggested in the first answer comes close to answering the question, but technically, that technique just distinguishes between having a value and not having a value, not necessarily being able to detect if a variable is uninitialized. One can determine the variable was initialized if it is non-default, but cannot determine if it was initialized to the default value, or subsequently reset to the default value after being set to a non-default value.

If you want to more accurately determine if the corresponding date value has been "initialized" or not, another approach would be to define an invalid value, and create a subtype that excludes that value. One could create an abstraction that default initializes a holder/wrapper type to have the invalid value, but provide an interface that only allows the user to assign valid values. Then one can more accurately determine at run time whether the variable has been initialized or not. Making the holder type a limited type also further restricts the usage to prevent reassigning an uninitialized value to a variable that has already been initialized.

e.g.

with Ada.Calendar;
with GNAT.Calendar.Time_IO;

package Initialized_Times is

   use type Ada.Calendar.Time;

   End_Of_Time : constant Ada.Calendar.Time
     := Ada.Calendar.Time_Of
       (Year    => Ada.Calendar.Year_Number'Last,
        Month   => Ada.Calendar.Month_Number'Last,
        Day     => Ada.Calendar.Day_Number'Last,
        Seconds =>
          Ada.Calendar.Day_Duration'Pred
            (Ada.Calendar.Day_Duration'Last));

   subtype Initialized_Time is Ada.Calendar.Time
     with Dynamic_Predicate => 
        Initialized_Time < End_Of_Time;

   type Time_Holder  is limited private;

   Invalid_Time : constant Time_Holder;

   function Create
      (Value : Initialized_Time) return Time_Holder;

   procedure Update (Date : in out Time_Holder;
                     Value : Initialized_Time);

   function Image (OT : Time_Holder) return String;

   function Time_Of
     (Date : Time_Holder) return Initialized_Time;

   function Is_Valid
     (Date : Time_Holder) return Boolean;

private

   type Time_Holder is limited
      record
         Value : Ada.Calendar.Time := End_Of_Time;
      end record;

   function Create
     (Value : Initialized_Time) return Time_Holder is
       (Value => Value);

   function Time_Of
     (Date : Time_Holder) return Initialized_Time is
       (Date.Value);

   function Image (OT : Time_Holder) return String is
     ((if Is_Valid (OT) then
         GNAT.Calendar.Time_IO.Image
           (OT.Value, "%Y-%m-%d %H:%M:%S")
       else "<Invalid>"));

   function Is_Valid
     (Date : Time_Holder) return Boolean is
       (Date.Value /= End_Of_Time);

   Invalid_Time : constant Time_Holder :=
      (Value => End_Of_Time);

end Initialized_Times;

---------------------------------------------

package body Initialized_Times is

   procedure Update (Date : in out Time_Holder; 
                     Value : Initialized_Time) is
   begin
      Date.Value := Value;
   end Update;

end Initialized_Times;

-------------------------------------------------

with Ada.Calendar;
with Ada.Text_IO;
with Initialized_Times;

procedure Main is
   Time : Initialized_Times.Time_Holder;
begin
   Ada.Text_IO.Put_Line
      (Initialized_Times.Image (Time));

   Ada.Text_IO.Put_Line ("Time is " &
                          (if Initialized_Times.Is_Valid
                             (Date => Time) then "" 
                           else "not ") &
                         "initialized.");

   Initialized_Times.Update
     (Date => Time,
      Value => Ada.Calendar.Clock);

   Ada.Text_IO.Put_Line ("Time is " &
                         (if Initialized_Times.Is_Valid
                            (Date => Time) then ""
                          else "not ") &
                         "initialized.");

   Ada.Text_IO.Put_Line
      (Initialized_Times.Image (Time));

end Main;