--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: assigns needed to prove function contract?



Hi,
The absence of 'loop assigns i' is interpreted by 'loop assigns \everything' in the WP.
This means current values of i,a,a[..] and v.

Actually, this is not a problem for the loop because the loop invariant maintains all the necessary relations between all these variables locally.

However, modifying [v] at each loop that your loop invariant are to weak : they do not relate a[..] values with the v at the Pre state of the function, but with the current value of v at each loop iteration.

But, the value of v occurring in the post state is the one of the formal parameter, aka \at(v,Pre).
The same remark applies to variables a and n.

You can add the following invariants :

loop invariant n == \at(n,Pre);                                           
loop invariant a == \at(a,Pre);                                           
loop invariant v == \at(v,Pre);

to make your post-conditions provable, even with a missing loop assigns clause.

Jessie makes this kind of analysis and the (non-distributed) plugin GenAssigns infer missing assigns clauses like those.

L.

Le 9 sept. 2013 ? 09:42, David MENTRE <dmentre at linux-france.org> a ?crit :

> <find.c>