Frama-C 23 和 Coq

Question

在 macOS 上安装 Frama-C (23)、Why3 和 Coq 后，我运行了命令

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

显示以下消息

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

• 这是否意味着我不能将 coq 与 Frama-C 一起使用？
• 如何指示 opam 编译上述 Why3 库？

问候

Answer 1

我想说，这可能更像是一个 Why3 问题，而不是 Frama-C 问题。不管怎样，你必须安装 Opam 包

why3-coq

，这样你才能为 Coq 编译 Why3 库（然后重新执行

why3 config detect

）。

Answer 2

事实上，

coq

和

why3-coq

都不是使用Frama-C/WP所必需的，除非你想用Coq履行一些证明义务。

安装一个或多个 SMT 求解器（cvc4、cvc5、z3、alt-ergo、colibri2...）就足够了。

但是，如果您真的想要在 Frama-C/WP 下使用 Coq --- 我不会推荐它 --- 安装

why3-coq

应该开箱即用。