勒柯克：找不到库Jessie_memory_model在loadpath

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 

MAX-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

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