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



Hollas Boris (CR/AEY1) wrote:
> 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
>
>
> _______________________________________________
> 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
>   
The only possible way currently is to provide a contract for each 
instance of type of pointers.

Typically, either p is a (char*) and you can give a contract without 
casts, or p is some larger data, int, double, structure, etc., and then 
'value 'is probably always 0, num must be a multiple of sizeof(*p). You 
can then specify the result values in term of the expected type.

- claude


-- 
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                    |