問題タブ [frama-c]

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

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

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

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

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

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

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

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

Frama-C (Neon-20140301) と Alt-Ergo で WP チュートリアルの例を試しています。「不一致アルゴリズム」の例には行き詰まりましたが、「equal」や「find」などの他の同様の例には問題はありません。コードを以下に示します。ポストコンディション P0、P2 は放電されていません。ここで何が間違っているのか誰にも教えてもらえますか?

まず第一に、ここで何をしたいかを説明します: C の大きなプログラムが与えられた場合、データのプロデューサー/コンシューマーのリストと、関数の呼び出し/呼び出し関数のリストを出力したいと思います。データは。

これを行うために、自分のプラグインで dataflow.ml や callgraph.ml のような、frama-c のいくつかのモジュールを計算するものを使用することを考えています。

ただし、プラグイン開発者のドキュメントを読んでいると、これらのモジュールのデータにアクセスする方法がわかりません。

ここで自分のプラグインでは「open.cyl_type」で十分ですか?

さらに、ここに私の他の質問があります：

ちなみにpdgプラグインを目的に使用してみましたが、それを呼び出して「pdgグラフが計算されました」と表示された場合、どうすればアクセスできますか?

「インパクト」プラグインについて、公式 Web ページ以外に詳細に文書化されているものはありますか? (私はプロジェクト前の段階にあり、ubuntu に apt-get を使用して frama-c をインストールし、影響を与えるプラグインが機能していないと言わざるを得ません (ソースをコンパイルすることで確認できます) )))

ところで、目的を達成するために正しい方法を使用していると思いますか?

Frama-c でメモリリークやダブルフリーを検出することはできますか? その例をテストしようとしましたが、

私は得る：

現在、バージョン: Neon-20140301 とFluorine-20130601 からコピーされたlibcを使用しています (なぜ fc_runtime.c と他の *.c ファイルが Neon リリースから削除されているのですか?)

指図：

他の定義 (FRAMA_C_MALLOC_XXXX) を使用すると機能しますが、バグは検出されません。

更新: その他の例

ソース コードとスライスされたコードを比較しようとしていますが、frama-c は解析時にコードを正規化するため、スライスされたコード ステートメントはソース コード ステートメントと同一ではありません。

Frama-c を使用してコードを前処理して、条件を使用してスライスしたときに、結果のスライスされたステートメントを前処理されたステートメントと比較できるようにすることは可能ですか?

ありがとう。