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



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