問題タブ [frama-c]

私は実際に、これらの 4 つのファイルを含む個人的な Frama-C プラグインを作成しています。

analyseTU_core.ml

と ：

analyseTU_register.ml

と ：

analyseTU_options.ml

そして最後にメイクファイル:

したがって、make コマンドでコンパイルすると、実際には次のようになります。

out がコンパイラに認識されないからだと思っていたので、out を chan に置き換えました。ところで、同じエラーが発生していました。

開発者ガイドのチュートリアルのコードで「out」が定義されていないという事実により、最終的に、このエラーは私が考えているものではないと思います...

遭遇したことはありますか？はいの場合、どのように対処しましたか？

私は Frama-c の新しいユーザーです。Neon-20140301 をインストールしたばかりで、Ocaml コンパイラ 4.01.0 を使用して Fedora 14 システムに 2.34 をインストールしたのはなぜですか。

非 GUI モードで、インストールは成功しました。

しかし、why2.34 からいくつかの例を実行しようとすると、次のようないくつかのエラーが発生しました: 互換性の問題があるようです。

Frama-C を使用して、動的メモリ割り当てを含む C コードの安全性を検証しようとしています。現在のバージョンの ACSL 仕様言語 (1.8) では、動的に割り当てられたメモリについて多くのことを表現できるようです。ただし、そのほとんどはまだ Frama-C Neon に実装されていません。

次のコード スニペットを使用するとします。

そのため、main は 2 つのメモリ ブロックを割り当て、それらへのポインタを関数 test に渡します。テストは、p が指すブロックを解放しますが、q が指すブロックは解放しません。テストの最後に、ポインター q がまだ有効であることを証明したいとします。どのように進めますか？

自分でヒープをモデル化する必要があるようです: ヒープについて話すいくつかの述語を公理化し、それらを使用して malloc と free を指定し、ACSL の実装されていない部分を模倣します。上記の例を確認できるように、それを行う最も簡単な方法は何ですか?

calculus.ml コードに従ってテーブルに格納されている Frama-C によって生成されたすべての前提条件を生成したいと思います。私は主に、論理式に変換されてソルバーに送信される初期述語を取得することに興味があります。これはできますか？ソルバーに送信される最初の述語を印刷するのを手伝ってください。私が試しているコードを以下に示します。

Frama-c から後方スライスを取得しましたが、動的スライスではなく静的スライスのように見えます。

動的後方スライスを取得するためのframa-cの特定のオプションはありますか?

frama-c と why3 をインストールしましたが、frama-c を起動しようとすると、jessie3 でエラーが発生します。

camlGzip に関する情報が見つからないため、構成ファイル (camlzip である可能性があります) でエラーになる可能性がありますが、宣言されている場所はわかりません。

編集: Jessie3.cmxs の camlzip で camlGzip を変更しようとしましたが、frama-c を起動するとセグメンテーション違反が発生します

私のframa-cとWhy3のバージョン：

Mint17 仮想マシンで作業していますが、各プログラムの ./configure と make にエラーはありませんでした

誰かがすでにこの問題を抱えていて、私を助けてくれることを願っています

この例で、戻り値が 0 (配列に 8 がない場合) または 1 (配列に 8 がある場合) になることを証明しようとしています。

そして、事前条件と事後条件を作成しました。

Frama-C は Hoare Logic に基づいているため、ループ不変条件:

forall を使用しようとしていて、存在する行に何かが欠けていると確信しています。配列に値が割り当てられているかどうかを正しく確認する方法を理解するために何時間も費やしていますが、ここで立ち往生しているように感じます。私は本当にあなたの助けに感謝します:)