甚至對「死枝」做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讀取）。