甚至对“死枝”做Frama-c显示依赖关系

Question

我正在使用frama-c铝-20160502版本，我想在大型程序中找到依赖关系。在命令行中使用选项-deps时，我发现缺少一些依赖关系。特别是当几个条件加入一个条件时，只要一个条件为假，依赖性分析就会停止。在这个例子中的位置：

#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

邮资显示以下依存关系：

[从] ======相关内容COMPUTED ======

这些依赖关系在终止用于执行终止成立：

[从]功能主要： RES FROM A; B; ÿ

[从] ====== DEPENDENCIES ======

OF END因此它不会达到的条件C，因为已经B是假的。

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

任何想法？

Answer 1

From插件使用Value分析插件的结果。在示例中，A和B的值是足够精确的该值能够推断到达C之前该条件完全确定（因为&&操作者懒惰地评估，从左至右），因此C从不影响的结果，并因此不是From的观点的依赖。

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

user error: Call to Frama_C_interval in constant. 

你可以，但是，使用 “黑客”（并不总是最好的解决方案，但在这里工作）：

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

请注意，因为nondet是volatile，所以为每个变量A,B和C分配了不同的非确定性值。

在这种情况下，价值必须考虑条件句的两个分支，因此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 user manual的第6章所述，From插件计算功能性，命令性和操作性依赖性。这些做而不是包括间接控制依赖关系，正如你提到的那些，这些如X from A, B, C。对于那些，你需要PDG（程序依赖图）插件，但它目前没有依赖关系的文本输出。您可以使用-pdg来计算它，然后使用-pdg-dot <file>以点（graphviz）格式导出依赖关系图。这是我为你的main功能（使用挥发性黑客如前所述）：

最后，作为一个侧面说明：-slevel主要是用来提高精度，但在你的例子中，你已经有太多精度（也就是说，Value已经能够推断C永远不会被main读取）。