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

Nuno Gaspar nmpgaspar at gmail.com
Wed Feb 29 10:58:11 CET 2012


slightly out of topic: Are there any plans for Isabelle support?

2012/2/29 Guillaume Melquiond <guillaume.melquiond at inria.fr>

> 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
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>



-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible
life choice.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120229/f6a75157/attachment.htm>


More information about the Why3-club mailing list