From 0654f7e6082e5de7dba9f39f608ed6a166043d92 Mon Sep 17 00:00:00 2001
From: "Dr. Christoph L. Spiel" <cspiel@freenet.de>
Date: Sat, 5 Jul 2014 09:58:45 +0200
Subject: [PATCH 1/2] Fix incomplete documentation with respect to Ptranal.

To use the Points-to-analysis module (Ptranal) it is not only
necessary to call Ptranal.analyze_file as stated in the documentation,
but to run Ptranal.compute_results afterwards and in particular before
any call to the "database query" functions of the module.

This fixes the initial problem as reported in issue #141 ("Bug in
pointer analysis or documentation")
    http://sourceforge.net/p/cil/bugs/141/
---
 doc/cil.tex | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/doc/cil.tex b/doc/cil.tex
index 331494ee0..c3c7a816e 100644
--- a/doc/cil.tex
+++ b/doc/cil.tex
@@ -1953,12 +1953,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,
@@ -2040,10 +2046,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}

From 083397744bd33bbec6336cb778478fe6f735b522 Mon Sep 17 00:00:00 2001
From: "Dr. Christoph L. Spiel" <cspiel@freenet.de>
Date: Sat, 5 Jul 2014 10:19:29 +0200
Subject: [PATCH 2/2] Document the new option `--ptr_use_olf' of cilly.

This partly fixes issue #146 ("Olf vs. Golf in Ptranal")
        http://sourceforge.net/p/cil/bugs/146/
---
 doc/cil.tex | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/doc/cil.tex b/doc/cil.tex
index c3c7a816e..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)
@@ -1992,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}.