--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on September 2013 ---
Hello Lo?c, 2013/9/9 Lo?c Correnson <loic.correnson at cea.fr>: > 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. Thank you for the clear explanation. > Jessie makes this kind of analysis and the (non-distributed) plugin GenAssigns infer missing assigns clauses like those. Maybe it would be interesting for WP to gain such capabilities, at least from a user point of view. ;-) Or maybe you have some use case in mind that need some manual writing of loop assigns. Sincerely yours, david