類型檢查Frama-c

Question

我想知道Frama-C是否實現某種與指針相關的類型檢查。例如，考慮以下內容：

int x[10]; 
void * v = x; 

//@ assert isOfTypeInt(x, 10) 
//@ assert isOfTypeInt(v, 10) 

在精神上有沒有類似於上述內容？看看ACSL手冊，有許多方法可以檢查內存和指針的使用情況（其中一部分在Frama-C氧氣中實現）。儘管如此，我還沒有發現任何通用的支持來處理類型信息。是否有一個frama-c插件可用於此目的？

感謝， 愛德華

Answer 1

的確有ACSL沒有這樣的事情。事實上，C中的內存位置並沒有真正的類型信息：如果我們忽略潛在的對齊約束，任何4字節的塊都可以用來存儲32位整數。

也就是說，Frama-C是一個可擴展的平臺，並且總是可以爲特定需求編寫插件。對於簡單變量，例如x（在您的示例中），聲明的類型可以在AST中相應的varinfo的vtype字段中直接訪問。對於指針（如v），應該可以利用Value的結果來查看它們可能指向的位置，並使用它來導出適當的類型信息（主要的問題是在Value不精確時決定應該做什麼並提供多個潛在位置不同類型）。