--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2015 ---
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>