--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on October 2014 ---
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.