--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2015 ---
Dear all, Since tabs apparently do not survive the mailing list process, I provide the same code below (also attached) but with spaces instead of tabs: #include <stdio.h> /*@ axiomatic loop28 { logic integer loop(integer k); axiom loop_base: loop(0) == 0; axiom loop_inductive: \forall integer k; k > 0 ==> loop(k) == k + loop(k - 1); } */ int main(void) { int i = 0; int j; //@ ghost int is_hello_printed = 0; /*@ loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0); loop invariant j >= 2 ==> i == \at(i, LoopEntry) + loop(j - 1); loop invariant j >= 8 ==> is_hello_printed == 1; loop assigns i, j, is_hello_printed; */ for (j = 1; j < 10; j++) { i += j; if (i == 28) { puts("Hello World!"); //@ ghost is_hello_printed = 1; } } //@ assert is_hello_printed == 1; } Best regards, Khairul On Sun, Jan 25, 2015 at 1:24 PM, Khairul Azhar Kasmiran <kazarmy at gmail.com> wrote: > Dear all, > > I'm trying to verify the following code with Frama-C and WP: > > #include <stdio.h> > > /*@ axiomatic loop28 { > logic integer loop(integer k); > axiom loop_base: > loop(0) == 0; > axiom loop_inductive: > \forall integer k; k > 0 ==> loop(k) == k + loop(k - 1); > } > */ > > int main(void) { > int i = 0; > int j; > //@ ghost int is_hello_printed = 0; > > /*@ loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0); > loop invariant j >= 2 ==> i == \at(i, LoopEntry) + loop(j - 1); > loop invariant j >= 8 ==> is_hello_printed == 1; > loop assigns i, j, is_hello_printed; */ > for (j = 1; j < 10; j++) { > i += j; > if (i == 28) { > puts("Hello World!"); > //@ ghost is_hello_printed = 1; > } > } > > //@ assert is_hello_printed == 1; > } > > Currently, all generated VCs are verified except the preservation of the > first loop invariant (i.e. the invariant with j==1).This is what Frama-C > generates for it: > > Goal Preservation of Invariant (file loop28_induct.c, line 17): > Assume { (* Domain *) Type: (is_sint32 i_3). } > Prove: i_3=(L_loop 0). > > which is obviously unprovable, but does suggest that the problem can be > fixed if an equation for i_3 can be provided. Indeed, if I add the > following loop invariant before all the other invariants: > > loop invariant i == \at(i, LoopEntry) + ((j - 1) * j) / 2; > > everything is verified, including all of the original invariants in the > code above. However, I don't want to do this, primarily because such > equations may not be available for other problems similar to this one. > > My questions: > 1. Why can't Frama-C verify the first loop invariant's preservation? > 2. What can I do to fix this, without involving the loop equation for i > stated above? > > I'm using Frama-C (Neon) with Alt-Ergo 0.99.1 and Z3 4.3.2. > > Best regards, > Khairul > > > > > -- > Dr. Khairul Azhar Kasmiran > Room C3-14, Department of Computer Science, > Faculty of Computer Science and Information Technology, > Universiti Putra Malaysia, > 43400 UPM Serdang, Selangor, > Malaysia. > Tel: +603 8947 1657 > Fax: +603 8946 6576 > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150125/102cf4e5/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: loop28_induct.c Type: text/x-csrc Size: 805 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150125/102cf4e5/attachment-0001.c>