--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on December 2009 ---
For the moment it is not possible to handle (void*) properly in Jessie, so no chance to verify this code. I know that memset, memcpy, and such are used quite often in embedded code. When I encountered those, I gave them a contract that I believe correct, and proceed with the rest of the code. - Claude Hollas Boris (CR/AEY1) wrote: > This is a re-implementation of the memset function. It uses void-pointers as in C. > > typedef unsigned int size_t; > typedef unsigned char uint8; > > /*! > * \brief Standard Libc memset() function. > * \param[out] pDest Pointer to target buffer of length > * \a num bytes. > * \param[in] value Value to set in each byte of \a pDest. > * \param[in] num Number of bytes in \a pDest to > * set to \a value. > * \return Pointer to target buffer. > */ > > /*@ 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); > @*/ > void *memset( void *pDest, const int value, const size_t num ) > { > size_t i; > > /*@ loop invariant \forall int k; 0 <= k < i > @ ==> ((uint8 *)pDest)[k] == (uint8)value; > @*/ > for( i=0; i < num; i++ ) > { > ((uint8 *)pDest)[i] = (uint8)value; > } > > return pDest; > } > > > > When I try to verify it, Jessie reports > > string.c:31:[jessie] user error: Casting from type struct char_P * to type struct unsigned_char_P * not allowed in logic > string.c:31:[jessie] warning: Dropping definition of function memset > string.c:19:[jessie] user error: Casting from type struct char_P * to type struct unsigned_char_P * not allowed in logic > [jessie] warning: Unsupported feature(s). > Jessie plugin can not be used on your code. > > > This error message puzzles me as there are no structs. Can a function that is equivalent to the memset function built into C be verified with Jessie? > > -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 > -- 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 |