Coq：在加载路径中找不到库 Jessie_memory_model

Question

在运行以下命令 frama-c -jessie max-anno.c 之后，GUI 正确启动，但是，当运行 Coq 时，我得到以下输出：

Welcome to Coq 8.4pl4 (July 2014)
Warning: Cannot open /usr/local/lib/why3/coq-tactic
File "/tmp/why_d206da_maxmnanno_T_WP_parameter_max_ensures_default.v", line 9, characters 0-28:
Error: Cannot find library Jessie_memory_model in loadpath
why3cpulimit time : 1.000000 s

最大-anno.c:

/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
int max(int x, int y) { return (x > y) ? x : y; }

问题截图：

似乎 "Jessie_memory_model" 不见了，但我不知道如何获得它或在哪里安装它。

编辑：why3 版本是 0.83。

Answer 1

why3 的 0.83 版本不支持 Coq 8.4。尝试安装其他验证器。我安装了 Alt-ergo 和 CVC3。

Coq：在加载路径中找不到库 Jessie_memory_model

Coq: Cannot find library Jessie_memory_model in loadpath

linux

coq

frama-c