Version longue et mise a jour du papier sur le front-end (premier jet).

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 40 insertions, 0 deletions

diff --git a/papers/cfrontend_new/values.etex b/papers/cfrontend_new/values.etex
new file mode 100755
index 00000000..bdf2858c
--- /dev/null
+++ b/papers/cfrontend_new/values.etex
@@ -0,0 +1,40 @@
+\begin{figure}
+
+\begin{syntax}
+\syntaxclass{Values:}
+\loc & ::= & (b, n) & location (byte offset $n$ in the memory block\\
+ &  &  & referenced by $b$)\\
+v & ::= & n & integer value\\
+  & \alt & f & floating-point value \\
+  & \alt & \loc & pointer value\\
+% v & ::= & "Vint"(n) & integer value\\
+% & \alt & "Vfloat"(f) & floating-point value \\
+% & \alt & "Vptr"(\loc) & pointer value\\
+  & \alt & "Vundef" & undefined value
+%
+\syntaxclass{Statement outcomes:}
+\out & ::= & "Out_normal" & go to the next statement \\
+    & \alt & "Out_continue" & go to the next iteration of the current loop \\
+    & \alt & "Out_break" & exit from the current loop \\
+    & \alt & "Out_return"  & function exit \\
+    & \alt & "Out_return"(v)  & function exit, returning the value $v$
+%
+\syntaxclass{Global environments:}
+G & ::=  & (id \mapsto b) & map from global variables to block references \\
+  &      & \times (b \mapsto \fn) & and map from function references \\
+  &      & & to function definitions
+%
+\syntaxclass{Local environments:}
+E & ::= &  \id \mapsto b   & map from local variables to block references
+%
+\syntaxclass{Memories:}
+{\it bounds} & ::= & \ldots & low and high bounds \\
+{\it kind} & ::= & \ldots & content map \\
+M & ::= &  b \mapsto {\it bounds} \times & map from block references to block contents\\
+& & (n \mapsto {\it kind} \mapsto v)   & 
+\end{syntax}
+%
+\caption{Values, outcomes, and evaluation environments}
+\label{fig:values}
+\end{figure}
+