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

Hello Pascal,

I've used this in a header file to verify memory safety of the caller:

typedef unsigned char uint8;
typedef unsigned int size_t;

/*@ 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);
  @*/
extern
void *memset( void *pDest, const int value, const size_t num );


However, Jessie reports

 Casting from type struct char_P * to type struct unsigned_char_P * not allowed in logic

Maybe it's because void-pointers aren't supported, as Claude wrote. Having a contract for memset in a header file as you suggest would be sufficient because we don't want to verify the implementation of memset itself.

Regards,
Boris