aboutsummaryrefslogtreecommitdiffstats
path: root/papers/cfrontend_new/dynsem4.etex
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-04 07:33:32 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-04 07:33:32 +0000
commitadc9e990a0c338cef57ff1bd9717adcc781f283c (patch)
treecdbb1265be6c524ade10565b1a2b500b510f3491 /papers/cfrontend_new/dynsem4.etex
parent355b4abcee015c3fae9ac5653c25259e104a886c (diff)
downloadcompcert-adc9e990a0c338cef57ff1bd9717adcc781f283c.tar.gz
compcert-adc9e990a0c338cef57ff1bd9717adcc781f283c.zip
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
Diffstat (limited to 'papers/cfrontend_new/dynsem4.etex')
-rwxr-xr-xpapers/cfrontend_new/dynsem4.etex42
1 files changed, 0 insertions, 42 deletions
diff --git a/papers/cfrontend_new/dynsem4.etex b/papers/cfrontend_new/dynsem4.etex
deleted file mode 100755
index 3f0b10af..00000000
--- a/papers/cfrontend_new/dynsem4.etex
+++ /dev/null
@@ -1,42 +0,0 @@
-\begin{figure}
-
-\numberrules
-
-Execution of a "switch" statement:
-\begin{pannel}
-
-\irule
- G, E |- a, M \evalexpr n, \tr, M_1 \\
- G, E |- "select_switch" (n,\ls), M_1 \evalstmt \out, \tr_2, M_2
- --------------------------------------------------
- G, E |- "switch" (a)\ls, M \evalstmt "outcome_switch" (\out), \cat {\tr_1} \tr_2, M_2
-\end \label{rule:28}
-\end{pannel}
-
-Execution of a "switch" branch:
-\begin{pannel}
-
-\irule
- G, E |- s, M \evalstmt \out, \tr, M'
- --------------------------------------------------
- G, E |- "default" (s) , M \evalstmt \out, \tr, M'
-\end \label{rule:29}
-
-\\
-\irule
- G, E |- s, M \evalstmt "Out_normal", \tr_1, M_1 \\
- G, E |- \ls, M \evalstmt \out, \tr_2, M_2
- --------------------------------------------------
- G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr_2, M_2
-\end \label{rule:30}
-\\
-\irule
- G, E |- s, M \evalstmt \out, \tr, M' & \out \not= "Out_normal"
- --------------------------------------------------
- G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr, M'
-\end \label{rule:31}
-
-\end{pannel}
-\caption{Dynamic semantics of switch statement}
-\label{fig:dynsem4}
-\end{figure}