MacOS下使用Coq插件时FromInt.v编译失败求助

我碰到过类似的版本兼容问题，你的错误本质是Frama-C Phosphorus版本的WP插件和Coq 8.7的实数库结构不匹配导致的。Coq 8.7对实数模块做了重构，IZR这个常量从Reals.Raxioms移到了Reals.RIneq里，而老版本的Frama-C WP还在引用旧的路径。下面给你几个可行的解决办法：

临时修复：手动修改生成的Coq文件 #

因为WP每次运行都会在临时目录生成FromInt.v，你可以先定位到报错里的文件路径（/var/folders/m5/pq77jvw12md76t51_6t51vfwhptwwy/T/wp7149b4.dir/coqwp/real/FromInt.v），把第22行的：

Require Import Reals.Raxioms.

改成：

Require Import Reals.RIneq.

然后重新运行Coq编译这个文件就能继续验证了。不过这个方法是一次性的，下次运行Frama-C又会生成新的临时文件，适合快速验证你的ACSL代码逻辑是否正确。

长期方案：安装版本匹配的依赖 #

Frama-C Phosphorus（2017年的版本）是针对Coq 8.6及更早版本开发的，和Coq 8.7存在兼容性冲突。你可以用opam创建一个独立的环境来安装适配的版本：

1. 创建并切换到新的opam环境：

   opam switch create frama-c-phosphorus ocaml-base-compiler.4.05.0
   eval $(opam env)
   

2. 安装对应版本的Coq和Frama-C：

   opam install coq.8.6.1 frama-c.phosphorus-20170501
   

3. 确认版本匹配：

   frama-c -version  # 应显示Phosphorus-20170501
   coqtop -version   # 应显示8.6.1
   

这个环境里的依赖完全匹配，之后运行你的验证命令frama-c -val -wp -wp-rte -wp-prover coq acsl-case-study.c就不会再出现这个错误了。

推荐方案：升级Frama-C到新版本 #

如果你的项目没有必须用旧版Frama-C的限制，我强烈建议升级到更新的Frama-C版本（比如2020年后的版本），这些版本已经适配了Coq 8.7及以上的实数库结构，同时还会带来更多功能和bug修复：

1. 先卸载现有依赖：

   opam remove frama-c why3 coq
   

2. 创建新环境并安装新版本（以Frama-C 2022为例，你可以根据需求选择最新稳定版）：

   opam switch create frama-c-latest ocaml-base-compiler.4.14.1
   eval $(opam env)
   opam install frama-c coq.8.15.2
   

升级后记得检查你的ACSL代码，少数旧版的语法可能在新版本里有细微调整，但大部分情况下都是兼容的。

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