--- layout: fc_discuss_archives title: Message 6 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? > Please, look at the document "ACSL: ANSI/ISO C Specification Language", section 2.3.5 about "default contracts". Patrick Baudin.