是否可以在frama-c中指定緩衝區訪問子句？

假設我有以下功能：是否可以在frama-c中指定緩衝區訪問子句？

void process_data(uint32_t * data, size_t length) { 
    for (size_t i = 0; i < length; i++) { 
     foo(data[i]); 
    } 
}

我怎麼能告訴郵資-C「這個功能，確保每次訪問data[i]滿足條件i < length」？據我所知，我可以在每行代碼data附近放置斷言，但有沒有更好的方法？

來源

2016-12-15 John Doe

問題給你 - 是絕對保證，'data'將是非NULL並指向'uint32_t'的集合？在進入'for'循環之前可能需要斷言？ – t0mm13b

是的，'data'是'\ valid'，它指向一個uint32_t的數組。 –

「這個功能確保...」是什麼意思？在我看來，你想說「這個功能需要......」（否則，你有無效的內存訪問），不是嗎？ – Anne

要防止無效的內存訪問，您需要檢查是否始終使用data指針調用此函數，從中可以讀取至少length元素。所以，你需要寫一個前提條件：

//@ requires \valid_read (data + (0 .. length-1)); 
void process_data(uint32_t * data, size_t length) {

所以，如果你能保證這個屬性是有效的，它保證你不會有任何無效的內存訪問。

來源

2016-12-16 09:28:13 Anne

也許我在解釋這個時太不清楚了，對不起。當'process_data'函數可能會在'length'維度之外訪問'data'時，我希望frama-c wp失敗。例如，如果'process_data'包含語句'uint32_t a = data [length + 1]''，則檢查失敗。 –

@JohnDoe恐怕答案取決於你對Frama-C的使用。例如，如果你想用'-wp-rte'來使用WP，Anne的註解就是你所需要的：因爲WP只知道在需求中寫的是什麼，所以任何訪問大於'length'的索引都會導致RTE註釋中的未知狀態。如果您使用Value並且使用大於'length'的緩衝區調用'process_data'，則需要更多特定註釋，您必須提供自己（或通過自定義腳本）提供的更多特定註釋。隨時優化您的問題，以便我們可以提供適當的答案。 – Virgile

這解釋了它。我以爲需求條款隻影響價值分析，謝謝。 –

是否可以在frama-c中指定緩衝區訪問子句？

回答

相關問題