Steensgard konkretisiert

This commit is contained in:
Marco Ammon 2020-08-14 12:56:20 +02:00
parent a45ac896f0
commit a0347487b1
2 changed files with 13 additions and 9 deletions

Binary file not shown.

View File

@ -28,6 +28,8 @@
%\pdfminorversion=7 % Import-Unterstützung für PDFs bis Version 1.7
%\pgfplotsset{compat=1.16} % verhindern, dass pgfplots im Rückwärtskompatibilitätsmodus arbeitet
% TODO: MathOperators verwenden
% TODO: Code in \texttt{} setzen
\setlist[enumerate,1]{label={\arabic*.}}
\setlist[enumerate,2]{label={\alph*)}}
@ -493,6 +495,7 @@
\subsection{Steensgards Algorithmus zur interprozeduralen, fluss-insensitiven may-Analyse}
\begin{itemize}
\item kontext-insensitiv: vermischt Aliaswissen mehrerer Aufrufe der gleichen Funktion
\item Speichergraph: \begin{itemize}
\item Knoten: eine oder mehrere Speicherstellen
\item gerichtete Kante: \enquote{zeigt (möglicherweise) auf}-Beziehung, damit Alias: (*start, ziel)
@ -507,24 +510,25 @@
\item $a = \&b$: Kante zwischen $a$ und $b$ einfügen; sofern bereits Kante zwischen $a$ und $x$ existiert, rekursives Verschmelzen von $x$ und $b$
\item $a = b$:\begin{itemize}
\item $b$ ist Zeiger: Verschmelzen der Ziele von $a$ und $b$, anschließend zeigen beide auf diesen Knoten
\item $b$ ist kein Zeiger bzw. noch nicht erkannt: Annotiere $b$ mit $(a:b)$ (Falls später Zeigerziel $y$ von $b$ entdeckt wird, muss Kante von $a$ nach $y$ ergänzt werden)
\item $b$ ist kein Zeiger bzw. noch nicht erkannt: Annotiere $b$ mit $\lbrace a = b\rbrace$ (Falls später Zeigerziel $y$ von $b$ entdeckt wird, muss Kante von $a$ nach $y$ ergänzt werden)
\end{itemize}
\item $a = *b$: \begin{itemize}
\item $b$, $*b$ haben bereits ausgehende Kanten: Kante zwischen $a$ und $**b$ ergänzen
\item sonst: analog zu $a = b$ mit adäquaten Annotationen (TODO: Übung)
\item sonst: analog zu $a = b$ mit adäquaten Annotationen
\end{itemize}
\item $*a = b$: \begin{itemize}
\item $a$, $*a$ mit ausgehenden Kanten: rekursives Verschmelzen von $*b$ und $**a$
\item sonst: TODO (Übung)
\item $a$ noch ohne ausgehende Kante: Annotation von $a$ mit $\lbrace *a = b\rbrace$
\end{itemize}
\item $a = b \oplus c$ mit $\oplus$ binärer Operation: \begin{itemize}
\item $a$, $b$, $c$ keine Zeiger: Annotation von $b$ und $c$ mit $(a:b)$ bzw. $(a:c)$
\item $b$ oder $c$ Zeiger: Kante von $a$ nach $*b$ hinzufügen, $c$ mit $(a:c)$ annotieren
\end{itemize}
\item $x = p(y_1, \textellipsis, y_n)$: \begin{itemize}
\item ggf. Speichergraph für $p$ berechnen
\item Zuweisungsregeln für $x$ und alle $y_i$ verwenden
\item $a$, $b$, $c$ nicht als Zeiger erkannt: Annotation von $b$ und $c$ mit $\lbrace a= b\rbrace$ bzw. $\lbrace a= c\rbrace$
\item $b$ oder $c$ Zeiger: Kante von $a$ nach $*b$ hinzufügen, $c$ mit $\lbrace a = b\rbrace$ annotieren
\end{itemize}
\item $x = p(y_1, \textellipsis, y_n)$ mit Funktion $p(z_1, \textellipsis, z_n)$ \begin{enumerate}
\item Zuweisungsregeln $z_i = y_i$ verwenden
\item ggf. Speichergraph für Anweisungen von $p$ berechnen
\item Zuweisungsregeln für $x$ verwenden
\end{enumerate}
\item Funktionszeiger: Bei Verschmelzen auf Typen achten
\end{itemize}
\end{enumerate}