2012-03-25 46 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; } 

这有助于,除其他事项外,切片只删除一个复杂语句的部分,可以被删除而不必保留整个复杂的语句。

相关问题