2012-03-25 45 views
5

我使用Frama-C工具來生成這個程序的依賴關係圖(main.c)。爲什麼這個scanf()的依賴圖 - 使用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 

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

回答

6

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格式,這是一個很好的機會使用它們。

Complex 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; } 

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

相關問題