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



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?