--- layout: fc_discuss_archives title: Message 17 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?



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

> On 19/07/2019 16:53, Virgile Prevosto wrote:
>
> I'd say that encapsulating memcpy into a dedicated well-typed function
> with an appropriate contract
>
> Yeah... I was probably heading in that direction... thanks for the
> confirmation.
>
> I have obviously been spoilt by SPARK where you just write "D := S;" and
> it just works... :-)
>

Well, if you can afford to go by a (well-typed) assignment, there are much
less problems:

struct T {
  int x[2];
};

/*@ requires \valid(d) && \valid_read(s);
    requires \separated(d,s);
    ensures *d == *s;
 */
void h(struct T* d, struct T* s) { *d = *s; }

is proved pretty easily by WP. It's really the fact that memcpy exposes the
gory details of byte-by-byte memory accesses that is the source of the
issue.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190719/a9b5ab5b/attachment.html>