なぜこのscanf（）の依存グラフは、Frama-Cのプログラムを使っているのですか？

Question

私はこのプログラム（main.c）の依存グラフを生成するためにFrama-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 

結果である 私の質問ですなぜたstatments "M = M * I;"、 "M =メートル％10000" にマップされませんノード。コードに3つのループがあるため、結果は正しくないようです。その定義された目標は に保存する定義された実行で、スライサーは変更未定義の実行に許可されている場合は、Cプログラムのための

Answer 1

スライサーは、実際に動作します。

そうでない場合、スライサーはすぐにpが理由だけであれば、それはそれはxを必要としないことを知っている場合でも、その時点で有効なポインタであると判断することができないようなx = *p;などの文を削除することができないであろうステートメントが削除され、その時点でpがNULLの実行が変更されます。

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終端FUNCTION」はそれことを意味していることを意味し続行するプログラムの単一の定義された実行を見つけることができません。

初期化されていない変数の未定義の使用は、PDGがほとんどのステートメントを削除する理由です。 PDGアルゴリズムは、変数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フォーマットを受け入れる場合は、これを使用するのがよいでしょう。

なお、最も外側の条件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; } 

これは、とりわけ、そのことができ、複雑な文の一部のみを除去するためのスライスを支援します複雑なステートメント全体を保持する代わりに削除することができます。