pdma中由circlema-c生成的圆节点的含义是什么

我使用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;的翻译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

大多数是自我解释：

• 圈 – 流量控制（分支）
• 菱形 – 条件（ a == 0等）
• 广场 – 分配

你的for循环被转换为while循环