--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with memset



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