如何从Frama-C的WP插件生成Coq文件

排查及解决步骤 #

• 首先确认依赖包安装完整，对应你使用的版本，需要额外安装why3-coq包，该包包含Why3对接Coq所需的标准库导出文件，多数环境默认不会随Why3主包同步安装
• 执行why3 config show命令，检查输出中Coq条目对应的editor配置是否指向coqide可执行文件，部分环境默认会配置为其他文本编辑器，导致无法唤起Coq IDE
• 打开Frama-C GUI后，进入WP插件的设置面板，找到「证明器」选项卡，确认Coq证明器已被识别且状态为可用，优先使用Why3自动检测生成的条目，不要使用自定义配置的证明器条目
• 对需要手动证明的目标，右键选择「Prove by」→ 选择Coq，不要使用默认的自动证明器，此时会自动生成.v格式的证明上下文文件并唤起Coq IDE加载
• 如果上述操作后仍无响应，尝试在终端执行frama-c-gui -wp -wp-prover coq 你的测试文件.c，查看终端输出的错误信息，常见报错包括Coq路径权限问题、Why3生成的证明文件语法与当前Coq版本不兼容

注意事项 #

你使用的Frama-C 22.0、Coq 8.12.0、Why3 1.3.3的版本组合属于官方验证过的兼容组合，不存在版本匹配问题，无需降级或升级版本。如果之前自行修改过Why3配置文件，建议删除~/.why3.conf后重新执行why3 config --detect，再按上述步骤配置即可。

内容的提问来源于stack exchange，提问作者Tekkno