Frama-C 23 and Coq

Question

After installing Frama-C (23), Why3, and Coq on macOS I ran the command

rm -f ~/.why3.conf ; why3 config detect

The following message was shown

Found prover Coq version 8.10.2, but no Why3 libraries were compiled for it

• Does this mean I cannot use coq with Frama-C?
• How do I instruct opam to compile the above mentioned Why3 libraries?

Regards

Answer 1

I would say that it might be more a Why3 question than a Frama-C question. Anyway, you have to install the Opam package why3-coq so that you have Why3 libraries compiled for Coq (and then re-execute why3 config detect).

Answer 2

As a matter of fact, neither coq nor why3-coq are necessary to use Frama-C/WP, unless you want to discharge some proof obligations with Coq.

Installing one or several SMT solvers (cvc4, cvc5, z3, alt-ergo, colibri2, ...) is sufficient.

However, if you really want to work with Coq under Frama-C/WP --- I would not recommend it --- installing why3-coq should work out-of-the-box.