Section 6.4 Pointers (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.
Definition 6.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.
Example 6.4.2.
Consider the state:
\begin{equation*}
\sigma=\rho;\mu \quad \text{ with }\quad \rho\defeq\{\CVar x\mapsto\adra,\CVar y\mapsto\adrb\}\quad\mu\defeq\{\adra\mapsto\adrb,\adrb\mapsto 3\}
\end{equation*}
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.
