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

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                    |