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

Guillaume Melquiond guillaume.melquiond at inria.fr
Wed Feb 29 09:54:45 CET 2012


Le mercredi 29 février 2012 à 08:47 +0100, Jean-Christophe Filliatre a
écrit :

> > 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.

I'm only guessing from the context, but if you only typed

  why3ml -P pvs pattern_trivial.mlw

then the error you got is expected. You have to point why3 at the
location of the jessie3 file. Take a look at the makefile generated by
jessie for more details. But it should basically be something like

  why3ml -I path/to/why/lib/why3 -P pvs pattern_trivial.mlw

Best regards,

Guillaume




More information about the Why3-club mailing list