--- layout: fc_discuss_archives title: Message 23 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



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