diff options
Diffstat (limited to 'papers/cfrontend_new/dynsem2.etex')
-rwxr-xr-x | papers/cfrontend_new/dynsem2.etex | 89 |
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} |