問題タブ [frama-c]

PDGの曲線または円弧の意味を知りたい。これはデータ依存であり、どれは制御依存であるかなどです。

手続き間のデータフロー/ポイントツーグラフを出力するframa-cプラグインはありますか?

スライサープラグインの -pdg にこの情報が含まれることは理解していますが、個別に取得できるかどうか疑問に思っています。

Frama-C を使用して C プログラムのスライスを計算しています。スライスされたプログラムを、コード変換なしで元のように見せたい。ただし、結果のスライスには常に goto ステートメントとラベルがあります。次のコマンドを使用します。

Cygwin の下の Windows マシンで最新の Oxygen リリースから Frama-C をコンパイルしました。

Frama-C バージョン Oxygen のプログラム スライサーを使用すると、結果のスライスが宣言されていない変数を使用するという問題があります。以前にこのトピックへの既存の投稿を検索したところ、これが見つかりました: http://bts.frama-c.com/print_bug_page.php?bug_id=806

Frama-C の Nitrogen バージョンでバグが修正されたことが記載されています。もしかして、この変更は Oxygen に引き継がれなかったのでしょうか? 既存の投稿の説明のように、ステートメントが 1 つだけのブロックでのみ発生します。お客様のプロジェクトからのものであるため、サンプル ソース コードを添付できません。

どのインクルード ファイルを使用するかをFrama-Cに伝える方法を決めるのに、いくつか問題があります。私は通常、オプションを追加します：

Frama-C の標準仕様を備えています。しかし、Frama-C ライブラリにないものが必要になることがよくあります。

たとえば、解析したいソース ファイルの 1 つは で定義されているマクロを使用しています<sys/wait.h>が、Frama-C には独自の があるためframa-c/libc/sys/wait.h、gcc ファイルは含まれていません。残念ながら、Frama-C はマクロを定義しておらず、最終的に定義が失われています。もちろん、ソース ファイルを変更したくありません。

my_libc/sys/wait.hFrama-C ファイルを含み、GCC ファイルにないものをコピーできるファイルでローカル ディレクトリを構築することを考えていました。

次に使用します：

しかし、GCC インクルード ファイルから定義を抽出するのは非常に難しい可能性があるため、私のソリューションには少し不安があります...

どう思いますか？それは良い考えだと思いますか？より良い組織についてアドバイスはありますか?

Frama-Cがポインタに関連付けられたある種の型チェックを実装しているかどうか知りたいです。たとえば、次のことを考慮してください。

上記に似た精神的なものはありますか？

ACSLのマニュアルを見ると、メモリとポインタの使用を確認する方法はたくさんあります（その一部はFrama-C Oxygenに実装されています）。ただし、型情報を処理するための一般的なサポートは見つかりませんでした。この目的で使用できるframa-cプラグインはありますか？

ありがとう、エドゥアルド

C言語用のフォワードスライシングツールを探しています。Googleで検索したところ、結果が見つかりませんでした。

ウィスコンシンプログラム-スライシングツールバージョン1.1にアクセスしたかったのですが、このツールは配布されませんでした。他のツールでフォワードスライスCプログラムの機能を提供できますか？

私がframa-c分析を使用するとき、私のcプログラム。frama-cのインパクトプラグインにバグが残っているようです。これが私のプログラムです。

変数「グローバル」の影響を受けるすべての統計を見つけたいと思います。明らかに、ステートメント「result +=100;」変数「global」に関連する「ifcondition」のスコープ内にあるため、ステートメント「result +=100;」ハイライトである必要があります。ただし、実行結果は正しくないようです。

Frama-c の WP プラグインを使用して、単純なアサーションを証明しようとしています。C コードは、Targetlink ルックアップ テーブルから生成されました。私の目的は、結果のコントラクトを使用して呼び出しプログラムのプロパティを証明できるように、関数に十分な注釈を提供することです。最初のステップとして、関数の先頭付近にアサーションを記述しました。このアサーションは、定数を参照解除されたポインターから取得した値と比較します。次の例を参照してください。

誰かが証明で成功するために必要な注釈を教えてもらえますか? Coq の証明義務を見てみると、「addr_of_data」や「access」など、用語を書き直すために必要な操作の公理がないことがわかります。また、アサーションで参照されているグローバル変数の情報も欠落しています。

BR、ハラルド

配列の定量化されたアサーションを証明しようとしていますが、いくつかの問題が発生しました。次の小さなプログラムを検討してください。

「型付き」メモリモデルを使用しています：

frama-c-gui -wp -wp-qed -wp-byreference -wp-model 'Typed' -main test Test.c

何らかの理由で「要求」が成り立たないため、1==2 であってもすべての主張を証明できます。これを克服するために、関数本体でグローバル変数を直接割り当てます。

ここで forall は成立しますが、exists は成立しません。存在は、アサーション「p[1] == 3」をその前に追加した場合にのみ保持されます。そのような存在する配列プロパティを証明するには何が欠けていますか? これは、配列エントリに対する検索ループのループ不変条件を表現するために必要です。

ありがとう、ハラルド