--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on December 2009 ---
Hollas Boris (CR/AEY1) wrote: > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > The only possible way currently is to provide a contract for each instance of type of pointers. Typically, either p is a (char*) and you can give a contract without casts, or p is some larger data, int, double, structure, etc., and then 'value 'is probably always 0, num must be a multiple of sizeof(*p). You can then specify the result values in term of the expected type. - claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |