Add open Expr in I

report/report.tex

@@ -398,9 +398,9 @@ parse the relevant FDE from its start, until it finds the row it was seeking.
 We will now define semantics covering most of the operations used for FDEs
 described in the DWARF standard~\cite{dwarf5std}, such as seen in
 Listing~\ref{lst:ex1_dwraw}, with the exception of DWARF expressions. These are
-not exhaustively treated because they form a rich language and would take a lot
-of time and space to formalize, and in the meantime are only seldom used (see
-the DWARF statistics regarding this).
+not treated here, because they form a rich language and would take a lot
+of time and space to formalize, while in the meantime being seldom used --~see
+Section~\ref{ssec:instr_cov}.
 
 These semantics are defined with respect to the well-formalized C language, and
 are passing through an intermediary language. The DWARF language can read the
@@ -489,6 +489,7 @@ Its grammar is as follows:
     \values &::= \bot & \text{Values: undefined,}\\
         &\quad\vert~\valaddr{\spexpr} & \text{at address $x$},\\
         &\quad\vert~\valval{\spexpr} & \text{of value $x$} \\
+        &\quad\vert~\valexpr{??} & \text{of expression $x$, see in text} \\
     \spexpr &::= \regs \times \mathbb{Z}
         & \text{A ``simple'' expression $\reg{reg} + \textit{offset}$} \\
 \end{align*}
@@ -510,7 +511,9 @@ value $x$, $x$ being here a simple expression consisting of $\reg{reg} +
 \textit{offset}$. The CFA is considered a simple register here. For instance,
 to define $\reg{rax}$ to the value contained in memory 16 bytes below the CFA,
 we would have $\reg{rax} \mapsto \valaddr{\reg{CFA}, -16}$, since the stack
-grows downwards.
+grows downwards. We also leave open the possibility to extend the language with
+DWARF expressions support as $\valexpr{}$, although we \emph{do not} specify
+them here.
 
 \subsection{Target language: a C function body}
 
@@ -632,9 +635,10 @@ we omit those two operations, we can plainly remove the stack.
 
 \subsection{From $\intermedlang$ to C}
 
-\textit{This only defines the semantics, with respect to standard C, of DWARF
-as interpreted by \ehelf\@. The actual DWARF to C compiler is not implemented
-this way.}
+\emph{The C code provided thereafter is a correct but inefficient reference
+implementation, which is only provided for formalization, to specify DWARF
+\wrt{} C. In particular, the actual compiler is \emph{not} implemented this
+way.}
 
 \medskip
 

shared/specific.sty

@@ -24,6 +24,7 @@
 
 \newcommand{\valaddr}[1]{\operatorname{Addr}\left(#1\right)}
 \newcommand{\valval}[1]{\operatorname{Val}\left(#1\right)}
+\newcommand{\valexpr}[1]{\operatorname{Expr}\left(#1\right)}
 
 \newcommand{\intermedlang}{\mathcal{I}}