--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on February 2012 ---
Missing also : @loop assigns x ; since the loop is modifying x. L. Le 7 f?vr. 12 ? 05:51, Henry a ?crit : > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss