--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on December 2009 ---
Hi Jens, the difference between your function and memset is that memset takes a void pointer to a memory location and returns that pointer. However, the buffer being pointed to is interpreted as an array of bytes. http://clc-wiki.net/wiki/C_standard_library:string.h:memset While this is awkward wrt type safety, a lot of embedded sw-developers use this function. My question is whether this can still be verified with Jessie. Regards, Boris ________________________________ Von: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] Im Auftrag von Jens Gerlach Gesendet: Mittwoch, 2. Dezember 2009 21:18 An: Frama-C public discussion Betreff: Re: [Frama-c-discuss] Problem with memset Boris, I think your function is similar to the following one (we called it fill_array). /*@ requires 0 <= length; requires \valid_range(a, 0, length-1); assigns a[0..length-1]; ensures \forall integer i; 0 <= i < length ==> a[i] == value; */ void fill_array (int* a, int length, int value ) { /*@ loop invariant 0 <= i <= length; loop assigns a[0..i-1]; loop invariant \forall integer k; 0 <= k < i ==> a[k] == value; */ for (int i = 0; i < length; i++) a[i] = value; } Simplify and Z3 can proof all 16 verification conditions. Regards Jens On Dec 2, 2009, at 5:13 PM, 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<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Dr.-Ing. Jens Gerlach http://www.first.fraunhofer.de/device_soft_en -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091203/08d8afe2/attachment.htm