ada - 检查变量的初始化

Question

在以下代码示例中，变量 Time_Two未初始化。这会导致随机输出，例如:

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

Ada 是否提供了一个函数来在运行时检查 Ada.Calendar.Time 类型的变量是否存在？被初始化了吗？

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

好吧，GNAT 确实发出警告:

warning: variable "Time_Two" is read but never assigned

通过放置配置编译指示 Warning_As_Error 可以将警告转换为错误。要么在 main.adb 的最顶端或在配置文件 gnat.adc [ GNAT RM 2.205 ]

pragma Warning_As_Error ("*never assigned");

处理未初始化的变量是错误的常见来源，本文提供了有关此主题的一些其他背景信息(特别关注使用运行时检查，根据要求)

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

有趣的是，放置配置pragma Initialize_Scalars [ GNAT RM 2.88 ] 在 main.adb 的最顶部产生(对于这种特殊情况)运行时异常 Times_Two用 Long_Long_Integer'First 初始化这似乎对 Ada.Calendar.Time 无效(在 GNAT 中， Long_Long_Integer 是 Ada.Calendar.Time 的底层类型，参见 a-calend.ads ):

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

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

当然，无效值可能不存在或可能具有不同的值。有关 Initialize_Scalars 用法的更多信息，请参阅 GNAT RM 的链接和论文。 .另请参阅相关的 pragma Normalize_Scalars [ GNAT RM 2.122 ]。

检测未初始化变量的另一种(静态)方法是使用 SPARK。试图证明 main.adb的正确性产量:

high: "Time_Two" is not initialized.

更新 1

这是一个如何使用编译指示的最小示例 Initialize_Scalars连同在代码中的特定点插入数据验证检查器的 GNAT 编译器开关:

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;

更新 2

针对以下评论中的反馈的第二个示例(我误解了该问题):

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;