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] WP and type casting

> 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.