1

私はまだ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 プロシージャを呼び出す前に、特定されていない例外を発生させるはずです。しかし、プログラムを実行すると、 Precondition に違反する無効な Size 引数でプロシージャが呼び出されることがわかります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 =>奇妙なことの 1 つは、ジェネリック プロシージャ本体/定義で句を繰り返すと、プログラムが実際にコンパイルされることです。これは通常、プロシージャに対してこれを許可せず、エラーを発生させます (つまり、事前条件は、定義ではなく正式な宣言にのみ含める必要があります)。この場合、一般的な手順は例外ですか?

また、ジェネリック手続き宣言に use 句を追加できることにも驚きました。これにより、正式なパラメーター名 (非常に長いもの) の定義が容易になりますが、これは通常/通常のプロシージャー宣言では実行できないため、バグのように見えます。

PS 私は、学習目的で Ada 言語で、C からの memcpy() の可能な限り最も近い模倣を実装したいと考えていました。

4

1 に答える 1

6

次のようにコンパイルして、アサーションを有効にする必要があります-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実際には適切なタイプではありません!

于 2013-08-28T11:34:28.750 に答える