frama-c

1熱

1答えて

私は、Linux、の最新FRAMA-cの放出（リン）を設置し、グローバル不変を定義しようとしましたが、 WPではまだサポートされていないメッセージを持っています。その状態はどうなっていますか？ ACSL言語でサポートされているものについてのドキュメントはありますか？ありがとうございました。

0熱

1答えて

Frama-cインストール - 構成：エラー：ocamlfindが見つかりません

xhy0908deMacBook-Pro:frama-c-Phosphorus-20170501 xhy0908$ ./configure configure: ****************** configure: * CONFIGURE MAKE * configure: ****************** checking for make... make checking

-3熱

1答えて

Frama-c前処理エラー

私はCコードをスライスしたいのですが、コマンドを書くときにエラーが発生します。 *******[15:18, 26.10.2017] Recep: [kernel] Parsing .opam/system/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] user error: so

1熱

1答えて

FRAMA-cは、非決定論フロートは

は、例として、私は次の関数を使用する値。変数xは、-inf、+ inf、NaNなどのfloat値の可能性があります。 xがNaNの場合、some_error（）に到達できるという結果を得たいと思います。だから私の質問は次のとおりです。私は非決定的山車をシミュレートする方法は？特定の関数呼び出しの到達可能性をテストするにはどうすればよいですか？

1熱

1答えて

Frama-cでCコードをスライス

私はframa-cで示されている未使用の変数をスライスしたいと思います。しかし、私はラインコマンドは考えが、私はhttps://frama-c.com/slicing.htmlに述べたように、1つのコマンドライン Last login: Thu Nov 9 20:48:42 on ttys000 Recep-MacBook-Pro:~ recepinanir$ cd desktop Recep

1熱

1答えて

WPは構造体へのポインタによって混乱します

私はWPが2つの構造体を交換する関数の事後条件を検証するのに苦労しています。 typedef struct { int x; int y; } pair; /*@ requires \valid({p, q}); assigns *p, *q; ensures *p == \old(*q); ensures *q == \old(*p); */ vo

3熱

1答えて

Ubuntu 14.04でFrama-c用のImpact Analysisプラグインをインストールするには？

私は、次のコマンドを使用して、Ubuntuの14.04でFRAMA-Cをインストール： sudo apt-get install frama-c しかし、私は次のコマンドを使用してFRAMA-CのGUIを開くとき： frama-c-gui を私は見つけることができません左側のウィンドウに "Impact Analysis"プラグインがあります。この図は私のFRAMA-Cの現在利用可能なプ

1熱

1答えて

Frama-Clangプラグインを使用したときのエラー

プラグインhttps://frama-c.com/frama-clang.htmlが開発の「初期段階」であると考えられたら、おそらく私は今や不運です。しかし、誰がこのような問題に遭遇した場合には不思議：レコードの [email protected]:~/code/c$ frama-c max.cpp [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_

1熱

1答えて

別のプラグインでWPの結果を使用するにはどうすればよいですか？

私はFrama-Cプラグインの作成に取り組んでいます。私のプラグインの中からWPを使って何かの弱い前提条件を得ることが可能かどうかを知りたいのですが？これまで、私は自分のプラグインでEVAプラグインの結果を使用するために、Db.Valueを使用しました。 WPのDb.Valueに類似したものはありますか？

2熱

1答えて

なぜcoqでスクリプトを生成したのかを証明する方法は？

私はframa-C WPを使用し、ACSLアノテーションをデバッグしたいと思います。緑色またはオレンジ色の結果があります。私はなぜIDE3を開き、生成されたスクリプトを参照してください。その後、リストから理論/目標を選択し、Alt-ErgoまたはCoq IDEを起動することができます。私はCoq IDEで生成されたコードで遊びたいです。私は、例えば、その後、その後、定理WP いくつかの公理を見て