我正在尝试创建一个frama-c插件.这个插件取决于Frama-c Value插件.我想获取并打印C源代码中所有左值的值集.为了做到这一点,我想使用Value.Eval_exprs,Value.Eval_op等中可用的函数Eval_exprs.lval_to_precise_loc
.
不幸的是我无法找到在我的插件中使用这些功能的方法.我尝试按照Frama-c插件开发指南的4.10.1节(通过.mli文件注册)中提到的步骤添加PLUGIN_DEPENDENCIES:=Value
到我的Makefile中,但我注意到该Value.mli
文件为空,并且没有通过此文件公开任何功能.之后我查看db.ml
了kernel
目录中的文件,找不到任何可用于访问Eval_exprs,Eval_op等中可用功能的模块.
有没有办法从其他插件访问Value插件的这些功能?