Search code examples
linuxcoqframa-c

Coq: Cannot find library Jessie_memory_model in loadpath

After running the following command frama-c -jessie max-anno.c, the GUI starts correctly, but then, when running Coq, I get the following output:

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; }

A screenshot of the issue:

Coq Cannot find library Jessie_memory_model in loadpath

It seems that "Jessie_memory_model" is missing, but I have no idea how to get it or where to install it.

EDIT: why3 version is 0.83.

Solution

  • Coq 8.4 is not supported by this version 0.83 of why3. Try to install other provers. I installed Alt-ergo and CVC3.