如何使用Domain_builder模块？导入时提示Unbound module是什么原因？

问题原因 #

• Domain_builder确实未作为顶层模块被导出，也没有包含在旧版本EVA的公开签名中，因此无法直接open Domain_builder调用。
• 你可以正常使用Cvalue模块与EVA的导出规则无关：Cvalue是Frama-C数值分析的基础公共模块，被单独注册到全局顶层命名空间，不受Eva.mli导出范围限制。

解决方案 #

1. 如果你使用的是Frama-C 25.0（Manganese）及以上版本，该模块已经被加入EVA的公开导出列表，将你的x.ml代码修改为：

open Eva.Domain_builder

重新运行frama-c -load-script x.ml即可正常运行。
2. 如果你使用的是更早版本的Frama-C，Domain_builder属于EVA的内部模块，仅支持内部调用，若要外部使用需要自行基于Frama-C的开发源码编译你的扩展，不能通过-load-script直接加载。

内容的提问来源于stack exchange，提问作者Tom