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

cmd是

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

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

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

Answer 2

其中大部分是不言自明的：

• circle - 流量控制（分支）
• 菱形 - 条件（a == 0等）
• 平方赋值

您的 for 循环已转换为 while 循环