From 22ff08b38616ceef336f5f974d4edc4d37d955e8 Mon Sep 17 00:00:00 2001
From: blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 3 Aug 2007 17:04:06 +0000
Subject: 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
---
 papers/cfrontend_new/trace.etex | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 papers/cfrontend_new/trace.etex

(limited to 'papers/cfrontend_new/trace.etex')

diff --git a/papers/cfrontend_new/trace.etex b/papers/cfrontend_new/trace.etex
new file mode 100644
index 00000000..d02b1fe9
--- /dev/null
+++ b/papers/cfrontend_new/trace.etex
@@ -0,0 +1,19 @@
+\begin{figure}
+
+\begin{syntax}
+\syntaxclass{Event values:}
+\evv & ::= & n & integer value\\
+  & \alt & f & floating-point value 
+%
+\syntaxclass{Events:}
+\ev & ::= & \id \, \evv^* \, \evv & 
+%
+\syntaxclass{Execution traces:}
+\tr & ::=  & \E0 & empty trace \\
+     & \alt & [\ev] & external call \\
+     & \alt & \cat \tr \tr& concatenation
+\end{syntax}
+\caption{Execution traces}
+\label{fig:trace}
+\end{figure}
+
-- 
cgit