--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 56, Issue 2



Hi,

Jessie is part of Why and Why-3 tools developed at INRIA Saclay.
Wp is a Frama-C plugin integrated in the public releases of Frama-C.

Wp aims to be more closely integrated with other plug-ins in Frama-C than Jessie.
More precisely, Jessie is difficult to combine with other Frama-C plug-ins.

Jessie seams to be easier to use than Wp for small programs and for training purpose.
Although, Wp should be used instead of Jessie for industrial use.

	L.

Le 3 janv. 2013 ? 10:16, intissar mzalouat a ?crit :

> Hello Jens,
> 
> Thank you for your answer.
> Could you, please, explain more the differences between jessie and WP?
> 
> Best regards,
> Intissar
> 
> 
> De : "Gerlach, Jens" <jens.gerlach at fokus.fraunhofer.de>
> ? : "<frama-c-discuss at lists.gforge.inria.fr>" <frama-c-discuss at lists.gforge.inria.fr> 
> Envoy? le : Jeudi 3 janvier 2013 10h09
> Objet : Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 56, Issue 2
> 
> Hello Intissar,
> 
> Jessie or WP make most sense on "small" functions (like those in "ACSL by Example").
> 
> By the way, as far as I know, Jessie is not actively maintained anymore.
> You should consider switching to WP.
> 
> Jens
> 
> > Message: 2
> > Date: Thu, 3 Jan 2013 08:55:18 +0000 (GMT)
> > From: intissar mzalouat <intissar_mzalouat at yahoo.fr>
> > To: "boris at yakobowski.org" <boris at yakobowski.org>,    "prubel at bbn.com"
> >     <prubel at bbn.com>,    Frama-C public discussion
> >     <frama-c-discuss at lists.gforge.inria.fr>,    Frama-C public discussion
> >     <frama-c-discuss at lists.gforge.inria.fr>
> > Subject: [Frama-c-discuss] long and complex program
> > Message-ID:
> >     <1357203318.25251.YahooMailNeo at web133006.mail.ir2.yahoo.com>
> > Content-Type: text/plain; charset="iso-8859-1"
> > 
> > Hello,
> > 
> > I have just started a new project to verify a C code using Frama C. I am facing so much problems.
> > Is it a good idea to verify a long and so complex C code using Frama C (jessie plug in)?
> > Could you answer me, please?
> > Could you share your experience?
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130107/bf9de9f8/attachment.html>