--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and type casting



Hi,

This is a question that was actually answered before, so I going to quote
it here:

> On a side note related to the new memory model. What implications arise
from using the unsafe castsoption?

Basically, you must verify by hand that unsafe castsare never used to
*store* data through a *modification* of aliased memory data layout.
For instance :

{
   int * p = ... ;
   char * q1 = (char *) p ;
   char * q2 = (char *) p ;
   if ( q1== q2 ) { .... } // CORRECT
   if ( *q1 == *q2 ) { .... } // CORRECT
   q1[2] = 0xFF ; // STILL CORRECT BUT ...
   if ( *p == ... )    // INCORRECT, because q1 is aliased to internal
representation of p

}

Regards,

A seg, 16/03/2015, 10:34, Filip Niksic <fniksic at mpi-sws.org> escreveu:

> Hi all,
>
> The WP manual mentions that the WP's Typed memory model supports limited
> casts. There is also an option for unlimited casts, but this is said to
> cause unsoundness. I was wondering if someone could elaborate on these
> points. What exactly is meant by "limited casts"? How does unsoundness
> emerge with unlimited casts? Perhaps someone could give an example?
>
> Thanks,
>
> Filip
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150316/20e7707a/attachment.html>