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] RTE array index bounds

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