在旧版本中使用 Frama-c 程序时我有一些问题。它使用函数varinfo_from_vid ()来获取varinfo. 在更改日志中我看到它已被删除，可以使用 varinfo 索引的映射或哈希表来获取它。我不太了解，因为我是 cil 和 frama-c 的新手。这是否意味着我需要自己保留一个 ( vid, varinfo) 哈希表并将其传递给每个使用过的函数variunfo_from_vid()？或者还有其他方法可以做到这一点。如果有人有例子或建议，我将不胜感激。谢谢
问问题
41 次
1 回答
3
插件应该转换为varinfo直接保存，而不是int代表vida 的字段varinfo。没有充分的理由只存储该vid字段，这与 Frama-C 的内部结构（尤其是项目）效果不佳。
如果插件包含由int(IntHash.t或Datatype.Int.Hashtbl.t) 索引的表，而键实际上是vid，则它们也应该被由varinfo( Cil_datatype.Varinfo.Hashtbl.t) 索引的表替换。有关 Frama-C 中数据类型的更多信息，请参见Frama-C 开发人员手册的第 4.9.2 节。
于 2014-04-04T06:45:22.343 回答