Предварительные условия не работают с GNAT?

Question

Я все еще новичок в Ada и думаю, что неправильно понимаю использование предварительных условий, потому что, глядя через GNAT RM, кажется, что проверки не выполняются во время выполнения. Кроме того, GNAT RM для предусловия здесь не указывает, какое исключение выдается, если предусловие не выполнено.

Вот код, который я пытаюсь:

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. Но вы можете видеть, что когда я запускаю программу, процедура вызывается с недопустимым аргументом размера, который нарушает предварительное условие 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 может быть добавлено в объявления общих процедур. Это облегчает определение формальных имен параметров (которые непристойно длинные), но больше похоже на ошибку, потому что это не может быть сделано для объявлений обычной / обычной процедуры.

PS Я хотел реализовать свою ближайшую имитацию memcpy() из C на языке Ada для изучения.

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 (ну, вы не можете использовать его для включения или выключения проверок). Однако это реализовано в GNAT GPL 2013; если вы не используете файлы проекта GNAT, это будет означать создание файла gnat.adc содержащий

pragma Assertion_Policy (Check);

Незначительная точка: 'Size в битах, а не в байтах, так Storage_Count не совсем подходит для этого типа!