diff options
author | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-03 17:04:06 +0000 |
---|---|---|
committer | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-03 17:04:06 +0000 |
commit | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (patch) | |
tree | 3ee53330a4b7306ba565fd1cc149a22299ecb48c /papers/cfrontend_new/dynsem4.etex | |
parent | 21a429c66efad3394024ba12203fa9a3d3d36fa8 (diff) | |
download | compcert-22ff08b38616ceef336f5f974d4edc4d37d955e8.tar.gz compcert-22ff08b38616ceef336f5f974d4edc4d37d955e8.zip |
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
Diffstat (limited to 'papers/cfrontend_new/dynsem4.etex')
-rwxr-xr-x | papers/cfrontend_new/dynsem4.etex | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/papers/cfrontend_new/dynsem4.etex b/papers/cfrontend_new/dynsem4.etex new file mode 100755 index 00000000..3f0b10af --- /dev/null +++ b/papers/cfrontend_new/dynsem4.etex @@ -0,0 +1,42 @@ +\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} |