--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] memset and non-chars



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>