Frama-C未绑定模块Z构建错误

Jon*_*her 4 ocaml frama-c

使用Ubuntu 14.04,我下载了Neon Frama-C发行版,并安装了所需的工具:labgtk,sourceview等.我配置Frama-C没问题,但是在构建得到了:

File "external/unz.ml", line 39, characters 10-19:
Error: Unbound module Z
make: *** [external/unz.cmo] Error 2
Run Code Online (Sandbox Code Playgroud)

问题是

 let n = Z.of_bits str in
Run Code Online (Sandbox Code Playgroud)

其中Z表示未导入的模块(我猜).我不知道Z应该引用什么,所以我无法试图解决这个问题.

Vir*_*ile 7

你安装了zarith库(libzarith-ocaml-dev在Ubuntu下)吗?Frama-C可以使用两个库来获得任意精度整数:或者Bignum,它包含在OCaml发行版中(虽然我不会感到惊讶,Debian/Ubuntu确实设法使它成为一个单独的包),或者Zarith更新,更有效的实现.unz.ml是绑定Zarith到Frama-C 的代码的一部分 ,因此如果您没有Zarith安装,您将遇到一些问题进行编译.

通常,./configure应该注意选择合适的库.你可以查看它的内容config.log.可能的问题是您已libzarith-ocaml安装软件包但未安装软件包libzarith-ocaml-dev.在这种情况下,库本身是安装的(并且可能是由它检测到的./configure),但不是编译代码所需的头文件.