frama-c - 在 MacOS 上编译 FromInt.v 失败（尝试将 wp 插件与 Coq 一起使用）

Question

如果我尝试：

frama-c -val -wp -wp-rte -wp-prover coq acsl-case-study.c 

然后我收到以下错误：

File "/var/folders/m5/pq77jvw12md76t51_6t51vfwhptwwy/T/wp7149b4.dir/coqwp/real/FromInt.v", line 22, characters 15-32:
Error: The reference Reals.Raxioms.IZR was not found in the current
environment.

（FromInt.v 之前的所有其他文件似乎编译成功）。即使在通过 opam 卸载并重新安装 why3 和 frama-c 软件包后，此行为仍然存在。

有谁知道如何解决这个问题？

我正在使用 MacOS High Sierra。相关版本信息：Why3 平台，版本 0.88.3，OCaml 顶层，版本 4.05.0，Frama-C Phosphorus-20170501c02v53d5hv2r，和 Coq Proof Assistant，版本 8.7.0（2017 年 12 月），均通过 opam 安装。