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

  • Subject: [Frama-c-discuss] Problem with memset
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
  • Date: Wed, 2 Dec 2009 17:13:45 +0100
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