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