--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2015 ---
> 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? The Typed memory model assumes that atomic types (int, float, pointers) are never split into small pieces (bytes), and never overlap with each others. Aggregates, like struct and arrays, are decomposed into such atomic types, such that eg. 'struct { int f ; int g; }' is actually laid out like ?int [2]?. Whenever a cast is consistent with these constraints, it is automatically accepted and correctly interpreted by the Typed memory model. Other casts are normally rejected, with an error message displaying the actual layout of pointer types in terms of atomic types. However, to cope with C-polymorphism implemented by using (void *) casts, it is sometimes necessary to admit other casts. Provided you check by hand that you still use the memory following the restriction of the Typed memory model, the WP is still sound, but we can not check it automatically (yet). A sound example : ``` //@ ensures *x == 0 ; void f(int *x) { void * p = (void *) x ; int * q = (int *) p ; *q = 0 ; } ``` An unsound example : ``` //@ ensures *x == 0 ; void f(int *x) { void * p = (void*) x ; short * q = (short*) p ; q[0] = 0 ; q[1] = 0 ; } ``` Even when `2*sizeof(short) = sizeof(int)`, the second example is unsound w.r.t Typed memory model, because an `int` pointer is later used as a `short` pointer. But WP discharges the generated proof obligation, considering that `q[0]` and `*x` designate the same atomic memory cell, which is not true. Another unsound example, where WP actually fails to discharge the proof : ``` //@ ensures *x == 0 ; void f(int *x) { void * p = (void*) x ; double * q = (double*) p ; *q = 0.0 ; } ``` Here, the inconsistency is more apparent because integer and floating point memory cells are modeled by different memories in the Typed memory model. Hence, assigning a value through a pointer to double never modify integer values. Hope these examples help. L.