2

ドキュメントとコードを検索してみましたが、これが何であるかを見つけることができないため、修正方法がわかりません。

シナリオ：

私は Ada SPARK ベクトル ライブラリを使用しており、次のコードがあります。

package MyPackage
  with SPARK_Mode => On
is
  package New_Vectors is new Formal_Vectors (Index_Type => test, Element_Type => My_Element.Object);
type Object is private;
private

   type Object is
      record
         Data : New_Vectors.Vector (Block_Vectors.Last_Count);
         Identifier : Identifier_Range;
      end record;

コードが呼び出すとエラーが発生します：

function Make (Identifier : Identifier_Range) return Object is
   begin
      return (
              Data => New_Vectors.Empty_Vector,
              Identifier => Identifier);
   end Make;

を指していEmpty_Vectorます。難しいのは、問題を引き起こしているように見えるasをEmpty_Vector定義することです。今では、型定義にあるように見えるので、それをどのように処理するかわかりません( を調べました)。Capacity0Capacitya-cofove.ads

したがって、基本的に私はこれを解決する方法について行き詰まっています。または、これが将来起こることをどのように見つけるか。

4

1 に答える 1

4

あなたの分析は正しいです。このエラーは、空のベクトル (つまり、容量が 0 のベクトル) を容量のあるベクトルBlock_Vectors.Last_Count(ゼロでないように見える) に代入しようとしたために発生します。

実際には、ベクターを使用するために明示的に初期化する必要はありません。以下の例に示すように、デフォルトの初期化 (を使用します。<>たとえば、ここを参照) で十分です。

ただし、実行時エラーがないことを証明するには、を使用してベクトルを明示的にクリアする必要がありますClear。このEmpty_Vector関数は、以下の例に示すように、ベクトルが空かどうかをチェックするアサーションで使用できます。を使用して、この例に実行時エラーがないことを示すことができますgnatprove。たとえば、GNAT Studio でメニュー SPARK > Prove からプローブ設定を開き、[全般] セクション (左上) で [レポート チェックが移動しました] を選択し、[実行] (右下) を選択して分析を実行します。

main.adb

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Containers.Formal_Vectors;

procedure Main with SPARK_Mode is
      
   package My_Vectors is new Ada.Containers.Formal_Vectors 
     (Index_Type   => Natural, 
      Element_Type => Integer);
   use My_Vectors;
   
   type Object is record
      Data  : Vector (Capacity => 10);   --  Max. # of elements: 10
      Value : Integer;
   end record;
   
   --  Initialize with default value (i.e. <>), no explicit initialization needed.
   Obj : Object :=
     (Data  => <>,
      Value => 42);
   
begin
   
   --  Clear the vector, required for the assertions to be proven.
   Clear (Obj.Data);
         
   --  Assert that the vector is not empty.
   pragma Assert (Obj.Data = Empty_Vector);
      
   --  Populate the vector with some elements.
   Append (Obj.Data, 4);
   Append (Obj.Data, 5);
   Append (Obj.Data, 6);
   
   --  Assert that the vector is populated.
   pragma Assert (Obj.Data /= Empty_Vector);
      
   --  Show the contents of Obj.Data.
   Put_Line ("Contents of Obj.Data:");
   for I in Natural range 0 .. Natural (Length (Obj.Data)) - 1 loop
      Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
   end loop;
   New_Line;
   
   --  or, alternatively using an iterator ...   
   declare
      I : Extended_Index := Iter_First (Obj.Data);
   begin
      while Iter_Has_Element (Obj.Data, I) loop
         Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
         I := Iter_Next (Obj.Data, I);
      end loop;
   end;
   New_Line;
   
   --  Show the contents of Obj.Value.
   Put_Line ("Contents of Obj.Value:");
   Put_Line (Obj.Value'Image);
   New_Line;   
   
end Main;

出力

Contents of Obj.Data:
[ 0] 4
[ 1] 5
[ 2] 6

[ 0] 4
[ 1] 5
[ 2] 6

Contents of Obj.Value:
 42
于 2021-01-20T19:10:50.780 に答える