--- layout: fc_discuss_archives title: Message 8 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?
>
>   
the call to f2 cannot be "ignored". A default contract will be 
considered, with "true" as both pre- and post-condition.

The main issue is for the assigns clause. in principle it should default 
to "everything" whatever it means.
In the Jessie plugin, there are two cases:

. If f2() is given an implementation, then an assigns clause which 
over-approximate the correct one is built from the implementation. In 
that situation you are safe.

. If f2() has no implementation, then "assigns \nothing" is assumed. 
Caution should of course be taken.

Hope this helps,

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |