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

  • Subject: [Frama-c-discuss] complete behaviors
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Wed Oct 15 18:46:01 2008
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: complete.c
Type: application/octet-stream
Size: 317 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081015/2dd69b9f/complete.obj
-------------- next part --------------



-- 

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