--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2008 ---
Hi, As other features in ACSL that Frama-C supports, it is not yet implemented in the Jessie plugin. I understand the fact Jessie does not currently document its limitations is a big problem, this will be corrected by the next release. Yannick On Wed, Oct 15, 2008 at 6:45 PM, Jens Gerlach < jens.gerlach@first.fraunhofer.de> wrote: > Hi, > > I have a questions about complete behaviours. > Does Frama-C check whether the behavior are really complete? > In the following spezification of abs I intentionally ommited the > specification for negative arguments, > but I also stated that the behaviors would be complete. > Nevertheless Jessie (alt-ergo, CVC3, Yices(SS)) prove that the > implementation of abs is correct. > Is there something I haven't understood about "complete"? > > Best regards > > Jens Gerlach > > > > > > -- > > Dr.-Ing. Jens Gerlach > Eingebettete Systeme - EST > Tel.: +49 (0)30 6392 1841 > Fax.: +49 (0)30 6392 1805 > E-Mail: jens.gerlach@first.fraunhofer.de > > Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST > Kekul?stra?e 7 > 12489 Berlin > Germany > http://www.first.fraunhofer.de > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081015/7a5c761d/attachment.html