diff --git a/doc/cil.tex b/doc/cil.tex index 331494ee0..ea597ea17 100644 --- a/doc/cil.tex +++ b/doc/cil.tex @@ -1935,15 +1935,14 @@ \subsection{Dominators} \subsection{Points-to Analysis} The module \t{ptranal.ml} contains two interprocedural points-to -analyses for CIL: \t{Olf} and \t{Golf}. \t{Olf} is the default. -(Switching from \t{olf.ml} to \t{golf.ml} requires a change in -\t{Ptranal} and a recompiling \t{cilly}.) +analyses for CIL: \t{Olf} and \t{Golf}. \t{Golf} is the default. +Switch to \t{Olf} with {\bf -{}-ptr\_use\_olf}. The analyses have the following characteristics: \begin{itemize} \item Not based on C types (inferred pointer relationships are sound despite most kinds of C casts) -\item One level of subtyping +\item One level of subtyping \item One level of context sensitivity (Golf only) \item Monomorphic type structures \item Field insensitive (fields of structs are conflated) @@ -1953,12 +1952,18 @@ \subsection{Points-to Analysis} The analysis itself is factored into two components: \t{Ptranal}, which walks over the CIL file and generates constraints, and \t{Olf} -or \t{Golf}, which solve the constraints. The analysis is invoked -with the function \t{Ptranal.analyze\_file: Cil.file -> - unit}. This function builds the points-to graph for the CIL file -and stores it internally. There is currently no facility for clearing -internal state, so \t{Ptranal.analyze\_file} should only be called -once. +or \t{Golf}, which solve the constraints. + +The analysis is invoked with the function \t{Ptranal.analyze\_file: + Cil.file -> unit}. This function builds the points-to graph for the +CIL file and stores it internally. (There is currently no facility +for clearing internal state, so \t{Ptranal.analyze\_file} should only +be called once.) After building the points-to graph the result +database must be built with a call to \t{Ptranal.compute\_results: bool ref -> unit}. +This will essentially serialize the points-to graph. If invoked with \t{true}, the +function will print out the points-to set of each variable in the +file, which is useful for debugging. + %%% Interface for querying the points-to graph... The constructed points-to graph supports several kinds of queries, @@ -1986,6 +1991,10 @@ \subsection{Points-to Analysis} of several flags: \begin{itemize} +\item \t{Ptranal.olf\_backend: bool ref}. + If \t{true}, module \t{Olf} performs the analysis. The default is + \t{false} and module \t{Golf} is used. Associated commandline option: + {\bf -{}-ptr\_use\_olf}. \item \t{Ptranal.no\_sub: bool ref}. If \t{true}, subtyping is disabled. Associated commandline option: {\bf -{}-ptr\_unify}. @@ -2040,10 +2049,6 @@ \subsection{Points-to Analysis} \t{true}, this output is sufficient to reconstruct the points-to graph. One nice feature is that there is a pretty printer for recursive types, so the print routine does not loop. -\item \t{Ptranal.compute\_results: bool ref}. - If \t{true}, the analysis will print out the points-to set of each - variable in the program. This will essentially serialize the - points-to graph. \end{itemize} \subsection{StackGuard}