--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on September 2013 ---
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>