frama-c影響分析不能分析控制依賴性嗎？

當我使用frama-c分析我的c程序。似乎在frama-c的衝擊插件中存在一個錯誤。這是我的程序。frama-c影響分析不能分析控制依賴性嗎？

#include<stdio.h> 
int global; 
int main() 
{ 
    global = 12; 
    int result = 0; 
    if(global > 1) 
    { 
     result += 100; 
    } 
    else 
    { 
     result += 200; 
    } 
    return 0; 
}

我想查找變量「global」影響的所有狀態。顯然，聲明「result + = 100;」在與變量「全局」相關的「if條件」範圍內，因此語句「result + = 100;」應該是高光。但是，運行結果似乎不正確。

來源

2012-11-29 zhaizhiqiang

您能否提供導致您認爲不令人滿意的結果的確切命令行？ – Virgile

我想我明白了這是怎麼回事，但無論如何，如果沒有兩個相同的語句'result + = 100;'，你的例子會更清晰。或者，如果你沒有提到「結果+」=「100」的結果，就好像只有一個。 –

我假設您沒有使用特殊選項，並且您已經開始在Frama-C的GUI中對語句global = 12進行影響分析。如果不是這種情況，請提供更詳細的說明。

在您的程序中，if (global > 1)指令被選中，因爲語句global = 12與數據有依賴關係。但是，Impact插件未選擇result += 100語句。這是預期的行爲，因爲在這種情況下有沒有控制依賴關係。請注意0的else分支已經死亡。因此，執行result += 100並不真正取決於對if (global > 1)的評估，因爲條件總是如此。由於控制流總是達到result += 100指令，因此不存在控制依賴關係。

如果你想表現出在這個例子中控制依賴，最簡單的方法在於改變您的線路global = 12到

global = Frama_C_interval(0,100);

和文件$(SHARE)/frama-C/libc/__fc_builtin.c添加到命令行。這兩條指令result += 100和result += 200將在每種情況下由於控制依賴性而被選中。

來源

2012-11-30 00:24:02 byako

frama-c影響分析不能分析控制依賴性嗎？

回答

相關問題