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] Unable to ensure null

Hi everybody,

Yes the two warning are very dangerous, indeed the Typed+cast memory model is very dangerous and must be used with extra care.

Casting the \null pointer is never harmful. WP actually uses a special cast when converting zero to a pointer type. But here, there is double cast that is not taken into account, unfortunately. This is about to be fixed.

As a workaround, you should define NULL as 0L instead of (void *) 0L and your program works.

Back to the Typed+cast model, you must convince yourself that *ALL* casts are only used to hide the actual type of data, and never to implicitly convert data. For instance, it is illegal for this memory model to:
 - cast an (int *) into a (short *) to access the high and low word of a int ;
 - perform pointer arithmetic on a casted type, for instance (char *) (a + sizeof(int)) when a has type (int *) ;
 - asking for validity and separation on a casted type.

The only valid operations when you use the Typed+cast memory model are casting back the pointers to their origine type before access, validity and separation. Some special cases are authorized, for instance when viewing a struct with only int fields as an int array. In those special cases, the WP don?t warns you.

Each time the WP warns about potentially harmful casts, you should verify by manual code review that you are safe w.r.t to above considerations.

	L.






Le 2 juin 2014 ? 08:32, David MENTRE <dmentre at linux-france.org> a ?crit :

> Hello,
> 
> Le 30/05/2014 17:56, Ian Blissard a ?crit :
>> I have come across a situation where I cannot ensure that a pointer will
>> be null, and I am unsure what I am doing incorrectly.
> 
> You are using the wrong memory model of WP. Using Typed+cast, everything is proved.
> 
> I used following command line:
> frama-c -pp-annot -cpp-command="gcc -nostdinc -C -E -I. -I`frama-c -print-share-path`/libc" -wp -wp-rte -wp-model Typed+cast null_pointer.c
> 
> Two points still unclear to me:
> * Why is this memory model working? I don't know. WP documentation should help you.
> 
> * There is still a warning and I don't know if it is dangerous or not:
> """
> null_pointer.c:12:[wp] warning: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
> null_pointer.c:15:[wp] warning: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
> """
> 
> Best regards,
> david
> 
> _______________________________________________
> 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