c - 为什么 Frama-C 的这个使用 scanf() 的程序的依赖图看起来像这样？

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

结果是 我的问题是为什么语句“m=m*i;”，“m=m%10000”没有映射到节点。结果似乎不对，因为代码中有三个循环。

Answer 1

C 程序的切片器只有在其定义的目标是保留已定义的执行，并且允许切片器更改未定义的执行。

否则，一旦无法确定 p 是一个有效指针，切片器将无法删除诸如 x = *p; 的语句到那一点，即使它知道它不需要 x，只是因为如果删除该语句，那时候 p 为 NULL 的执行将被更改。

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这个词的意思是Frama-C的选项-val无法确定所有的执行都被定义，而“NON TERMINATING FUNCTION”则表示无法找到一个已定义的程序执行以继续。

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

除其他外，这有助于切片以仅删除复杂语句中可以删除的部分，而不必保留整个复杂语句。