summaryrefslogtreecommitdiff
path: root/papers/cfrontend_new/values.etex
diff options
context:
space:
mode:
Diffstat (limited to 'papers/cfrontend_new/values.etex')
-rwxr-xr-xpapers/cfrontend_new/values.etex40
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 0000000..bdf2858
--- /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}
+