--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Preservation of base loop invariant not verified



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>