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