爲什麼這個scanf（）的依賴圖 - 使用Frama-C的程序看起來像這樣？

Question

我使用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 

結果是 我的問題是爲什麼statments 「M = M * I;」， 「M = M％10000」 沒有映射到節點。結果看起來不正確，因爲代碼中有三個循環。

Answer 1

C程序的切片機只有在其定義的目標是 到保留定義處決，和切片機允許變化不確定的執行工程實踐。

否則，切片機將無法儘快刪除的語句，如x = *p;，因爲它是無法確定p是在這一點上一個有效的指針，即使它知道它不需要x，只是因爲如果該語句被刪除，p在那個點上的執行被改變。

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意味着郵資-C的選項-val無法確定所有執行的定義，與「非結束函數」意味着無法找到要繼續執行的程序的單個定義執行。

未定義的未初始化變量的使用是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; } 

這有助於，除其他事項外，切片只刪除一個複雜語句的部分，可以被刪除而不必保留整個複雜的語句。