CODEWITHSUNDEEP
frama-cwhy3
Dominic Mulligan
Dominic Mulligan

Reputation: 466

Compilation of FromInt.v failing on MacOS (trying to use wp plugin with Coq)

If I try:

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

then I get the following error:

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.

(all other files before FromInt.v seem to compile successfully). This behaviour persists even after uninstalling and reinstalling why3 and frama-c packages via opam.

Does anybody know how to fix this?

I'm using MacOS High Sierra. Relevant version info: Why3 platform, version 0.88.3, OCaml toplevel, version 4.05.0, Frama-C Phosphorus-20170501c02v53d5hv2r, and Coq Proof Assistant, version 8.7.0 (December 2017), all installed through opam.

Upvotes: 0

Views: 46

Answers (0)

Related Questions