c - 型チェックとコード パターン検出、Frama-C

Question

私は Frama-C ソフトウェアを発見しました。ダブル if テストや、特定の関数の呼び出しの後に常に別の関数が続くなどのコード パターンを検出できるかどうか疑問に思っていました。

または、変数名を使用する何か、たとえば、特定の接頭辞が付いた名前の変数が特定のタイプに属しているかどうかを確認するなどです。

Frama-C で (ACSL を使用するか、新しいモジュールを開発することによって) 可能だと思いますか?

どうもありがとう =)

Answer 1

doubled if テストなどのコード パターンを検出する

外側の if の結果であるため、内側の if の条件が常に true であるパターンを意味する場合、GUI はelse、値の分析中に内側の if の分岐が到達不能であることが判明したことを既に示している可能性があります。

簡単な例:

int x, y;

int main(int c){
  if (c == 2)
    {
      x = x * c;
      if (c == 2)
        {
          y = y * c;
        }
      else
        {
          y = y / c;
        }
    }
}

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

$ frama-c-gui -val t.c

これはヒューリスティックにのみ使用できます。関連する変数が変更されていない実行パスによって分離された冗長テストのサウンド検出器は、値分析の結果を利用するプラグインとして実装できます。

特定の関数の呼び出しの後には常に別の関数が続くこと。

これは、 Aoraïを使用して可能です。これは、(編集済み:) Frama-C ディストリビューションに含まれている Frama-C プラグインであり、その Web ページの主張にもかかわらずです。Aoraï は、表現された一時的なプロパティに対応する証明義務を生成します。これらの義務を証明することは多かれ少なかれ難しいかもしれません。ある意味では、Aoraï は一時的なプロパティを検証する問題を Frama-C にプラグインがある別の問題に還元するだけです。

指定された接頭辞が付いた変数が特定のタイプに属しているかどうかを確認します。

このタイプの「コーディング標準」チェックは、Frama-C プラグインとしても実装できます。Atos は、エアバスのコーディング ルールを検証するために、 Tasterという名前のプラグインを実装しました。