SA

• Course front page
• Staff
• Students
• Login

Static Analysis, Assignment #6

Consider a program in the while fragment of our tiny imperative language. A points-to analysis produces a map from Vars to Targets. For a program P, we denote the map computed by Andersen's analysis by Andersen(P). The shape analysis can also be used to compute a flow-sensitive points-to map for every program point v which we denote Shape(P,v). Given a points-to map pt, the null pointer analysis computes for every program point v a map nullable(pt,v) telling about possible null pointers. A concrete program P is called boostable, if it is the case that for some program point v and variable x:

nullable(Shape(P,v),v)(x)=NN nullable(Andersen(P),v)(x)=?

so that P is unfairly rejected using Andersen but accepted using shape analysis.

Show that the following program is boostable:

q = malloc;
y = &q;
x = *y;
p = null;
y = &p;
*x = p;