--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C native:coq



Hello,

when installing Frama-C 20 there is a message that mentions that the native:coq prover is deprecated.
Instead using ‘tip’ or ‘Why-3’ is suggested.
I understand what using ‘tip’ means but I do not understand the suggestion w.r.t ‘Why3’.
Does this mean to use coq through Why3? If so, how is it done?

Regards

Jens