2

当我使用 frama-c 分析我的 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;
}

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

4

1 回答 1

3

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

在您的程序中，该if (global > 1)指令被选中，因为该语句存在数据依赖性global = 12。result += 100但是，影响插件不会选择该语句。这是预期的行为，因为在这种情况下没有控制依赖性。请注意，else分支if已死。因此， 的执行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-30T00:24:02.893 回答