--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on October 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