> | Another interesting issue would be:
> |
> | struct S {
> | int i;
> | float j;
> | } s;
> |
> | *(float *)((char*)&s + 4);
>
> I was actually referring to this case (or something to that effect) --
> I believe Mark Mitchell was of the opinion that it is undefined
> (though, apologies if I misrepresent exactly the opposite of what he
> said) and another camp thought it should be defined (or the opposite.)
> I don't recall we ever reached an agreement.
> -- Gaby
In the case anybody cares about code verifiability... It's exteremely hard
to automatically prove the correctness of the code that uses pointer
arithmetic and casts as in the example above.
Consider the following example:
enum ftype {T1, T2, T3};
static int calls=0;
union x {
double dparam;
float fparam;
long lparam;
int iparam;
};
struct coefs {
union x ux;
float c1;
float c2;
float c3;
int (*offset_callback)(enum ftype t);
} filter_s;
void init(void) {
filter_s.offset_callback = offset;
int offset(enum ftype t) {
int off = sizeof(union x);
calls++;
switch (t) {
case T1: return off;
case T2: return off + sizeof(float);
case T3: return off + 2*sizeof(float);
}
}
float get_coef(enum ftype t) {
return *(float *)((char *)&filter_s + filter_s.offset_callback(t));
}
enum ftype set_coef(enum ftype t, float val) {
*(float *)((char *)&filter_s + filter_s.offset_callback(t)) = val;
return t;
}
How is the compiler going to figure out that c1,c2 and c3 are actually
used?
Proving more interesting properties like
enum ftype tx;
float fx;
... (assign to tx and fx)
assert(get_coef(set_coef(tx, fx)) == fx);
would be even harder.
Domagoj
--
___________________________________________________
Play 100s of games for FREE! http://games.mail.com/
