4

Frama-C を使用してある種の前方条件付きスライシングを実行できるかどうかを知りたいのですが、これをどのように達成できるかを理解するためにいくつかの例を試しています。

不正確なスライスになると思われるこの単純な例がありますが、その理由がわかりません。スライスしたい関数は次のとおりです。

int f(int a){
int x;
if(a == 0)
    x = 0;
else if(a != 0)
    x = 1;
return x;
}

この仕様を使用する場合:

/*@ requires a == 0;
  @ ensures \old(a) == a;
  @ ensures \result == 0;
*/

Frama-C は、「f -slice-return」基準と f をエントリ ポイントとして使用して、次のスライス (正確です) を返します。

/*@ ensures \result ≡ 0; */
int f(void){
  int x;
  x = 0;
  return x;
}

しかし、この仕様を使用する場合:

/*@ requires a != 0;
  @ ensures \old(a) == a;
  @ ensures \result == 1;
*/

その後、すべての命令 (& 注釈) が残ります (このスライスが返されるのを待っていたとき:

/*@ ensures \result ≡ 1; */
int f(void){
  int x;
  x = 1;
 return x;
}

)

最後の場合、スライスは不正確ですか? この場合、何が原因として考えられるでしょうか？

よろしく、

ロマン

編集：「else if(a != 0) ...」と書きましたが、「else ...」に問題が残ります

4

2 に答える 2

2

これはあなたの主な質問とはまったく関係ありませんが、あなたのensures a == \old(a)句はあなたが期待することをしていません。オプション を使用してソース コードを整形-printすると、暗黙のうちに に変換されていることがわかりますensures \old(a) == \old(a)。

ACSL 言語では、事後状態で仮変数の値を参照することは許可されていません。これは主に、これが呼び出し元の観点から無意味であるためです。(呼び出しが終了すると、呼び出し先のスタック フレームがポップされます。)

于 2013-07-10T20:50:30.560 に答える