--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on December 2009 ---
Hello Pascal, I've used this in a header file to verify memory safety of the caller: typedef unsigned char uint8; typedef unsigned int size_t; /*@ requires (\valid((uint8*)pDest +(0..num-1))) && @ (0 <= value <= 255) && @ (0 < num); @ ensures (\forall int i; 0 <= i < num @ ==> (((uint8*)pDest)[i] == value)) && @ (\result == pDest); @*/ extern void *memset( void *pDest, const int value, const size_t num ); However, Jessie reports Casting from type struct char_P * to type struct unsigned_char_P * not allowed in logic Maybe it's because void-pointers aren't supported, as Claude wrote. Having a contract for memset in a header file as you suggest would be sufficient because we don't want to verify the implementation of memset itself. Regards, Boris