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



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.