--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on February 2010 ---
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?