## 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:

\begin{align*} \denotR{\CBinary{-}{\CBinary{+}{\CIndir{\CVar x}}{\CVar y}}{\CConst 1}}\sigma\amp = \CBinary{-}{\denotR{\CBinary{+}{\CIndir{\CVar x}}{\CVar y}}\sigma}{\denotR{\CConst 1}}\sigma \\ \amp = \CBinary{-}{\denotR{\CBinary{+}{\CIndir{\CVar x}}{\CVar y}}\sigma}{\CConst 1} \\ \amp = \CBinary{-}{\CBinary{+}{\denotR{\CIndir{\CVar x}}\sigma}{\denotR{\CVar y}\sigma}}{\CConst 1} \end{align*}

Let us consider the R-evaluation of the last two remaining terms in detail:

\begin{equation*} \begin{array}[t]{lcl} \denotR{\CVar y}\sigma \amp = \amp \mu\,\denotL{\CVar y}\sigma \\ \amp = \amp \mu\,(\rho\,\CVar y) \\ \amp = \amp \mu\,\adrb \\ \amp = \amp 3 \end{array} \qquad \begin{array}[t]{lcl} \denotR{\CIndir{\CVar x}}\sigma \amp = \amp \mu\,\denotL{\CIndir{\CVar x}}\sigma \\ \amp = \amp \mu\,\denotR{\CVar x}\sigma \\ \amp = \amp \mu\,(\mu\,\denotL{\CVar x}\sigma) \\ \amp = \amp \mu\,(\mu\,(\rho\,\CVar x)) \\ \amp = \amp \mu\,(\mu\,\adra) \\ \amp = \amp \mu\,\adrb \\ \amp = \amp 3 \end{array} \end{equation*}

The final result of R-evaluating the above expression is hence 5.