static-analysis - ACSL/Frama-C による数学関数仕様の導入

Question

通常 -lm でコンパイル時に呼び出される関数の仕様を ACSL で sqrt として実装することは可能ですか? Frama-CのプラグインWPに使用しています。

これは、私がやりたいことを説明するための小さな例です。

/*@ requires sqrt_spec: \forall float x; 
             \model(sqrt(x)) * \model(sqrt(x)) == \model(x);  
    ensures [...] */  

void f (...) {
double y = sqrt x;
[...]
}

明らかに、これを行うと、注釈で使用すると sqrt が存在しないため、WP が泣きます。

[カーネル] ユーザー エラー: 注釈内のバインドされていない関数 sqrt

だから私は抽象的なsqrtを定義したいのですが、私のテストはどれもうまくいきませんでした:

#define sqrt(x) (...)

これについては、float sqrt全体を再実装するのではなく、抽象的な定義が必要なため、(...)に何を入れることができるかわかりません。

/*@  axiomatic SqrtSpec {
logic real sqrt (real x);
} */

そして、これは私の問題を解決しません:

関数 sqrt のコードも仕様もなく、プロトタイプからデフォルトの代入を生成します。