--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2010 ---
Hollas Boris (CR/AEY1) wrote: > Consider a function that calls another function: > > Void f1(...) { > ... > K = f2(...); // (*) > ... > } > > I assume that if f2 has a contract (ie, pre- and postcondition as given by the user), this contract will be used by the verifier at the place of the function call. That is, the prover shows that > - the postcondition of f2 implies the wp derived so far > - the precondition of f2 is the new precondition for line (*). > > What happens if f2 isn't annotated? Will the call to f2 just be ignored by the verifier? > > the call to f2 cannot be "ignored". A default contract will be considered, with "true" as both pre- and post-condition. The main issue is for the assigns clause. in principle it should default to "everything" whatever it means. In the Jessie plugin, there are two cases: . If f2() is given an implementation, then an assigns clause which over-approximate the correct one is built from the implementation. In that situation you are safe. . If f2() has no implementation, then "assigns \nothing" is assumed. Caution should of course be taken. Hope this helps, - 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 |