使用 Frama-C 进行价值依赖分析

Question

在下面程序的最后，变量 x 的值取决于变量集 {x,y,z,c}。同样，变量 y 的值取决于变量集 {y,c}。

int main(){
    int x = 100;
    int y = 50;
    int z = 20;
    int c = g();

    if (c){
        x += y + 1;
    }else{
        x += z + 1;
        y = y + 1;
    }

    return 0;
}

我可以从命令行的 Frama-c 工具中获取此信息吗？如果是，如果有人可以帮助我，我将不胜感激。

Answer 1

您可以尝试使用frama-c -pdg -pdg-print选项。它调用 PDG（Program Dependence Graph）插件。但是您需要解码神秘的输出。

您还可以使用 -pdg-dot 选项使用 dot 图形格式（来自 Graphviz）获得更友好的表示。

Answer 2

您无法从您提供的 main 函数上的 Frama-C 现有插件之一获得此结果。但是，如果您稍微修改一下代码，插件 From 将 return 提供您想要的信息。

// test.c
int x = 100;
int y = 50;
int z = 20;

extern int c; // unknown value

int main(){

    if (c){
        x += y + 1;
    }else{
        x += z + 1;
        y = y + 1;
    }

    return 0;
}

frama-c -deps test.c

[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function main:
  x FROM x; y; z; c
  y FROM y; c (and SELF)
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======

x 的结果不言自明。对于 y，您会得到额外的信息，即 y 自函数开始以来可能未发生变化，因此 (and SELF).

通过 main 初始化变量得到不同结果的原因是 -deps 分析计算其结果 w.r.t。函数开始时的状态。在您的 main 中，由于 x、y 和 z 设置为常数值，因此它们的最终结果仅取决于 c，而 c 又仅取决于g 读取的内容以计算其结果。

使用 Frama-C 进行价值依赖分析

Value Dependency Analysis with Frama-C

c

dependencies

frama-c