勒柯克：找不到庫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。