Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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