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”块中的语句。
我认为我没有明确的抽象模型来完全准确地理解控制依赖性。 你能帮我或给我任何建议吗? 非常感谢涛先生。
使用命令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); }
大多数是自我解释:
- 圈 – 流量控制(分支)
- 菱形 – 条件(
a == 0
等) - 广场 – 分配
你的for循环被转换为while循环