1

我已经安装了frama-c 和why3，但是当我尝试启动frama-c 时，jessie3 出现错误。

frama-c -verbose 2
[kernel] warning: cannot load plug-in `Jessie3' (incompatible with Neon-20140301).
The exact failure is: error loading shared library:
/usr/local/lib/framac/plugins/Jessie3.cmxs: undefined symbol: camlGzip

我没有找到有关 camlGzip 的任何信息，因此它可能是任何配置文件中的错误（它可以是 camlzip），但我没有找到它的声明位置。

编辑：我试图在 Jessie3.cmxs 中修改 camlzip 中的 camlGzip，但是当我启动 frama-c 时它会产生分段错误

我的 frama-c 和 Why3 版本：

frama-c -version
Version: Neon-20140301

why3 --version
Why3 platform, version 0.85 (build date: Wed Oct 29 10:42:47 CET 2014)

我在 Mint17 虚拟机上工作，每个程序的 ./configure 和 make 都没有错误

我希望有人已经遇到过这个问题并且可以帮助我

4

1 回答 1

0

我刚刚遇到了这个问题并修复了它。您必须安装 Why-2.34 才能将 jessie 安装到您的 frama-c 库中。从此链接下载：https ://opam.ocaml.org/packages/why/why.2.34/

我在编译它时遇到了一些麻烦，因为我必须删除 coq 才能成功编译它。顺便说一句，任何人都知道我应该如何报告 coq 编译错误，请帮忙。

另外如果你有Why3.85，我建议你降级到3.83，因为它似乎是Why.2.34唯一认可的版本。

干杯。

于 2014-12-01T00:50:22.050 回答