Hi Mike,
----- Original Message -----
> static inline float get_coef(enum ftype t) {
> return *(float *)((char *)&filter_s + filter_s.offset_callback(t));
> }
>
> static inline enum ftype set_coef(enum ftype t, float val) {
> *(float *)((char *)&filter_s + filter_s.offset_callback(t)) = val;
> return t;
> }
>
> void foo();
> void boo() {
> enum ftype tx;
> float fx;
> fx = 1.0;
> tx = T1;
> init();
> if (filter_s.offset_callback != offset)
> if (get_coef(set_coef(tx, fx)) != fx)
> foo();
> }
I guess you meant:
if (filter_s.offset_callback == offset) {
if (get_coef(set_coef(tx, fx)) != fx) foo
}
In your example the call to foo() can be trivially proven to be
unreachable. For the modified example, the model checker has to prove
(assuming get_coef and set_coef have no other side-effects):
*(float *)((char *)&filter_s + offset(tx, fx)) = VAL;
*(float *)((char *)&filter_s + offset(tx, fx)) != VAL;
which is trivially false and can be proven by using uninterpreted
functions (as offset is declared to be pure and const). If there were
several possible offset callbacks and each of them had some
side-effects, the proof would get harder....
Happy New Year!
Domagoj
--
___________________________________________________
Play 100s of games for FREE! http://games.mail.com/
