--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verifications of calls to unannotated functions



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                    |