前提条件不适用于GNAT？

Question

我仍然是Ada的新手,我认为我误解了Preconditions的使用,因为通过GNAT RM查看似乎检查不会在运行时执行.此外,此处的GNAT RM for Precondition不指定在不满足前提条件时抛出哪个异常.

这是我正在尝试的代码:

procedure Test is
begin

   generic
      type Element_Type is private;
      use System.Storage_Elements;
   procedure Byte_Copy (Destination : out Element_Type;
                        Source      : in  Element_Type;
                        Size        : in  Storage_Count := Element_Type'Size)
      with Pre =>
         Size <= Destination'Size and 
         Size <= Source'Size;

   procedure Byte_Copy (Destination : out Element_Type;
                        Source      : in  Element_Type;
                        Size        : in  Storage_Count := Element_Type'Size)
   is
      subtype Byte_Array is Storage_Array (1 .. Size / System.Storage_Unit);

      Write, Read : Byte_Array;
      for Write'Address use Destination'Address;
      for Read'Address  use Source'Address;
   begin
      Ada.Text_IO.Put_Line("Size to copy =" & Size'Img  &
                           " and Source'Size =" & Source'Size'Img);

      if Size > Destination'Size or else Size > Source'Size then
         raise Constraint_Error with
            "Source'Size < Size or else > Destination'Size";
      end if;

      for N in Byte_Array'Range loop
         Write (N) := Read (N);
      end loop;
   end Byte_Copy;

   procedure Integer_Copy is new Byte_Copy(Integer);
   use type System.Storage_Elements.Storage_Count;

   A, B : Integer;
begin
   A := 5;
   B := 987;
   Ada.Text_IO.Put_Line ("A =" & A'Img);
   Ada.Text_IO.Put_Line ("B =" & B'Img);

   Integer_Copy (A, B, Integer'Size / 2);
   Ada.Text_IO.Put_Line ("A = " & A'Img);
   Ada.Text_IO.Put_Line ("B = " & B'Img);

   Integer_Copy (A, B, Integer'Size * 2);
   Ada.Text_IO.Put_Line ("A =" & A'Img);
   Ada.Text_IO.Put_Line ("B =" & B'Img);
end Test;

如果我理解正确,那么在调用Put_Line过程之前,该程序应该引发一些未指定的异常.但是你可以看到,当我运行程序时,使用无效的Size参数调用该过程,该参数违反了Precondition Destination'Size ? Size ? Source'Size.相反,我必须放置一个if语句来实际捕获错误并引发异常Constraint_Error以保持理智.

$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A =  987
B =  987
Size to copy = 64 and Source'Size = 32

raised CONSTRAINT_ERROR : Source'Size < Size or else > Destination'Size

我尝试过像添加pragma Precondition ( ... )这样的变体,但这也不起作用.

一个奇怪的事情是,如果我with Pre =>在通用过程体/定义中重复该子句,程序实际上会编译.它通常不允许这个过程并引发错误(即,前提条件应仅在正式声明中,而不是在定义中).在这种情况下,通用程序是例外吗？

我也很惊讶use子句可以添加到泛型过程声明中.这使得定义形式参数名称更容易(那些是非常长的)但看起来更像是一个bug,因为这不能用于正常/常规过程声明.

PS我想用C语言实现我最接近的可能模仿memcpy(),用于学习目的.

Answer 1

您需要通过编译来启用断言-gnata:

$ gnatmake -gnat12 -gnata test.adb
gcc -c -gnat12 -gnata test.adb
gnatbind -x test.ali
gnatlink test.ali
gnatlink: warning: executable name "test" may conflict with shell command

$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A =  987
B =  987

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from test.adb:13 instantiated at test.adb:39

Pragma Assertion_Policy未在FSF GNAT <= 4.8中实现(嗯,您无法使用它来打开或关闭检查).但是,它是在GPL GNAT 2013执行; 如果您不使用GNAT项目文件,这将意味着创建一个gnat.adc包含的文件

pragma Assertion_Policy (Check);

小点:'Size是位,而不是字节,因此Storage_Count它不是真正的正确类型!