From adc9e990a0c338cef57ff1bd9717adcc781f283c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Aug 2007 07:33:32 +0000
Subject: Deplacement du repertoire "papers" dans la hierarchie SVN

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 papers/cfrontend_new/dynsem1.etex | 80 ---------------------------------------
 1 file changed, 80 deletions(-)
 delete mode 100755 papers/cfrontend_new/dynsem1.etex

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

diff --git a/papers/cfrontend_new/dynsem1.etex b/papers/cfrontend_new/dynsem1.etex
deleted file mode 100755
index 136c0cda..00000000
--- a/papers/cfrontend_new/dynsem1.etex
+++ /dev/null
@@ -1,80 +0,0 @@
-\begin{figure}
-
-\numberrules
-
-Expressions in l-value position:
-\begin{pannel}
-
-\irule
-        E(\id) = b
-        --------------------------------------------------
-        G, E |- \id^\tau, M \evallvalue (b, 0), \E0, M
-\end \label{rule:1}
-
-\irule
-%        G, E |- a, M \evalexpr {\tt Vptr}(\loc), \tr, M'
-        G, E |- a, M \evalexpr \loc, \tr, M'
-        --------------------------------------------------
-        G, E |- (\hbox{"*"}a)^\tau, M \evallvalue \loc, \tr, M'
-\end \label{rule:2}
-
-\irule
-        G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 \\
-        G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\
-        "add" (v_1, \tau_1, v_2, \tau_2) = \some{\loc}
-        --------------------------------------------------
-        G, E |- (\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}])^\tau, M \evallvalue \loc, \cat {\tr_1} \tr_2, M_2
-\end \label{rule:3}
-
-\irule
-        G, E |- \unannot{a}{\tau}, M \evallvalue (b,\ofs), \tr, M' \\
-        \tau = "Tstruct" (\id, \fl) &
-%        "type_of" (a) = "Tstruct" (\id, \fl) &
-       "field_offset" (f, \fl) =  \some{\delta}
-        --------------------------------------------------
-        G, E |- (\unannot{a}{\tau} \dot f)^{\tau_s}, M \evallvalue (b,\ofs + "repr" (\delta)), \tr, M'
-\end \label{rule:4}
-
-\irule
-        G, E |- \unannot{a}{\tau}, M \evallvalue \loc, \tr, M' &
-         \tau = "Tunion" (\id, \fl) 
-        --------------------------------------------------
-        G, E |- (\unannot{a}{\tau} \dot f)^{\tau_u}, M \evallvalue \loc, \tr, M'
-\end \label{rule:5}
-
-\end{pannel}
-Expressions in r-value position:
-\begin{pannel}
-
-\irule
-        G, E |- \unannot{a}\tau, M \evallvalue \loc, \tr, M' &
-        "loadval" (\tau, M', \loc) = \some{v}
-        --------------------------------------------------
-        G, E |- \unannot{a}\tau, M \evalexpr v, \tr, M'
-\end \label{rule:6}
-
-\irule
-        G, E |- a, M \evallvalue \loc, \tr, M'
-        --------------------------------------------------
-        G, E |- (\hbox{"&"}a)^\tau, M \evalexpr \loc, \tr, M'
-\end \label{rule:7}
-
-\irule
-        G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 &
-        G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\
-        "eval_binary_operation" (\op, v_1,\tau_1, v_2,\tau_2) =  \some{v}
-        --------------------------------------------------
-        G, E |- (\unannot{a_1}{\tau_1} \op \, \unannot{a_2}{\tau_2})^\tau, M \evalexpr v, \cat \tr_1 \tr_2, M_2
-\end \label{rule:8}
-
-\irule
-        G, E |- \unannot{a}{\tau_a}, M \evalexpr v', \tr, M' &
-        "cast" (v',\tau_a,\tau) = \some{v}
-        --------------------------------------------------
-        G, E |- ((\tau)\unannot{a}{\tau_a}))^\tau, M \evalexpr v, \tr, M'
-\end \label{rule:9}
-\end{pannel}
-
-\caption{Selected rules of the dynamic semantics of Clight (expression evaluation)}
-\label{fig:dynsem1}
-\end{figure}
-- 
cgit