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; }
这有助于,除其他事项外,切片只删除一个复杂语句的部分,可以被删除而不必保留整个复杂的语句。