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/dynsem1.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/dynsem1.etex')
-rwxr-xr-x | papers/cfrontend_new/dynsem1.etex | 80 |
1 files changed, 0 insertions, 80 deletions
diff --git a/papers/cfrontend_new/dynsem1.etex b/papers/cfrontend_new/dynsem1.etex deleted file mode 100755 index 136c0cda..00000000 --- a/papers/cfrontend_new/dynsem1.etex +++ /dev/null @@ -1,80 +0,0 @@ -\begin{figure} - -\numberrules - -Expressions in l-value position: -\begin{pannel} - -\irule - E(\id) = b - -------------------------------------------------- - G, E |- \id^\tau, M \evallvalue (b, 0), \E0, M -\end \label{rule:1} - -\irule -% G, E |- a, M \evalexpr {\tt Vptr}(\loc), \tr, M' - G, E |- a, M \evalexpr \loc, \tr, M' - -------------------------------------------------- - G, E |- (\hbox{"*"}a)^\tau, M \evallvalue \loc, \tr, M' -\end \label{rule:2} - -\irule - G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 \\ - G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\ - "add" (v_1, \tau_1, v_2, \tau_2) = \some{\loc} - -------------------------------------------------- - G, E |- (\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}])^\tau, M \evallvalue \loc, \cat {\tr_1} \tr_2, M_2 -\end \label{rule:3} - -\irule - G, E |- \unannot{a}{\tau}, M \evallvalue (b,\ofs), \tr, M' \\ - \tau = "Tstruct" (\id, \fl) & -% "type_of" (a) = "Tstruct" (\id, \fl) & - "field_offset" (f, \fl) = \some{\delta} - -------------------------------------------------- - G, E |- (\unannot{a}{\tau} \dot f)^{\tau_s}, M \evallvalue (b,\ofs + "repr" (\delta)), \tr, M' -\end \label{rule:4} - -\irule - G, E |- \unannot{a}{\tau}, M \evallvalue \loc, \tr, M' & - \tau = "Tunion" (\id, \fl) - -------------------------------------------------- - G, E |- (\unannot{a}{\tau} \dot f)^{\tau_u}, M \evallvalue \loc, \tr, M' -\end \label{rule:5} - -\end{pannel} -Expressions in r-value position: -\begin{pannel} - -\irule - G, E |- \unannot{a}\tau, M \evallvalue \loc, \tr, M' & - "loadval" (\tau, M', \loc) = \some{v} - -------------------------------------------------- - G, E |- \unannot{a}\tau, M \evalexpr v, \tr, M' -\end \label{rule:6} - -\irule - G, E |- a, M \evallvalue \loc, \tr, M' - -------------------------------------------------- - G, E |- (\hbox{"&"}a)^\tau, M \evalexpr \loc, \tr, M' -\end \label{rule:7} - -\irule - G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 & - G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\ - "eval_binary_operation" (\op, v_1,\tau_1, v_2,\tau_2) = \some{v} - -------------------------------------------------- - G, E |- (\unannot{a_1}{\tau_1} \op \, \unannot{a_2}{\tau_2})^\tau, M \evalexpr v, \cat \tr_1 \tr_2, M_2 -\end \label{rule:8} - -\irule - G, E |- \unannot{a}{\tau_a}, M \evalexpr v', \tr, M' & - "cast" (v',\tau_a,\tau) = \some{v} - -------------------------------------------------- - G, E |- ((\tau)\unannot{a}{\tau_a}))^\tau, M \evalexpr v, \tr, M' -\end \label{rule:9} -\end{pannel} - -\caption{Selected rules of the dynamic semantics of Clight (expression evaluation)} -\label{fig:dynsem1} -\end{figure} |