Frama-C：在Cil謂詞中替換Cil術語

Question

使用Frama-C API中定義的Cil_datatypes模塊，我試圖用謂詞（Cil_datatype）中的新術語替換術語（Cil_datatype）。 要做到這一點，我需要映射一個謂詞與一個函數，當它發現的術語（或術語）在那裏取代它。你如何映射一個謂詞來替換一個術語？

Answer 1

我認爲您正在尋找the plugin development guide的第4.16節中描述的訪客機制。基本上，您繼承Visitor.frama_c_copy或Visitor.frama_c_inplace類，並重新定義vterm方法，以便在需要時返回修改的術語。要啓動訪問，您可以調用Visitor.visitFramacIdPredicate（或根據謂詞的確切類型使用類似的函數）以及您的類的實例和要修改的謂詞。

請注意，如果您進行就地修改，您的轉換可能會干擾Frama-C內核所做的註釋管理。因此，Visitor.frama_c_copy執行謂詞的深層副本更好。