マグネシウムの-rteオプションでの不自然な動作

Question

マグネシウムバージョン（ubuntuから直接インストールされています）の-rteオプションでインコヒーレントな動作に直面しています。私は誰かがその問題を認識しているのか、私が何か間違っているのかどうか疑問に思っています。

私は、配列の外に誤ったアクセス権を持つプログラムを持っています。 frama-c-guiでオプションと値の分析を行わないと、範囲外アクセスが検出され、対応する注釈がオレンジ色の円で表示されます。 -rteオプションを使用すると、2つのアノテーションが表示され（配列の下限と上限）、両方に緑色の円が表示されます（これは誤りです）。

/*@ assert rte: index_bound: 0 ≤ cpt; */ 
/*@ assert rte: index_bound: cpt < 5; */ 

コンソールは言う：

tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid. 

は、私は彼らの両方が同じ「名前」を持っているので、2つの注釈の間に不一致がある疑いがある：index_bound。

また、誤ったアクセスを含むループの後のコード部分は赤色で色分けされています。これは、以前のエラーのために解析できないと解析が正しく推測したことを示しています。ここで

は私のプログラムである：ここでは

int main(){ 
    int t[5] = {1,2,3,4,5}; 
    int cpt =0 ; 
    int tmp ; 
    while (cpt<10){ 
    tmp = getchar() ; 
    if (t[cpt] > tmp) 
     { return 1 ; } 
    cpt++ ; 
    } 
    return 10 ; 
} 

は（frama-c-gui -rte tableau_erreur.cを使用して）私のディスプレイのキャプチャです。

私はバグトラッカーを見ていたが、それの痕跡を見つけることができませんでした：私は結果が正しい-rteオプション（オレンジ色の円）を使用していない場合は

。私はそれをテストするためにFrama-Cのより新しいバージョンをコンパイルすることはできませんでした。

Answer 1

更新：この現象は、FRAMA-C（rte: index_bound: cpt < 5をアサートに関連する状態は不明ままである）のシリコンリリースで修正されています。

---

私はあなたが言ったこと正確再現することができませんでしたが、あなたのコマンドのようにGUIを起動した後、バリュー分析パネルで、「ファイル名を指定して実行」ボタンをそしてクリックすると、私は緑の弾丸を得ました。

これは実行中のframa-c-gui -rte -then -valに相当し、緑色の（間違った）箇条書きも表示されます。

実際、これは現行のFrama-Cバージョンでも問題であると思われるので、バグレポートが順調です。同等の注釈（//@ assert cpt < 5;）を手動で挿入すると、黄色の箇条書きが表示されることに注意してください。また、ループをアンロールすると（たとえば、-slevel 5）、黄色の弾丸が表示されます。この問題は、特にRTEプラグインの使用に関連しているようですが、いずれにしても調査されます。

副題では、プロパティの横にあるindex_boundラベルは識別子ではなく、ラベルであり、したがって一意ではなく、ここでの問題とは関係ありません。

技術的詳細：FRAMA-Cを使用するかもしれない（ソースコードの隣に弾丸に要約するが、いずれかプロパティパネルを介してさらに詳細に説明されている特性と状態の概念を、有します一部のフィルタを変更して、Refreshボタンをクリックするか、レポートプラグイン（例：frama-c -val -then -report）をクリックする必要があります。あなたの例では、ループの最初の反復は0であるcptの値を持ちます。したがって、プロパティはvalidステータス（緑色の箇条書き）を取得し、最後の反復では（cptが5の場合）、unknownステータス）。なんらかの理由でそれはvalidとして（誤って）統合されていました。ただし、値ログにはfile.c:8:[value] warning: assertion 'rte,index_bound' got status unknownと表示されます。これはGUIのMessagesパネルに表示されます。これはエラーの説明ではありませんが、メッセージとプロパティパネルの組み合わせは、プロパティの問題を診断する強力なツールです。