Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>