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

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                    |