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] Validity of an array of struct

Hello,

2012/11/14 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> But Jessie produces 2 VCs related to pointer dereferencing. I think that it
> is necessary to write annotations to prove them, isn't?

Yes, but not those you're trying to write, which are redundant with
the fact the G_E is an array. See below.

>
> Wtih the follow annotation, I didn't get to run. I am using the Carbon
> version.
> The follow message is showed:
> "
> File "ro.jc", line 48, characters 48-61: typing error: unbound term
> identifier __framac_tmp1
> "

Any error that occurs in one of the files generated by the Jessie
plugin (.jc or .why) should be considered as a bug. That said, Carbon
is quite old, and it would be better if you could switch to Nitrogen
or Oxygen.

> I attached the source code. What is the solution for my verification?

In short, you can't prove anything with deductive verification
techniques if you don't provide loop invariants (and loop assigns[1])
for each loop in your program. In particular you must provide
appropriate bounds for the index i.

More precisely, in presence of a loop, the proof obligations are
abstracted with respect to the number of loop steps by saying that the
only things that are known about the locations that are modified in
the loop are what is in the invariants. In your case, we don't know
anything about i at the beginning of a step. When we are inside the
loop, we know that the test has been successful, thus that i<5: that's
why one half of the validity proof obligation can be discharged. On
the other hand, nothing in the code implies that i>=0, hence the
failure on the other half. i>=0 has to be established inductively (if
it's true at the beginning of a step, it is also true at the end, and
it is true initially), precisely what a loop invariant is for.

>   for(i=0;i<5;i++)
>   {
>         if(G_E[i].G_Ativo == FALSE && G_E[i].G_Inst_Ativ <= Tempo)
>             G_E[i].G_Ativo = TRUE;
>   }
> }

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile