GNAT에서는 전제 조건이 작동하지 않습니까?

Question

저는 아직 Ada에 대해 처음 접했고 GNAT RM을 살펴보면 검사가 런타임에 수행되지 않는 것 같아서 전제 조건을 잘못 사용하고 있다고 생각합니다. 또한 Precondition here에 대한 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 프로 시저를 호출하기 전에 몇 가지 지정되지 않은 예외가 발생한다 : 여기

은 내가 노력하고있어 코드입니다. 그러나 프로그램을 실행할 때 유효하지 않은 Size 인수를 사용하여 프로 시저가 호출되어 사전 조건 Destination'Size ≥ Size ≤ Source'Size을 위반하는 것을 알 수 있습니다. 대신 실제로 오류를 잡아 내고 Constraint_Error 예외를 발생시켜 정상적인 상태로 유지하려면 if 문을 사용해야합니다.

$ ./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 절을 ​​추가 할 수 있다는 것도 놀랍습니다. 이것은 형식적인 매개 변수 이름을 더 쉽게 정의 할 수있게하지만 (보통은 길다), 보통/정규 프로 시저 선언에서는 수행 할 수 없으므로 버그와 비슷해 보입니다.

P. 나는 학습 목적으로 Ada 언어로 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 (물론, 오프에 검사를 켜거나 사용할 수 없음)에서 구현되지 않습니다. 그러나 은 GNAT GPL 2013에 구현 된입니다. 당신이 GNAT 프로젝트 파일을 사용하지 않는 경우,이 포함 된 파일 gnat.adc을 만드는 의미

pragma Assertion_Policy (Check); 

마이너 점 : 'Size이 비트에,하지 바이트, 그래서 Storage_Count가 정말 올바른 형식이 아닙니다!