Frama-C：使用指針時獲取函數輸出

我需要獲取函數的所有輸出列表。當我使用From -plugin以下代碼Frama-C：使用指針時獲取函數輸出

void add(int *sum, int a, int b) 
{ 
    *sum = a + b; 
} 

int main() 
{ 
    int result; 
    add(&result, 1, 2); 
}

它告訴我，result是add函數的輸出。這當然是正確的，但我希望插件在某處提到sum。我知道sum是一個指針，並沒有修改該函數，所以它不是輸出，但*sum是修改，我想知道。有沒有簡單的（或任何）方法來實現這一目標？

來源

2016-08-31 DaviD.

爲什麼會提到'sum'，它是* local *的函數？ –

@DaviD。什麼是From-plugin？ –

@JohnBollinger我正在實現一個代碼轉換，在函數返回之前需要對所有函數輸出做些什麼。我知道'sum'是本地的，並且沒有被修改，但是它指向函數外的一個值，並且該值被修改並且因此是該函數的輸出。所以如果'sum'將被報告爲輸出，那將會非常好。 –

如果設置add作爲主入口點，你也許能夠檢索到您想要的信息：

$ frama-c -main add -deps file.c 
[...] 
[from] ====== DEPENDENCIES COMPUTED ====== 
    These dependencies hold at termination for the executions that terminate: 
[from] Function add: 
    S_sum[0] FROM sum; a; b

基本上，S_sum[0]是*sum：Value（上From依賴）生成的初始狀態這些指針可以是NULL，也可以指向一個名稱與指針相似的塊，默認情況下有兩個元素。有一些命令行選項可以調整默認行爲（有關更多信息，請參閱Value Analysis manual），但是您可能會發現，對於更復雜的示例，您需要編寫（或生成）包裝函數，以設置更復雜的初始狀態在調用函數之前。在這種情況下，您必須跟蹤哪些指針指向哪個位置才能重建信息。

堆積問題的是，在Value抽象狀態，sum被映射到可能位置的一組L（這裏減少到一個單），但是*sum不是一個對象本身。寫訪問將簡單地更新映射到L的元素的所有值。因此，從From的角度來看，一切看起來都是對result（或者如果更改入口點，則爲S_sum[0]）的修改。

來源

2016-08-31 16:50:39 Virgile

通過「包裝函數」，你的意思是我應該寫一個'add'的包裝器，在這裏我使用已知名稱作爲參數，比如'add（＆arg1，arg2，arg3）'，以便我可以翻譯'arg1 FROM sum;一個; b'到'* sum的總和;一個; B'？並且：使用OCaml綁定時是否適用相同的限制？無論如何，謝謝你的答案！ –

@DaviD。是的，這個上下文中的包裝函數是一個函數，它設置了一個適當的初始狀態並調用分析的真正入口點。儘管如此，我不確定你的意思是「使用OCaml綁定」。你想使用'Db.Value'和'Db.From'函數來代替輸出嗎？這確實是一個好主意，但是，同樣的限制適用：你不會在那裏看到'* sum'。 – Virgile

Frama-C：使用指針時獲取函數輸出

回答

相關問題