--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on February 2012 ---
Hi, I encounter a problem about the plugin wp. Here given a simple program named b.c as follow void phase(void) { int x; int z; x = 0; z = 10; /*@ loop invariant ? int x; x>=0; */ while (x<=z) { x++; } return; } void main(void) { phase(); return; } Then the command "frama-c-gui -wp b.c" was executed. But I found that the status of the loop invariant was unknown because loop_inv_1_established could not decide. The proof obligation was: Goal store_phase_loop_inv_1_established: forall x_0:int. is_sint32(x_0) -> (0 <= x_0) I think the reason is that wp didn't consider the initial value of x. Can wp prove this invariant? Best wishes. Henry -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120207/b418750b/attachment.htm>