Tag: frama c

Frama-C anagram函数行为validation

我写了一个C函数，检查两个给定的字符串（C风格）是否是字谜。 我尝试用Frama-Cvalidation它，但它不能validation函数的最终行为（其他规范是有效的）。 第一个进入超时（即使WP中的超时值非常高），第二个未知。 这是代码： #include //@ ghost char alphabet[26] = {‘a’, ‘b’, ‘c’, ‘d’, ‘e’, ‘f’, ‘g’, ‘h’, ‘i’, ‘j’, ‘k’, ‘l’, ‘m’, ‘n’, ‘o’, ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘u’, ‘v’, ‘w’, ‘x’, ‘y’, ‘z’}; /*@ // Takes a character and return it to lowercase if it’s uppercase axiomatic ToLower { logic char to_lower(char […]

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”块中的语句。 我认为我没有明确的抽象模型来完全准确地理解控制依赖性。 […]