3

私はFrama-Cの初心者ユーザーであり、ポインターに対するアサーションに関していくつか質問があります。

以下のCフラグメントについて考えてみます。

  • 2つの関連するデータ構造DataとHandle、stHandleにはDataへのポインターがあります。
  • いくつかの架空の操作が完了したかどうかを示すデータの「状態」フィールド
  • 3つの関数：init（）、start_operation（）、wait（）;
  • 上記を使用し、6つのアサーションを含むmain（）関数（A1-A6）

さて、なぜA5とA6はWPベリファイア（ "frama-c -wp file.c"）でアサートできないのですか？start_operation（）の最後の "ensures"句のために保持されるべきではありませんか？

私は何が間違っているのですか？

一番、

エドゥアルド

typedef enum 
{ 
  PENDING, NOT_PENDING
} DataState;

typedef struct 
{
  DataState state;
  int value;  
} Data;


typedef struct 
{
  Data* data;
  int id;
} Handle;

/*@
  @ ensures \valid(\result);
  @ ensures \result->state == NOT_PENDING;
  @*/
Data* init(void);

/*@ 
  @ requires data->state == NOT_PENDING;
  @ ensures data->state == PENDING;
  @ ensures \result->data == data;
  @*/  
 Handle* start_operation(Data* data, int to);

/*@
  @ requires handle->data->state == PENDING;
  @ ensures handle->data->state == NOT_PENDING;
  @ ensures handle->data == \old(handle)->data;
  @*/  
 void wait(Handle* handle);


 int main(int argc, char** argv)
 {
  Data* data = init();
  /*@ assert A1: data->state == NOT_PENDING; */

  Handle* h = start_operation(data,0);
  /*@ assert A2: data->state == PENDING; */
  /*@ assert A3: h->data == data; */

  wait(h);
  /*@ assert A4: h->data->state == NOT_PENDING; */
  /*@ assert A5: data->state == NOT_PENDING; */
  /*@ assert A6: h->data == data; */

  return 0; 
}
4

1 に答える 1

2

あなたは「初心者」のためのトリッキーなメモリ操作を検証しています。

ACSL コンストラクト\oldは、あなたが思っているようには機能しません。

まず、はパラメータであるため\old(handle)、事後条件では と同じです。コントラクトは、呼び出し元の観点から使用することを目的としています。関数が変更されたとしても(異常ではありますが可能です)、そのコントラクトは、呼び出し元によって引数として渡された値と、関数によって返された状態を呼び出し元に関連付けることを目的としています。handlehandlewaithandle

つまり、ACSL 事後条件でparameter\old(parameter)parameterは、(関数がローカル変数のように変更される場合でも)常に意味します。

第 2 に、上記のルールはパラメーターのみを対象としています。グローバル変数とメモリ アクセスの場合、その名前から予想されるように、事後条件は事後状態に適用されると見なされます。あなたが書いた構造\old(handle)->dataは と同等であり、「ハンドルの古い値が新しい状態で指すhandle->dataフィールド」を意味するため、事後条件はトートロジーであり、おそらく意図したものではありません。.datahandle->data == \old(handle)->data

handle->data == \old(handle->data)コンテキストから、代わりに意図したように見えます。これは、「新しい状態で の古い値が指すフィールドは、古い状態で の古い値が指すフィールドと等しい.data」ことを意味します。その変更により、すべてあなたのプログラムのアサーションは私のために証明されます (Alt-Ergo 0.93 を使用)。handle.datahandle

于 2012-03-29T20:50:04.320 に答える