問題タブ [frama-c]

ACSL 仕様で名前付き定数を使用するにはどうすればよいですか? これらの定数は、マクロ ( #define MY_CONST ...) または定数宣言 ( )のいずれかconst int MY_CONST ...です。前者はマクロがプリプロセッサによって展開されないため (ACSL 仕様は C コメントです)、機能しません。後者は、定数が変数として扱われ、一部の証明が失敗するため機能しません。名前付き定数を実際の数値に置き換えると、仕様は正常に機能します。

名前付き定数を処理する良いアイデアはありますか? 前もって感謝します

私はframa-cへのプラグインを開発しようとしています。いくつかのファイルを持つアプリケーションをビルドし、makefile必要なすべてのファイルを参照するアプリケーションを作成しました。

プラグインを使用makeして実行することができます。関数内のライブラリmake installから関数を呼び出すと、私の問題が発生します...ocamlyices

私はまだmakeとmake installを実行できますが、実行しようとすると次のエラーが発生します:

したがって、ocamlyices関数への呼び出しを追加すると、互換性がないと表示されます。どこかに欠けているオプション/構成はありますか?

ご協力ありがとうございました。

最終的な解決策は次のようになりました。

変数 $(YICES) は次のように定義されます。

私は Frama-C の初心者で、char 配列の注釈の書き方に関するいくつかの注釈を探していました。通常、例では整数を使用しています。そのため、私が書いたことが正しいかどうかはわかりません。

私はこの機能を持っています:

以下のような注釈を書きましたが、よくわかりません。

使用してみframa-c-guiましたが、影響分析を実行できましたが、Frama-C のバッチ モードで影響分析を実行する必要があるステートメント番号を渡す方法がわかりません。

私は、Why2、Why3、および Coq と共に Frama-C Neon (Ubuntu) を正常にコンパイルしました。

以前のバージョン (Nitrogen) では、次のようなシンボルを定義することで、特定のヒープ モデルを選択することができました。

等々。

Frama-C Neonのユーザー マニュアルでは、ファイルを含めるように提案されていますshare/malloc.cが、見つかりません。

• Frama-C Nitrogen にはshare/malloc.cとの両方が含まれていますshare/libc/stdlib.c(後者は正常に機能しました)。
• Frama-C Fluorine 3 には次の成分share/stdlib.cのみが含まれています。
• Frama-C Fluorine 2 にはどちらも含まれていません。
• Frama-C Neon にはどちらも含まれていません。

さらに、Fluorine 3 の変更ログには、「欠落している C ライブラリ ファイルを追加する」と記載されています。

シンボルは非推奨ですかFRAMA_C_MALLOC_*、それとも Neon ソース配布はやや不完全ですか?

Frama-C を Mavericks にインストールした人はいますか? インストールできない、またはインストール方法がわからないため（Guiバージョン）！

私はすでに ocaml を PC にインストールしていますが、Gui バージョンでは次のライブラリをインストールする必要があります: Gtk、GtkSourceView、GnomeCanvas、Lablgtk2。

だから私は以前の投稿を見て、それをしました：

次のようなframa-cで「make」を行う際に問題があります：

どうすればこれを解決できますか?