--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2010 ---
>> Please, look at the document "ACSL: ANSI/ISO C Specification Language", >> section 2.3.5 about "default contracts". >To complete Patrick's answer, even if f2 is not annotated, it has a >contract (requires \true; ensures \true;), thus the schema you >described above still holds (of course, you'll have trouble proving >anything related to K after line (*)). However, I see a problem with a postcondition \true: Assume you have statements S; T in the code where S is a call of an unannotated function and T is some statement. Further, assume the verifier has shown {P} T {Q}, where P = wp(T,Q) is the weakest precondition of T wrt Q. Then, the verifier has to show that true -> P is valid, which means it has to show that P is valid. The problem I see is that the verifier will fail here. Maybe the verifier works differently? -Boris