检查变量的初始化

Question

在下面的代码示例中，变量Time_Two未初始化。结果是随机输出，如：

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

Ada是否提供一种在运行时检查类型变量Ada.Calendar.Time是否已初始化的功能？

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

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

处理未初始化的变量是常见的错误来源，并且本文中提供了有关此主题的其他一些背景信息（特别是按要求着重于使用运行时检查）。

公开未初始化的变量：加强和扩展Ada中的运行时检查

有趣的是，将配置实用程序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

当然，无效值可能不存在或具有不同的值。有关使用的更多信息，请参见GNAT RM的链接和本文Initialize_Scalars。另请参阅相关的用法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;