GitLab

I have been using Why3 1.3.1 (through Frama-C 21.1/WP dev) to generate verification conditions in PVS.

Today I tried to install Why3 in a different computer (both are Macs) via Opam.

$ opam install why3
The following actions will be performed:
  ∗ install why3 1.3.1

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
[why3.1.3.1] downloaded from cache at https://opam.ocaml.org/cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
∗ installed why3.1.3.1
Done.

The installation goes smoothly but it seems that something is missing in order to be able to use PVS.

$ why3 config --detect
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Save config to /Users/niauser/.why3.conf

When I try to use it, I get

$ frama-c test.c -wp -wp-prover pvs
[kernel] Parsing test.c (with preprocessing)
[wp] User Error: Prover 'pvs' not found in why3.conf
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

I've also tried why3 config --full-config with the same result.

$ why3 config --full-config
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Generating strategies:
  Prover Alt-Ergo 2.3.1 will be used in Auto level >= 1
Save config to /Users/niauser/.why3.conf

$ frama-c -wp-detect
[wp] Prover   Alt-Ergo 2.3.1  [alt-ergo|altergo|Alt-Ergo:2.3.1]
$

I don’t remember performing any special step during the installation on my other Mac.

Is there something else I should do in order to be able to use Why3 with PVS?