From 22ff08b38616ceef336f5f974d4edc4d37d955e8 Mon Sep 17 00:00:00 2001
From: blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 3 Aug 2007 17:04:06 +0000
Subject: 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
---
 papers/cfrontend_new/dynsem3.etex | 48 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 papers/cfrontend_new/dynsem3.etex

(limited to 'papers/cfrontend_new/dynsem3.etex')

diff --git a/papers/cfrontend_new/dynsem3.etex b/papers/cfrontend_new/dynsem3.etex
new file mode 100644
index 00000000..bddcef64
--- /dev/null
+++ b/papers/cfrontend_new/dynsem3.etex
@@ -0,0 +1,48 @@
+\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}
-- 
cgit