Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Preservation of base loop invariant not verified
  • From: kazarmy at gmail.com (Khairul Azhar Kasmiran)
  • Date: Sun, 25 Jan 2015 13:24:04 +0800
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>