## Section6.4Pointers (C0p)

In this section, we extend C0 with pointers. This extension only affects the expression language of C0. The statement language stays the same.

\begin{equation*} \begin{array}{rclll} \mathit{LExpr} \ni l \amp \syndef \amp \cdots \amp \cdots \amp \text{like defined above} \\ \amp | \amp \AIndir{e} \amp \CIndir{e} \amp \text{Indirection} \\ \mathit{Expr} \ni e \amp \syndef \amp \cdots \amp \cdots \amp \text{like defined above} \\ \amp | \amp \AAddrOf{l} \amp \CAddrOf{l} \amp \text{Address-Of} \\ \end{array} \end{equation*}

Let us now extend the L- and R-evaluation functions to this extended syntax.

### Definition6.4.1.Pointer Extension to the C0 Expression Evaluation.

\begin{align*} \denotR{\CAddrOf{l}}\sigma \amp\defeq \denotL{l}\sigma \\ \denotL{\CIndir{e}}\sigma \amp\defeq \denotR{e}\sigma \amp \text{if }\denotR{e}\sigma\in\Addr \end{align*}

Note that $$\denotL{\CIndir{e}}\sigma$$ may not be defined if $$\denotR{e}\sigma$$ does not yield an address.

This definition also nicely displays the “duality” of both operators. $$\&$$ turns an L-value into an R-value and $$*$$ does the opposite.

### Example6.4.2.

Consider the state:

Apparently, $$\CVar x$$ points to the same container as $$\CVar y\text{.}$$ $$\CVar y$$ points to a container that contains the value 3. Let us consider the R-evaluation of the expression $$\CBinary{-}{\CBinary{+}{\CIndir{x}}{y}}{\CConst 1}$$ using Definition 6.4.1: