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

Question

当我使用 frama-c 分析我的 c 程序时。 frame-c 的影响插件中似乎存在一个错误。这是我的程序。

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

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

Answer 1

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

在您的程序中，if (global > 1)指令被选中，因为语句存在数据依赖性 global = 12 .然而，声明result += 100不会被 Impact 插件选中。这是预期的行为，因为在这种情况下没有控制依赖。请注意 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将被选中，在每种情况下都是因为控件依赖性。