--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] complete behaviors



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