c - 使用 Frama-C 进行值(value)依赖分析

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

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

// 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 自函数开始以来可能未更改，因此 (和 SELF)。

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