--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2012 ---
Hello, On Tue, Feb 7, 2012 at 5:51 AM, Henry <njucslzh0714 at gmail.com> wrote: > x = 0; > z = 10; > /*@ loop invariant ? int x; x>=0; > */ > while (x<=z) { > x++; > } > 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) > The \forall quantifier in your invariant means that "x" in the rest of the formula is not variable x from the program, but any int x. You mean to talk about the variable x of the program. For instance, like this: /*@ loop invariant 0 <= x <= (z+1) ; */ while (x<=z) { x++; } Frama-C Nitrogen with baseline Wp, together with alt-ergo 0.93, verify this invariant. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120207/542cb617/attachment.htm>