Commit 72c68b20 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

More images.

parent 66bc3b5c
......@@ -460,6 +460,22 @@
\end{frame}
\begin{frame}{Selected Reasoning Rules}
\begin{center}
\includegraphics[width=.9\textwidth]{store}
\end{center}
\end{frame}
\begin{frame}{Selected Reasoning Rules}
\begin{center}
\includegraphics[width=.5\textwidth]{alloca}
\end{center}
\end{frame}
\begin{frame}{Axioms}
Points-to and pointed-by assertions can be \emph{split} and \emph{joined}.
......@@ -487,13 +503,12 @@
\begin{frame}{Logical Deallocation}
Logical deallocation of a block is a \emph{ghost operation:}
\bgroup\renewcommand\star{\;\ordinarystar\;}
\[
\inferrule[FreeSingleton]{}{
\loc\fpointsto{1}{\btuple\vals} \star \loc\vfpointedby{1}\lsv
\star \pure{\dom{\lsv}\subseteq\{\loc\}}
\qquad \supd \qquad
\quad \supd \quad
\ddag{\{\loc\}} \star \SC{\sz{\btuple\vals}}
}
\]
% TODO re-draw this rule by hand
......@@ -516,9 +531,6 @@
\end{frame}
% TODO reasoning rule for Load or Store
% TODO reasoning rule for Alloca
\begin{frame}{Soundness of \DIAMS}
\begin{theorem}[Soundness]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment