[Why3-club] [Why-discuss] Why3 PVS backend and Jessie

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Feb 29 08:47:38 CET 2012

Hi Pierre-Loïc,

On 28/02/2012 04:42, Pierre-Loïc Garoche wrote:
> we are at least a few interested in the PVS backend of
> Frama-C/Jessie/Why. While we were going to start contributing,
> François (Bobot) pointed to us that the PVS driver was already part
> of the git head.

You are obviously referring to Why3, not Why 2.xx, thus why3-club might 
have been a more appropriate list for such a question. I CC it.

Anyway, the answer is simple: François has been too hasty :-)

I indeed started a PVS support in Why3 recently, but it is not 
completed. Currently, its sole purpose is to help the PVS developers 
adding declaration-level polymorphism in PVS, which we'll use to have a 
natural PVS support in Why3 (otherwise, it's a pain: you have to produce 
many theories with distinct sets of type parameters). Thus the PVS 
driver produces syntax for a *forthcoming* version of PVS.

That being said, the PVS driver should already work fine on a purely 
monomorphic task (no polymorphism at all in the context and the goal). 
And the current PVS version (5.0) should accept the resulting file. If 
this is not the case, please report a bug.

Note: you are not the only one willing to use PVS in the Frama-C/Jessie 
toolchain, and we have put some friendly pressure on the PVS team to be 
able to do that soon.

> I tried to use this backend with Frama-C: #1 frama-c -jessie
> -jessie-behavior default -jessie-atp why3ml -jessie-gen-only
> pattern_trivial.c #2 jessie -why3ml -locs pattern_trivial.cloc
> pattern_trivial.jc #3 why3ml -P pvs pattern_trivial.mlw
> But I obtained the following error: Library file not found: jessie3

Regarding jessie3 and Frama-C, Claude will answer, I guess. And such a 
question could even go to the Frama-c-discuss mailing list. But please 
do not mention the PVS driver there; that's definitely premature.

Best regards,

More information about the Why3-club mailing list