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