Skip to content

GitLab

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

Closed
Open
Opened Dec 04, 2020 by MARCHE Claude@marcheOwner

Allow user to customize drivers

Here is a short example of what a user of Why3 may want to do, but can't do it easily for the moment. Imagine I want to add a new symbol, that could have been already in Why3 stdlib but it is not. Say for example I want to add operators that given a bitvector of size 16, return the two bytes it is made of. As a user, I can define my own theory, say bvmisc.mlw, containing

theory T
use bv.BV8
use bv.BV16
function lsb BV16.t : BV8.t
function msb BV16.t : BV8.t
end

For my examples, I can import my own lib, using option -L for example. But in this case, I know that solvers like Z3 or CVC4 can support these operators very nicely. So I would like to make an complement to their drivers. I can design my own driver file, say my.drv, containing

theory bvmisc.T
syntax function lsb "((_ extract 7 0) %1)"
syntax function msb "((_ extract 15 8) %1)"
end

But then how am I supposed to tell why3, either for commands prove or ide, that I would like this driver addition to be used by my Z3 or CVC4? I couldn't find any satisfactory solution.

  • the -extra-config option is poorly documented, and trying to use with a file, say my.conf, containing
[prover_modifiers]
prover = "CVC4"
driver = "my.drv"

does not seem to do anything. Is it supposed to work?

  • What other alternative do I have?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#521