On Thu, Jun 18, 2020 at 12:31:44PM +0100, Richard W.M. Jones wrote:
- Run /usr/lib64/why3/commands/why3config by hand (why isn't it
in
/usr/bin?), which creates $HOME/.why3.conf
So the reason it's not in /usr/bin is because you have to run it like
this:
$ why3 config --detect
Found prover Alt-Ergo version 2.0.0, OK.
Prover Coq version 8.11.2 is not known to be supported.
Known versions for this prover: 8.6, 8.6.1, ^8\.7\.[0-2]$, ^8\.8\.[0-2]$,
^8\.9\.[0-1]$, ^8\.10\.[0-2]$, ^8\.11\.0$.
Known old versions for this prover: 8.5, ^8\.5pl[1-3]$.
2 prover(s) added (including 1 prover(s) with an unrecognized version)
Save config to /home/rjones/.why3.conf
Although it still doesn't work.
It's possible to omit the -wp parameter and get frama-c to start up,
but it doesn't appear to be working correctly. In particular I
couldn't get it to prove anything about the example code.
Rich.
--
Richard Jones, Virtualization Group, Red Hat
http://people.redhat.com/~rjones
Read my programming and virtualization blog:
http://rwmj.wordpress.com
virt-df lists disk usage of guests without needing to install any
software inside the virtual machine. Supports Linux and Windows.
http://people.redhat.com/~rjones/virt-df/