frama-cによって生成されるpdgsの円ノードの意味

Question

私はframa-cツールを使用して以下のコードを分析します。

int main (int argc, char *argv[]) 
    { 
    int i,a; 
    for (i = 0; i < 100; i += 1) 
    { 
     a=0; 
     if (a==0) 
     { 
      continue; 
     } 
     else 
     { 
      break; 
     } 
    } 
    return 0; 
    } 

cmdは私の質問は、制御依存についてです

frama-c -pdg -dot-pdg graph main.c 

です。サークルノードとは何ですか？私はループが "i < 100"から始まるので、 "while"ノードを説明しようとします。おそらく、1つの時間ループを表しています。そのため、コントロールの依存関係（ "i < 100" ------ o "while" ）。私は正しいと思いますか？ "break"ノードの意味は何ですか？私はノード "goto __Cont;" "休憩"に関連している"else"ブロックの文。
私は、コントロールの依存関係を完全かつ正確に理解するために私の頭の中に明確な抽象モデルがないと思います。私を助けたり、何か提案してくれませんか？多くの先生のおかげでタオ。

Answer 1

コマンドを使用してくださいプログラムの翻訳方法については、を参照してください（私は以下の翻訳版を含みます）。

正規化されたバージョンの文goto __Cont;は、元のcontinue;の訳です。

そして、ビニラミンが述べたように、forループをwhileループに正規化した。

int main(int argc, char **argv) 
{ 
    int __retres; 
    int i; 
    int a; 
    i = 0; 
    while (i < 100) { 
    a = 0; 
    if (a == 0) { goto __Cont; } 
    else { break; } 
    __Cont: /* internal */ i ++; 
    } 
    __retres = 0; 
    return (__retres); 
} 

Answer 2

それのほとんどは自明である：

• 円 - フロー制御（分岐）
• 菱形 - 条件（a == 0等）
• 正方形 - あなたのループの割り当て

whileループに翻訳されました