5

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

    #include<stdio.h>
    int main()
    {
        int n,i,m,j;
        while(scanf("%d",&n)!=EOF)
        { 
            m=n;
            for(i=n-1;i>=1;i--)
            {   
                m=m*i;
                while(m%10==0)
                {
                     m=m/10;
                }
                m=m%10000;
            }  
            m=m%10;
            printf("%5d -> %d\n",n,m);
        }
       return 0;
    }

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

    frama-c -pdg -dot-pdg main main.c 
    dot -Tpdf main.main.dot -o main.pdf

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

4

1 に答える 1

6

C プログラムのスライサーは、その定義された目標が定義済みの実行を保持することであり、スライサーが未定義の実行を変更できる場合にのみ実際に機能します。

そうしないと、スライサーは、その時点でそれが有効なポインターであるとx = *p;判断できなくなるとすぐに、ステートメントを削除できなくなります。ステートメントが削除された場合、実行場所がその時点で NULL は変更されます。pxp

Frama-C は、 などの複雑なライブラリ関数を処理しませんscanf()。このため、ローカル変数nが初期化されずに使用されていると考えられます。

次frama-c -val main.c のような警告が表示されるはずです。

main.c:10:[kernel] warning: accessing uninitialized left-value:
               assert \initialized(&n);
...
[value] Values for function main:
      NON TERMINATING FUNCTION

この単語assertは、Frama-C のオプション-valがすべての実行が定義されていると判断できないことを意味し、「NON TERMINATING FUNCTION」は、プログラムの単一の定義された実行を見つけて続行できないことを意味します。

初期化されていない変数の未定義の使用が、PDG がほとんどのステートメントを削除する理由です。PDG アルゴリズムは、未定義の動作である variable への最初のアクセスであると判断した後に発生するため、それらを削除できると考えていますn。

プログラムを少し変更して、scanf()呼び出しをより単純なステートメントに置き換えました。

#define EOF (-1)
int unknown_int();

int scan_unknown_int(int *p)
{
  *p = unknown_int();
  return unknown_int();
}

int main()
{
  int n,i,m,j;
  while(scan_unknown_int(&n) != EOF)
    { 
      m=n;
      for(i=n-1;i>=1;i--)
      {   
        m=m*i;
        while(m%10==0)
        {
          m=m/10;
        }
        m=m%10000;
      }  
      m=m%10;
      printf("%5d -> %d\n",n,m);
    }
  return 0;
}

以下のPDGを取得しました。私が知る限り、それは完全に見えます。あなたがより優れたレイアウト プログラムを知ってdotいて、フォーマットを受け入れる場合dot、これはそれらを使用する良い機会です。

複雑な PDG 最外側の状態はご了承whileくださいtmp != -1。グラフのノードは、プログラムの内部正規化表現のステートメントです。条件tmp != -1には、ステートメントのノードへのデータ依存関係がありますtmp = unknown_int();。で内部表現を表示するとframa-c -print main.c、最も外側のループ条件が次のように分割されていることがわかります。

  while (1) {
    int tmp;
    tmp = scan_unknown_int(& n);
    if (! (tmp != -1)) { break; }

これは、とりわけ、複雑なステートメント全体を保持する代わりに、複雑なステートメントの削除可能な部分のみを削除するスライスに役立ちます。

于 2012-03-25T14:17:03.667 に答える