struct _str {
    int a;
    int b;
    int c;
    int d;
    int e;
    int f;
    int g;
    int h;
    int i;
    int j;
    int k;
    int l;
    int m;
    int n;
    int o;
    int p;
};

struct _str *s;
struct _str *t;

int a;
int b;
int c;
int d;
int e;
int f;
int g;
int h;
int i;
int j;
int k;
int l;
int m;
int n;
int o;
int p;


/*@ 
    requires \valid(s);
    requires \valid(t);
    ensures    a == 0;
    ensures s->a == 0;
    ensures t->a == 0;
*/
void ftest(void) {
       a = 0;
    s->a = 0;
    t->a = 0;
       b = 0;
    s->b = 0;
    t->b = 0;
       c = 0;
    s->c = 0;
    t->c = 0;
       d = 0;
    s->d = 0;
    t->d = 0;
       e = 0;
    s->e = 0;
    t->e = 0;
       f = 0;
    s->f = 0;
    t->f = 0;
       g = 0;
    s->g = 0;
    t->g = 0;
       h = 0;
    s->h = 0;
    t->h = 0;
       i = 0;
    s->i = 0;
    t->i = 0;
       j = 0;
    s->j = 0;
    t->j = 0;
       k = 0;
    s->k = 0;
    t->k = 0;
       l = 0;
    s->l = 0;
    t->l = 0;
       m = 0;
    s->m = 0;
    t->m = 0;
       n = 0;
    s->n = 0;
    t->n = 0;
       o = 0;
    s->o = 0;
    t->o = 0;
       p = 0;
    s->p = 0;
    t->p = 0;
}