Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
F
frama-c
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 14
    • Issues 14
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • pub
  • frama-c
  • Issues
  • #21

Closed
Open
Opened Jul 27, 2020 by Mariano Moscato@moscato

No Why3 libraries compiled for PVS

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?

To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#21