--- layout: fc_discuss_archives title: Message 11 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



>> 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