linux - 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。