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