--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2010 ---
Claude Marche wrote: > . If f2() has no implementation, then "assigns \nothing" is assumed. > Caution should of course be taken. > It seems that Virgile's answer invalidates this. Virgile is right, sorry for the mistake: Frama-C kernel infers a clause that is not "assigns \nothing". It remains true that caution should be taken, because there is no guarantee that the generated clause is correct! Generally speaking, all functions without implementation should be given a contract. By the way, any suggestion welcome. E.g., do you think Jessie should reject functions without either an implementation or a contract? - claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |