--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2019 ---
[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>