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

1 files changed, 0 insertions, 89 deletions

diff --git a/papers/cfrontend_new/dynsem2.etex b/papers/cfrontend_new/dynsem2.etex
deleted file mode 100755
index e6f81639..00000000
--- a/papers/cfrontend_new/dynsem2.etex
+++ /dev/null
@@ -1,89 +0,0 @@
-\begin{figure}
-
-\numberrules
-
-Statements:
-\begin{pannel}
-
-\srule  G, E |- "skip", M \evalstmt "Out_normal", \E0, M
-\end
-\label{rule:10}
-
-\\[2mm]
-\srule  G, E |- "break", M \evalstmt "Out_break", \E0, M
-\end
-\label{rule:13}
-
-\\[2mm]
-\srule  G, E |- "continue", M \evalstmt "Out_continue", \E0, M
-\end
-\label{rule:14}
-
-\irule
-        G, E |- a, M \evalexpr v, \tr, M'
-        --------------------------------------------------
-        G, E |-  a , M \evalstmt \out, \tr, M'
-\end \label{rule:11}
-
-\irule
-        G, E |- \unannot{a_1}{\tau}, M \evallvalue \loc, \tr_1, M_1 &
-        G, E |- \unannot{a_2}{\tau'}, M_1 \evalexpr v, \tr_2, M_2 \\
-        "storeval"(\tau,M_2,\loc,v) = \some{M_3}
-        --------------------------------------------------
-        G, E |-  {(\unannot{a_1}{\tau} \hbox{" = "} \unannot{a_2}{\tau'})}^{\tau}, M \evalexpr v, \cat {\tr_1} \tr_2, M_3
-\end \label{rule:12}
-
-\\
-\irule
-        G, E |- s_1, M \evalstmt "Out_normal", \tr_1, M_1 &
-        G, E |- s_2, M_1 \evalstmt \out, \tr_2, M_2
-        --------------------------------------------------
-        G, E |- (s_1 ; s_2), M \evalstmt \out, \cat {\tr_1} \tr_2, M_2
-\end \label{rule:15}
-
-\irule
-        G, E |- s_1, M \evalstmt out, \tr, M' &
-        out \not= "Out_normal"
-        --------------------------------------------------
-        G, E |- (s_1; s_2), M \evalstmt \out, \tr, M'
-\end \label{rule:16}
-
-\\
-\irule
-        G, E |- a, M \evalexpr v, \tr, M' & "is_false"(v) 
-        --------------------------------------------------
-        G, E |- ("while" (a) ~ s), M \evalstmt  "Out_normal", \tr, M'
-\end \label{rule:17}
-
-\irule
-        G, E |- a, M \evalexpr v, \tr_1, M_1 & "is_true" (v) \\
-        G, E |- s, M_1 \evalstmt \out, \tr_2, M_2 \\
-       \out \in \{"Out_break", "Out_return", "Out_return" (v)\}
-        --------------------------------------------------
-        G, E |- ("while" (a)~s), M \evalstmt "Out_normal", \cat {\tr_1} \tr_2, M_2
-\end \label{rule:18}
-
-\irule
-        G, E |- a, M \evalexpr v_a, \tr_1, M_1 & "is_true" (v_a) \\
-        G, E |- s, M_1 \evalstmt ("Out_normal" \mid "Out_continue"), \tr_2, M_2 \\
-        G, E |- ("while" (a)~s), M_2 \evalstmt \out', \tr_3, M_3 
-        --------------------------------------------------
-        G, E |- ("while" (a)~s), M \evalstmt \out', \cat {\cat {\tr_1} \tr_2} \tr_3, M_3
-\end \label{rule:19}
-
-\\
-\srule
-        G, E |- ("return" \, \None), M \evalstmt "Out_return" , \tr, M
-\end \label{rule:20}
-
-\\
-\irule
-        G, E |- a, M \evalexpr v, \tr, M'
-        --------------------------------------------------
-        G, E |- ("return" \some a), M \evalstmt "Out_return" (v), \tr, M'
-\end \label{rule:21}
-
-\end{pannel}
-\caption{Selected rules of the dynamic semantics of Clight (statements execution)}
-\label{fig:dynsem2}
-\end{figure}