GitLab

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?