0

我正在使用 frama-c Aluminium-20160502 版本，我想找出大型程序中的依赖关系。在命令行中使用选项 -deps 时，我发现缺少一些依赖项。特别是当多个条件合并为一个 if 时，只要一个条件为假，依赖性分析就会停止。在此示例中：

#include<stdio.h>
#include<stdbool.h>

/*Global variable definitions*/
bool A = true;
bool B = false;
bool C = true;
bool X;
bool Y;

bool res;


void main(){

        if (A && B && C) {
                res = X;
        }else res = Y;
}

当我尝试时：frama-c -deps program.c

frama 显示以下依赖项：

[来自] ====== 依赖项计算 ======

对于终止的执行，这些依赖项在终止时保持：

[来自] 函数 main: res FROM A; 乙; 是

[来自] ====== 依赖关系结束 ======

所以它没有达到条件C，因为B已经是假的。

我想知道是否有办法告诉 frama 计算所有依赖项，即使条件不满足。我尝试使用选项 -slevel 但没有结果。我知道有一种方法可以使用区间 Frama_C_interval(0,1) 但是当我使用它时，使用此函数的变量不会显示在依赖项中。我想让 X 和 Y 依赖于 A、B、C 和 res 依赖于 A、B、C、X、Y

有任何想法吗？

4

1 回答 1

0

From 插件使用 Value analysis 插件的结果。在您的示例中，A和的值B足够精确，以至于 Value 能够推断出条件是完全确定的（因为&&运算符是从左到右懒惰地评估的）C，因此C永远不会影响结果，因此不是依赖项从From的角度来看。

不幸的是，Frama_C_interval不能直接在全局初始化器中使用：

user error: Call to Frama_C_interval in constant.

但是，您可以使用“hack”（并不总是最好的解决方案，但在这里有效）：

volatile bool nondet;
bool A = nondet;
bool B = nondet;
bool C = nondet;
...

请注意，因为nondetis volatile，每个变量A和B都C被分配了一个不同的非确定性值。

在这种情况下， Value 必须考虑条件的两个分支，因此C在您的示例中成为依赖项，因为它可能C会在main. 然后，您将拥有：

       These dependencies hold at termination for the executions that terminate:
[from] Function main:
  res FROM A; B; C; X; Y

请注意，某些插件在处理 volatile 变量时需要特殊处理，因此这并不总是最好的解决方案。

然而，这仅处理某些类型的依赖关系。正如Value Analysis 用户手册第 6 章所述，From 插件计算功能性、命令性和操作性依赖关系。这些不包括间接控制依赖关系，X from A, B, C如您提到的那样。对于这些，您需要 PDG（程序依赖图）插件，但它目前没有依赖的文本输出。您可以使用-pdg它来计算它，然后-pdg-dot <file>以点（graphviz）格式导出依赖图。这是我为您的main功能得到的（使用前面提到的 volatile hack）：

主函数的PDG

最后，作为旁注：-slevel主要用于提高精度，但在您的示例中，您的精度已经过高（也就是说， Value 已经能够推断出C从未在内部读取main）。

于 2016-11-18T12:51:10.387 回答