私が試してみると：
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 を介してインストールされます。