--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RTE array index bounds



On Tue, 7 Oct 2014 09:03:09 +0200
Virgile Prevosto <virgile.prevosto at m4x.org> wrote:

> Hello,
> 
> 2014-10-07 5:26 GMT+02:00 Mansour Moufid <mansourmoufid at gmail.com>:
> 
> > I would like to prove that indices to access an array are bounded
> > properly, using the WPE plugin, after reading data into the array.
> >
> >     $ frama-c -pp-annot -wp -wp-rte bar.c
> >     ...
> 
> Just as a side note, there is a WP plugin and a RTE plugin (to
> generate the assertions that must be verified to ensure that there is
> no runtime errors), but no WPE plugin. Anyway, your command line is
> clear enough to show what you want to do.
> 
> > function is always less than or equal to its third argument, so I add
> > the following annotation above the main function:
> >
> >     /*@ ensures \result <= nbyte; */
> >     ssize_t read(int fildes, void *buf, size_t nbyte);
> >
> 
> You are on the good track. It is indeed important that all the
> functions called by the function you are trying to verify have a
> proper contract (you might want to add assigns ((char *)buff)[0 ..
> (nbyte - 1)) \from fildes, nbyte;  to constrain the side-effects of
> read. However, this is not sufficient. You must also provide some
> indications about the effects of the loop:
> 
> > for (j = 0; j < (size_t) i; j++) {
> >            if (buffer[j] == '\n') {
> >                buffer[j] = '\0';
> >                break;
> >           }
> >        }
> 
> In particular here, since we know that j is unsigned, hence always
> non-negative, and less than i (because otherwise we would exit the
> loop), the only thing that we need is to tell WP that i remains
> unchanged during a loop step. This can for instance be done with a
> loop assigns:
> 
> /*@ loop assigns buffer[0..j-1], j; */
> 
> As a rule of thumb, you must provide loop assigns (and often
> additional loop invariants) for any loop in your code (as well as
> function contracts as mentioned above).
> 
> Best regards,
> -- 
> E tutto per oggi, a la prossima volta
> Virgile

Thank you! I just finished reading the documentation about loop
annotations, that's exactly what I was missing.

I am more and more impressed with Frama-C every day.