frama-c影响分析不能分析控制依赖性吗？

当我使用frama-c分析我的c程序。似乎在frama-c的冲击插件中存在一个错误。这是我的程序。frama-c影响分析不能分析控制依赖性吗？

#include<stdio.h> 
int global; 
int main() 
{ 
    global = 12; 
    int result = 0; 
    if(global > 1) 
    { 
     result += 100; 
    } 
    else 
    { 
     result += 200; 
    } 
    return 0; 
}

我想查找变量“global”影响的所有状态。显然，声明“result + = 100;”在与变量“全局”相关的“if条件”范围内，因此语句“result + = 100;”应该是高光。但是，运行结果似乎不正确。

来源

2012-11-29 zhaizhiqiang

您能否提供导致您认为不令人满意的结果的确切命令行？ – Virgile

我想我明白了这是怎么回事，但无论如何，如果没有两个相同的语句'result + = 100;'，你的例子会更清晰。或者，如果你没有提到“结果+”=“100”的结果，就好像只有一个。 –

我假设您没有使用特殊选项，并且您已经开始在Frama-C的GUI中对语句global = 12进行影响分析。如果不是这种情况，请提供更详细的说明。

在您的程序中，if (global > 1)指令被选中，因为语句global = 12与数据有依赖关系。但是，Impact插件未选择result += 100语句。这是预期的行为，因为在这种情况下有没有控制依赖关系。请注意0的else分支已经死亡。因此，执行result += 100并不真正取决于对if (global > 1)的评估，因为条件总是如此。由于控制流总是达到result += 100指令，因此不存在控制依赖关系。

如果你想表现出在这个例子中控制依赖，最简单的方法在于改变您的线路global = 12到

global = Frama_C_interval(0,100);

和文件$(SHARE)/frama-C/libc/__fc_builtin.c添加到命令行。这两条指令result += 100和result += 200将在每种情况下由于控制依赖性而被选中。

来源

2012-11-30 00:24:02 byako

frama-c影响分析不能分析控制依赖性吗？

回答

相关问题