PE - based on equality, *, ptr struct fields

P = &x

p -> f = &z

tt = p

q = &y

*q = &w

r = &u

*q = r

Pointer related

assignment

statements

{p,tt, &x} {p=&x,tt=p}

(*p,x} { }

{p->f,x.f,&z} {p->f=&z}

{p->g,x.g} { }

{z,*(p->f)} { }

{q,&y} {q = &y}

{*q,y,&w,r,&u} { *q = &w, r= &u, *q = r}

{w,u,*r,**q}

{p, tt, &x}

*

{*p, x}

g

f

{p->f, x.f, &z}

{z, *(p->f)}

*

Equivalence classes

Source

{p->g,x.g}

Previous slide

Next slide

Back to first slide

View graphic version