問題タブ [frama-c]

OCamlでCヘッダーファイルを処理する方法としてframa-cを検討していました（たとえば、言語バインディングを生成するため）。非常によく文書化され、維持されているプロジェクトのように見えるので、魅力的です。ただし、ドキュメントを何度もグーグル検索して検索した後、目的に適したものを見つけることができません。これを行う正しい方法が欠けているだけですか、それともframa-cの範囲外ですか? 他のいくつかのプラグインと比較すると、それはかなり些細なことのように思えます。

Frama-C値分析を使用して、論理積（&&）ではなくビット単位のAND（＆）を使用して境界チェックが行われる大規模な生成Cコードを調査しようとしています。例えば：

Frama-C値分析は、配列アクセスについて不平を言います：

テストの前にアサーションを追加することで、小さな例でそれを幸せにすることができました：

増加しslevelますが、実際のコードではそれを行うことができません（大きすぎます！）。

誰かがこのアラームを取り除くために私が何ができるかについての考えを持っていますか？

（ところで、そのようにテストを書く理由はありますか？）

外部関数の動作、より正確にはそれらの終了を指定しようとしています。ACSLのドキュメントによると、\terminates p;プロパティでは、述語が保持されている場合pは関数が終了することが保証されていますが、保持されていない場合は何も指定されpていません。また、決して返されない関数は次のように指定できることも説明しています。

さらに、ACSLは\exits p;、突然終了した場合の事後条件を指定するプロパティを提供します。だから私は疑問に思っています：

関数が常に無限ループになるように指定しますか？

さらに、仕様は何ですか：

可能な無限ループに関する手段？

文字列の長さの公理を定義するときは、reads 句を使用する必要があります。

ただし、任意の領域の読み取り句は WP ではまだ実装されていません。他にどのような代替手段がありますか?

string.h からいくつかの関数を証明するために、この公理が必要です (例: strcmp)

ある種のエイリアス分析を行うframa-cプラグインの開発を始めたところです。私は Dataflow.Backwards 分析を使用していますが、さまざまな割り当てステートメントを調べて、左辺値に関する情報を収集する必要があります。

frama-c は 3 アドレス コードを提供しますか? 左辺値 (またはメモリアクセス) の形状について保証はありますか? つまり、soot や wala のように、a->b->c の場合、最大で 1 つのフィールド アクセス st があり、tmp=a->b のような一時変数が存在します。tmp->c;? マニュアルを確認しましたが、これに関するものは見つかりませんでした。

2つのループ不変条件を証明するのに問題があります：

\atが期待どおりに配列に対して機能していないと思います。

ACSL by Example（68ページ、swap_ranges）にも同様の関数があり、これを使用していますが、前述のように、WPプラグインでこの特定の関数を証明することはできませんでした。私は自分のマシンでそれを試しましたが、実際に同じ不変条件を証明することはできません。

完全なコード

編集

Frama-C Oxygenリリースを使用しており、alt-ergo（0.94）およびcvc3（2.4.1）を使用して自動証明を試しました

frama-cからの出力：

cvc3：

alt-ergo：

ACSL で C マクロに注釈を付けることは可能ですか?

例えば：

または次のような関数呼び出しも

私はすでにそれを試しましたが、成功しませんでした。私は何か間違ったことをしていますか、それとも単に不可能ですか?

構造体で \valid 注釈を正しく使用する方法について疑問があります。

構造体のメモリの安全性を検証する正しい述語は次のようになります。

また

\valid(p)最初の例では、 (構造体へのポインタである場所) がそれが指す構造体のメモリの安全性を保証することを前提としてpいますが、2 番目の例では (メモリ フィールドのサイズを考慮して) 範囲を手動で指定する必要があります。

例による ACSLのスタックの例(125 ページ) を参照してください。彼らは最初の例を採用しています。ただし、多くの場所\valid(some_string+(0..strlen(some_string)))で、これらの特定のメモリ位置でメモリの安全性を確保するために使用されます。

編集：

与えられた答えに応じて。このための正しいメモリ セーフティ述語 (stdio.h から取得)

たとえば、次のようになります。

私は Frama-C を初めて使用し、ACSL 構文を適切に学習したいと考えています。このダミーの例がありますが、Jessie プラグインは行番号 9 と 12 を検証できません。検証される関数 (等しい) は、2 つの配列 (a と b) が各インデックスで同じ値を持っているかどうかをチェックします。

FFS のソフトウェア実装を検証しようとしています。FFS の機能は、数値の最下位ビットのインデックス位置 (1 から始まる) を返すことです。ゴースト変数を使用するなど、さまざまな方法で試しました。ジェシーはそれを確認できず、理由がわかりませんか? いくつかの指針は本当に役に立ちます。これがコードのサンプルです。8ビットの数値を想定しています。