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

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
> 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/20091202/995811a6/attachment-0001.htm