Skip to main content
Logo image

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.