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] Warnings for call to memcpy()... why?

Hello again,

Le ven. 19 juil. 2019 à 17:14, Roderick Chapman <rod at proteancode.com> a
écrit :

> On 19/07/2019 13:13, Virgile Prevosto wrote:
>
> Generally speaking, WP is quite bad at handling memcpy and other functions
> of its ilk
>
> OK. In that case, what is the preferred and correct method for performing
> assignment of a whole array in Frama-C?
>

I'd say that encapsulating memcpy into a dedicated well-typed function with
an appropriate contract should let you contain the problem: you will not be
able to prove the contract (as a matter of fact, only the prototype of the
wrapper matters, its definition can be put on another .c file which can be
ignored by Frama-C WP[1]) but you will be able to use it in the main proof.
For instance, with unsigned char, you'd end up with the following
(untested):

/*@ requires \valid(d+(0 .. n-1));
       requires \valid_read(s+(0 .. n-1));
        requires \separated(d+(0 .. n-1), s+(0 .. n-1)
        assigns d[0 .. n-1];
        ensures \forall integer i; 0<= i < n ==> d[i] == s[i];
*/
void uc_memcpy(unsigned char d, unsigned char s, size_t n);

int f (...) {
...
uc_memcpy(new_array, old_array, size);
...
}

Obviously, if you use memcpy over arrays of several distinct types, you'll
need one specialized version for each type, which will quickly become quite
tedious. As said before, this would probably be much more easily handled by
a code transformation performed by a script/plugin, but unfortunately this
script does not exist yet.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
[1] Eva or E-ACSL would probably need to have the definition as well,
though.
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190719/03131f33/attachment-0001.html>