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] [Jessie] loop invariant

Hello,

2013/9/17 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> After inserting the two annotations below, there were some not proved VCs
> (401/405):
> assigns Gbl_Eventos[9].Gbl_Ativo;

There is no "Gbl_Eventos" variable in the code you sent. You probably meant:

  assigns Eventos[9].Ativo;

> ensures (pri == 1) && (ID == 1) && (\old(Eventos[9].Ativo) == 0) &&
> average > 12.0 ==> Eventos[9].Ativo == 1;

I cannot test as I don't have Jessie installed so take my remarks with
a grain of salt.

Jessie loops are somewhat "opaque", so you need to state in loop
invariants properties that are true when entering the loop, even if
the loop does not modify this property, e.g. "loop invariant pri ==
1".

The best way to debug such cases is to add various assert in your code
to check that properties you think are true at a given code point are
indeed seen true by Jessie (or WP or Value analysis). You can for
example try to add "assert pri == 1;" before and within the for loop.

I hope it helps,
Best regards,
david