問題タブ [frama-c]

私は Frama-c を初めて使用するので、この簡単な例の問題点を理解したいと思います。

この例では、Frama-c (WP + 値) は関数コントラクトの assign 句を証明せず、その理由がわかりません。どんな助けでも大歓迎です=）

cygwin に frama-c をインストールしようとすると、次のエラーが表示されますが、解釈できません。それらを解釈するのを手伝ってくれますか、それとも情報を入手できる場所へのリンクを教えてくれますか?

coqc と ocaml はどちらも最新バージョンです。

ポインターを入力として取り、ポインターが NULL でないときにその内容を使用する関数の依存関係について、ACSL 仕様を作成する必要があります。この仕様は正しいと思います：

しかし、私はむしろ動作を避けたいと思いますが、これが正しい（そして同等である）かどうかはわかりません：

場合でも*p右の部分で使用できますか?\frompNULL

Frama-C ツールによって作成された抽象構文ツリー (AST) にアクセスしたいと考えています。Frama-C で AST にアクセスするためのプラグインまたはその他のサポートはありますか?

オフセットマップの値を出力するこの関数が機能しています。

ここで、値を文字列変数に取得して、目的に合わせて変換したいと思います。に置き換えFormat.fprintf fmtましたPrintf.sprintfが、機能しません。コンパイル エラー:

Frama-C を使用してある種の前方条件付きスライシングを実行できるかどうかを知りたいのですが、これをどのように達成できるかを理解するためにいくつかの例を試しています。

不正確なスライスになると思われるこの単純な例がありますが、その理由がわかりません。スライスしたい関数は次のとおりです。

この仕様を使用する場合:

Frama-C は、「f -slice-return」基準と f をエントリ ポイントとして使用して、次のスライス (正確です) を返します。

しかし、この仕様を使用する場合:

その後、すべての命令 (& 注釈) が残ります (このスライスが返されるのを待っていたとき:

)

最後の場合、スライスは不正確ですか? この場合、何が原因として考えられるでしょうか？

よろしく、

ロマン

編集：「else if(a != 0) ...」と書きましたが、「else ...」に問題が残ります