c - 由frama-c生成的pdgs中的圆节点是什么意思

Question

我使用 frama-c 工具来分析下面的代码。

  int main (int argc, char *argv[])
  {
     int i,a;
     for (i = 0; i < 100; i += 1)
     {
        a=0;
        if (a==0)
        {
            continue;
        }
        else
        {
            break;
        }
     }
     return 0;
  }

命令是

   frama-c -pdg -dot-pdg graph main.c

我的问题是关于控制依赖。圆节点是什么意思？我试着解释一下while节点，可能代表一次循环，因为一个循环是从"i<100"开始的，所以有一个控制依赖("i<100"------o "while").我猜对了吗？但是“中断”节点是什么意思？我猜那个节点“goto __Cont;”与“休息”有关； “else” block 中的语句。
我想我脑子里没有清晰的抽象模型来完整准确地理解控制依赖性。你会帮助我或给我任何建议吗？非常感谢 Tao。

Answer 1

使用命令 frama-c -print main.c 查看程序是如何翻译的(我在下面包含了翻译版本)。

规范化版本中的语句goto __Cont;是原文中continue;的翻译。

而且，正如 Binyamin 所说，for 循环被规范化为 while 循环。

int main(int argc, char **argv)
{
  int __retres;
  int i;
  int a;
  i = 0;
  while (i < 100) {
    a = 0;
    if (a == 0) { goto __Cont; }
    else { break; }
    __Cont: /* internal */ i ++;
  }
  __retres = 0;
  return (__retres);
}