--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on January 2015 ---
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/e3471e50/attachment.html>