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/dynsem3.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/dynsem3.etex')
-rw-r--r-- | papers/cfrontend_new/dynsem3.etex | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/papers/cfrontend_new/dynsem3.etex b/papers/cfrontend_new/dynsem3.etex deleted file mode 100644 index bddcef64..00000000 --- a/papers/cfrontend_new/dynsem3.etex +++ /dev/null @@ -1,48 +0,0 @@ -\begin{figure} -Compatibility between values, outcomes and return types: - -$$\begin{array}{rclr} -"Out_normal", "Tvoid" & \# & "Vundef"& \\ -"Out_normal", "Tvoid" & \# & "Vundef"& \\ -"Out_return", \, "Tvoid" & \# & "Vundef" & \\ -"Out_return" \some v, \, \tau & \# & v & \mbox{when}\,\tau~\not="Tvoid" -\end{array}$$ - -\numberrules - -Function calls: -\begin{pannel} - -\irule - G, E |- {a_{fun}}^{\tau}, M \evalexpr v_{fun}, \tr_1, M_1 & - G, E |- a_{args}, M_1 \evalexpr v_{args}, \tr_2, M_2 \\ - G[v_{fun}] = \some{f} & - "type_of_fundef" (f) = \tau \\ - G |- f(v_{args}), M_2 \evalfunc v_{res}, \tr_3, M_3 - -------------------------------------------------- - G, E |- {({a_{fun}}^{\tau} (a_{args}))}^{\tau'}, M \evalexpr v_{res}, \cat {\cat {\tr_1} \tr_2} \tr_3, M_3 -\end \label{rule:25} -\end{pannel} - -Function invocations: -\begin{pannel} - -\irule - "alloc" ({\it \emptyset_E}, M, "params" (f) + "vars" (f),E) = (M_1, b) \\ - "bind_params" (E, M_1, "params" (f), v_{args}) = M_2 \\ - G, E |- "body" (f), M_2 \evalstmt \out, \tr, M_3 \\ - \out, \, "fn_return" (f) \, "#" \, v_{res} - -------------------------------------------------- - G, E |- f(v_{args}), M \evalstmt v_{res}, \tr, "free" (M_3, b) -\end \label{rule:26} - -\irule - v_{args}, v_{res} \cong^{\sigma} e_{args}, e_{res} - -------------------------------------------------- - G, E |- <\id \, \sigma>(v_{args}), M \evalstmt v_{res}, [\id \,e_{args}\, e_{res}], M -\end \label{rule:27} - -\end{pannel} -\caption{Dynamic semantics of function call} -\label{fig:dynsem3} -\end{figure} |