我们现在也能够定义一种检测空指针解引用的分析。具体而言，我们希望确保只有在 X 不为 null 时才执行 *X。让我们考虑过程内分析，这样我们可以忽略函数调用。

同之前一致，我们假设程序已经被标准化，也就是所有指针操作都是11.2节中六种操作之一。那么描述指针状态的格，我们叫作Null，定义如下：

Untitled

其中底元素NN表示一定不为null，顶部元素表示可能为null。我们对于一个程序点的抽象状态用一个映射格来表示，定义如下：在某个cfg点的时候，所有内存Cell的指针状态

Untitled

对于每一个CFG中的节点v，我们同样的引入约束变量[[v]]表示抽象状态映射格里面的一个元素，也就是v点的结果。对于程序中每个节点之后的状态，我们可以用对应的约束变量来表示抽象状态。

定义约束规则：

  1. 没有指针操作的节点：对于那么没有所有的节点，我们的约束规则如下：表示就是前序节点的合并

Untitled

Untitled

  1. 取值load操作：X1 = *X2，我们需要对程序变量 X1 的变化建模。我们的抽象中只有一个针对 X1 的单一抽象单元。在假设进行过程内分析的情况下，这个抽象单元表示一个具体单元。（在进行过程间分析时，我们需要考虑运行时每个栈帧都有该变量的一个实例。）对于表达式 *X2，我们可以向指向分析询问 pt(X2) 的可能单元。有了这些结果，我们的约束规则如下：也就是说需要将X1的结果替换为所有X2可能指向的单元的状态的join。也就是说，此时X1等价于X2这个指针指向的单元，所以要用pt(x2)的结果R来更新X1。（这里用join的原因是，假设X2指向两个不同的单元，那么有一个是可能为null，那么X此时就有问题）

    Untitled

  2. 存值store操作：*X1=X2，我们需要对X1指向的任何内容的变化进行建模。这可能是多个抽象单元，即pt(X1)。此外，每个抽象堆单元alloc-i可能描述多个具体单元。因此，在存储操作的约束中，我们必须将新的抽象值合并到pt(X1)中每个受影响的单元的现有值中。也就是说，X1所有指向的单元的状态需要进行更新

    Untitled

  3. 其他操作类似：

Untitled

    在存储操作中，我们对赋值进行建模，通过将新的抽象值合并到现有值中的情况被称为弱更新。相反，在强更新中，新的抽象值会覆盖现有值，在修改程序变量的所有操作中都可以看到，例如在空指针分析中。强更新通常在一般情况下比弱更新更精确，但为了安全地检测可以应用强更新的情况，可能需要更精致的分析抽象。

    在对于给定程序完成空指针分析之后，一个指针的解引用*X在一个程序点v，如果满足JOIN(v)(X)=NN，那么程序就是安全的。这个分析的精度严重依赖于指针分析的结果。

例子：

p = alloc null; // p = NN, alloc 1 = T; 
q = &p; // p = NN, alloc 1 = T, q = NN; 
n = null; // p = NN, alloc 1 = T, q = NN, n = T;
*q = n; // p = T, alloc 1 = T, q = NN, n = T;
*p = n; // p = T, alloc 1 = T, q = NN, n = T;