問題タブ [frama-c]

システムにframa-cをインストールしました。

それが何をするか、それはすべての私のコードをCのすべての暗黙の変換でより拡張された形式に変換します。

（例）
//私の実際のコード

//Frama-c変換されたコード

今私の疑問は、 オブジェクトプログラムを作成する前に、Cコンパイラがすべての暗黙的な変換を行うかどうかです。

また

オブジェクトプログラムの作成中に、これらの暗黙の変換が並行して行われるかどうか。

また

実装に依存しますか？もしそうなら、なぜですか？

Frama-Cオープンソースプロジェクトで実験をしたいと思っており、Windows7マシンにツールをインストールしたいと思います。以前のバージョンにはWindows用のバイナリインストーラーがあるようですが、最新バージョンのNitrogenにはソースコードしかありません。プロジェクトframa-c.comのWebサイトには、これらは利用可能であるはずだと書かれていますが、ダウンロードページには表示されません。バイナリインストーラーは他の場所で利用できますか？

Frama-C ツールを使用して、このプログラム (main.c) の依存グラフを生成します。

コマンドは次のとおりです。

結果は、 私の質問は、ステートメント「m=m*i;」、「m=m%10000」がノードにマップされない理由です。コードに 3 つのループがあるため、結果は正しくないようです。

私はframa-cツールを使用して以下のコードを分析します。

cmdは

私の質問は、コントロールの依存関係についてです。サークルノードとはどういう意味ですか？「while」ノードについて説明しようとしています。ループは「i<100」から始まるため、制御依存関係があります（「i<100」------o「while」）。 ）。私が推測することは正しいですか？しかし、「ブレーク」ノードとはどういう意味ですか？そのノードは「goto__Cont;」だと思います。「休憩」に関連しています。「else」ブロックのステートメント。
コントロールの依存関係を完全かつ正確に理解するための明確な抽象モデルは頭の中にないと思います。私を助けてくれませんか、それとも何か提案をしてくれませんか？事前タオに感謝します。

私はFrama-Cの初心者ユーザーであり、ポインターに対するアサーションに関していくつか質問があります。

以下のCフラグメントについて考えてみます。

• 2つの関連するデータ構造DataとHandle、stHandleにはDataへのポインターがあります。
• いくつかの架空の操作が完了したかどうかを示すデータの「状態」フィールド
• 3つの関数：init（）、start_operation（）、wait（）;
• 上記を使用し、6つのアサーションを含むmain（）関数（A1-A6）

さて、なぜA5とA6はWPベリファイア（ "frama-c -wp file.c"）でアサートできないのですか？start_operation（）の最後の "ensures"句のために保持されるべきではありませんか？

私は何が間違っているのですか？

一番、

エドゥアルド

Macで窒素バージョンのFrama-cを使用していますが、ACSLマニュアルに記載されているように、「設定」ロジックを使用できないようです。たとえば、「//@」のようにゴースト変数を宣言できません。 ghost set <integer>someSet;"。

frama-cプログラムは、セットが宣言されている行の構文エラーについて、何があっても常に文句を言います。

また、「set」の代わりに「Set」を試し、「integer」の代わりに他のタイプ（「char *」など）を使用して、「//@openset;」を指定しました。モジュールをインポートします。

たぶん私はいくつかのコマンドラインオプションを指定する必要がありますか？「frama-c-kernel-help」を実行すると、それがどうなるかは明確ではありません。

または、Macバージョン（Intelバイナリバージョンをダウンロードした）が古くなっているため、最新のソースコードをコンパイルする必要がありますか？

感謝をこめて、

エドゥアルド

モデル変数は Frama-C マニュアル (仕様と「実装」バージョンの両方) で説明されています。

ただし、マニュアルにあるような単純なフラグメントを解析することはできません。

あるいは

解析エラーにつながります。

モデル変数は本当にサポートされていますか? もしそうなら、私は何を間違っていますか？私が使用しているframa-cのバージョンは、MacOSのNitrogenです。

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

実際にスレッド化された C コードを評価するために、frama-c 値アナライザーを試しています。発生する可能性のあるスレッドの問題を無視して、単一のスレッドの可能な値を調べるだけです。これまでのところ、エントリ ポイントをスレッドの開始位置に設定することで機能します。

ここで私の問題: あるスレッド内で、別のスレッドによって書き込まれた値を読み取ります。これは、frama-c がスレッド化を考慮していない (またすべきではない) (現在のところ)、変数が広い範囲にあると想定しているためです。範囲は実際にははるかに小さいです。値アナライザーにこの変数の値の範囲を伝えることは可能ですか?

例：

ここで、frama-c は x が揮発性であり、したがって [--..--] の範囲を持っていることを検出しますが、他のスレッドが x に何を書き込むかを知っているので、アナライザーに x が 0 または 1 しかできないことを伝えたいと考えています。特にGUIで、これはframa-cで可能ですか？

前もってありがとうクリスチャン

2 つの外部関数 init() と revoke() があるとします。Init() は「有効な」値を返し、revoke() はそれらを無効にします。use() が、初期化されているが取り消されていない値のみを使用していることを確認したいと思います。このプロパティを述語 (ランダムなセッション ID と考えてください) またはそれ以外として説明する方法がわかりません。

frama-cの要件としてocamlgraphをインストールしようとしています。ocamlgraphをインストールしてmakeを実行すると、次のコンパイルエラーが発生します。

私はUbuntu-10.04で実行していて、同じエラーでocamlgraph-1.6バージョンとocamlgraph-1.8.2バージョンを試しました。私のマシンのocamlバージョンはocaml-3.11.2です。

ありがとう