問題タブ [frama-c]

Frama-C プラグインの開発方法を学んでいます。Frama-C 開発者マニュアルを読み、CFG プラグインの例を実行した後、すべての注釈を C ファイルに出力する基本的なスクリプトを実行しようとしました。私はこれを思いついた：

入力ファイルにACSL注釈があり、注釈IDが出力されない場合でも、常にリストが空であると表示されます。私は何を間違っていますか？

編集：

次のコードの例:

そして、frama-c を次のように呼び出します。

次の出力が得られます。

Frama-C でプラグインを開発しています。xml ファイルを解析したい。パッケージ libxml-light-ocaml-dev をインストールしましたが、コンパイル中に「Unbound module Xml」というエラーが発生します。Frama-C がパッケージを認識できるようにする方法がわかりません。または、別のパッケージを使用する必要がありますか?

printf 呼び出しで次のプログラムをスライスしようとしています。

ただし、Value Analysis プラグインは次のメッセージを表示します。

foo.c:9:[value] 関数呼び出し式の引数 (char const )の評価で非終了(argv + 2),

スライスされたプログラムは空です！これは Frama-C のバグ/機能ですか? それとも私は何か間違ったことをしていますか？

完全なトレースは次のとおりです。

Ubuntu 14.04 を使用して、Neon Frama-C ディストリビューションをダウンロードし、必要なツール (labgtk、sourceview など) をインストールしました。

問題は

ここで、Z はインポートされていないモジュールを示します (推測します)。Z が何を参照することになっているのかわからないので、これを修正しようとする方法がありません。

オプション -wp-out を指定して Frama-C WP を使用する場合、たとえば (swap.c の例を使用): swap.c

実行する:

そして出力付き：

プロパティを証明し、プログラムの妥当性を証明するために必要な証明義務を含むフォルダーを生成しますが、すべてではなく、Alt-ergo に送信されたものだけが Qed によって証明されるものは生成されません。

Qed の目的は単純化し、自明な特性を証明して証明者の時間と労力を節約することだと理解していますが、証明者に送信するすべての証明義務を生成させることは可能ですか? これは、Qed を無効にして Frama-C にすべての証明義務をオルターゴに生成させることですか?

Frama-C の最新バージョンの ACSL 仕様に問題があります。
実数のペアを宣言するために多くのことを試みましたが、どれも機能しませんでした。問題ごとに示す小さな例を次に示します。

与える：

[カーネル] ユーザー エラー: 予期しないトークン '('

最後に、コードを の近くに置きたい:

誰かがエラーの場所を見ていますか? ACSL ドキュメントの型宣言が非常に曖昧であることがわかりました...

回答ありがとうございます。

よろしくお願いします、

ニレクシス。