Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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