--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on September 2015 ---
Hi, Actually, memset, memcpy and such functions drives WP memory model into trouble. Using Typed+cast memory model is not a solution here: as (briefly) mentioned in the Manual, this memory model might be unsound, and should be used by expert users _only_. The correct workaround â that should be automated by a dedicated plugin â is to define a specialized function : struct S { int f ; int g ; } *p ; /*@ requires \valid(p); ensures p->f == 0 && p->g == 0; assigns *p ; */ memset_S(struct S *p); [...] { ⦠//REWORDED FOR WP: // memset(p,0,sizeof(struct S)); memset_S(p); ⦠} Just run WP with -wp-skip-fct=memset_S The price to pay the non-proved introduced function. There is actually no memory model in WP capable of proving this contract using an explicit call to the stdlib-memset function â there is no axiomatisation of datatype layout at the byte level in WP. L. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150907/f1faa62f/attachment-0001.html>