[Why3-club] [Why-discuss] Why3 PVS backend and Jessie
Jean-Christophe.Filliatre at lri.fr
Wed Feb 29 08:47:38 CET 2012
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.
More information about the Why3-club