私はまだ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() の可能な限り最も近い模倣を実装したいと考えていました。