diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:33:32 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:33:32 +0000 |
commit | adc9e990a0c338cef57ff1bd9717adcc781f283c (patch) | |
tree | cdbb1265be6c524ade10565b1a2b500b510f3491 /papers/cfrontend_new/dynsem4.etex | |
parent | 355b4abcee015c3fae9ac5653c25259e104a886c (diff) | |
download | compcert-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-x | papers/cfrontend_new/dynsem4.etex | 42 |
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} |