CODEWITHSUNDEEP
macoscoqframa-cwhy3
Night Heron
Night Heron

Reputation: 31

Frama-C 23 and Coq

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

Regards

Upvotes: 3

Views: 446

Answers (2)

Loïc Correnson
Loïc Correnson

Reputation: 36

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.

Upvotes: 1

Ksass'Peuk
Ksass'Peuk

Reputation: 757

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).

Upvotes: 2

Related Questions