Cleaned up configure script.

Distribution of CIL as an expanded source tree with changes applied
(instead of original .tar.gz + patches to be applied at config time).


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

12 files changed, 5850 insertions, 0 deletions

diff --git a/cil/src/ext/pta/golf.ml b/cil/src/ext/pta/golf.ml
new file mode 100644
index 00000000..5ea47ff1
--- /dev/null
+++ b/cil/src/ext/pta/golf.ml
@@ -0,0 +1,1657 @@
+(*
+ *
+ * Copyright (c) 2001-2002,
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(* Exceptions                                                          *)
+(*                                                                     *)
+(***********************************************************************)
+
+exception Inconsistent (* raised if constraint system is inconsistent *)
+exception WellFormed   (* raised if types are not well-formed *)
+exception NoContents
+exception APFound      (* raised if an alias pair is found, a control
+                          flow exception *)
+
+
+module U = Uref
+module S = Setp
+module H = Hashtbl
+module Q = Queue
+
+
+(** Subtyping kinds *)
+type polarity =
+    Pos
+  | Neg
+  | Sub
+
+(** Path kinds, for CFL reachability *)
+type pkind =
+    Positive
+  | Negative
+  | Match
+  | Seed
+
+(** Context kinds -- open or closed *)
+type context =
+    Open
+  | Closed
+
+(* A configuration is a context (open or closed) coupled with a pair
+   of stamps representing a state in the cartesian product DFA. *)
+type configuration = context * int * int
+
+module ConfigHash =
+struct
+  type t = configuration
+  let equal t t' = t = t'
+  let hash t = Hashtbl.hash t
+end
+
+module CH = H.Make (ConfigHash)
+
+type config_map = unit CH.t
+
+(** Generic bounds *)
+type 'a bound = {index : int; info : 'a U.uref}
+
+(** For label paths. *)
+type 'a path = {
+  kind : pkind;
+  reached_global : bool;
+  head : 'a U.uref;
+  tail : 'a U.uref
+}
+
+module Bound =
+struct
+  type 'a t = 'a bound
+  let compare (x : 'a t) (y : 'a t) =
+    if U.equal (x.info, y.info) then x.index - y.index
+    else Pervasives.compare (U.deref x.info) (U.deref y.info)
+end
+
+module Path =
+struct
+  type 'a t = 'a path
+  let compare (x : 'a t) (y : 'a t) =
+    if U.equal (x.head, y.head) then
+      begin
+        if U.equal (x.tail, y.tail) then
+          begin
+            if x.reached_global = y.reached_global then
+              Pervasives.compare x.kind y.kind
+            else Pervasives.compare x.reached_global y.reached_global
+          end
+        else Pervasives.compare (U.deref x.tail) (U.deref y.tail)
+      end
+    else Pervasives.compare (U.deref x.head) (U.deref y.head)
+end
+
+module B = S.Make (Bound)
+
+module P = S.Make (Path)
+
+type 'a boundset = 'a B.t
+
+type 'a pathset = 'a P.t
+
+(** Constants, which identify elements in points-to sets *)
+(** jk : I'd prefer to make this an 'a constant and specialize it to varinfo
+    for use with the Cil frontend, but for now, this will do *)
+type constant = int * string * Cil.varinfo
+
+module Constant =
+struct
+  type t = constant
+  let compare (xid, _, _) (yid, _, _) = xid - yid
+end
+module C = Set.Make (Constant)
+
+(** Sets of constants. Set union is used when two labels containing
+  constant sets are unified *)
+type constantset = C.t
+
+type lblinfo = {
+  mutable l_name: string;
+  (** either empty or a singleton, the initial location for this label *)
+  loc : constantset;
+  (** Name of this label *)
+  l_stamp : int;
+  (** Unique integer for this label *)
+  mutable l_global : bool;
+  (** True if this location is globally accessible *)
+  mutable aliases: constantset;
+  (** Set of constants (tags) for checking aliases *)
+  mutable p_lbounds: lblinfo boundset;
+  (** Set of umatched (p) lower bounds *)
+  mutable n_lbounds: lblinfo boundset;
+  (** Set of unmatched (n) lower bounds *)
+  mutable p_ubounds: lblinfo boundset;
+  (** Set of umatched (p) upper bounds *)
+  mutable n_ubounds: lblinfo boundset;
+  (** Set of unmatched (n) upper bounds *)
+  mutable m_lbounds: lblinfo boundset;
+  (** Set of matched (m) lower bounds *)
+  mutable m_ubounds: lblinfo boundset;
+  (** Set of matched (m) upper bounds *)
+
+  mutable m_upath: lblinfo pathset;
+  mutable m_lpath: lblinfo pathset;
+  mutable n_upath: lblinfo pathset;
+  mutable n_lpath: lblinfo pathset;
+  mutable p_upath: lblinfo pathset;
+  mutable p_lpath: lblinfo pathset;
+
+  mutable l_seeded : bool;
+  mutable l_ret : bool;
+  mutable l_param : bool;
+}
+
+(** Constructor labels *)
+and label = lblinfo U.uref
+
+(** The type of lvalues. *)
+type lvalue = {
+  l: label;
+  contents: tau
+}
+
+and vinfo = {
+  v_stamp : int;
+  v_name : string;
+
+  mutable v_hole : (int,unit) H.t;
+  mutable v_global : bool;
+  mutable v_mlbs : tinfo boundset;
+  mutable v_mubs : tinfo boundset;
+  mutable v_plbs : tinfo boundset;
+  mutable v_pubs : tinfo boundset;
+  mutable v_nlbs : tinfo boundset;
+  mutable v_nubs : tinfo boundset
+}
+
+and rinfo = {
+  r_stamp : int;
+  rl : label;
+  points_to : tau;
+  mutable r_global: bool;
+}
+
+and finfo = {
+  f_stamp : int;
+  fl : label;
+  ret : tau;
+  mutable args : tau list;
+  mutable f_global : bool;
+}
+
+and pinfo = {
+  p_stamp : int;
+  ptr : tau;
+  lam : tau;
+  mutable p_global : bool;
+}
+
+and tinfo = Var of vinfo
+            | Ref of rinfo
+            | Fun of finfo
+            | Pair of pinfo
+
+and tau = tinfo U.uref
+
+type tconstraint = Unification of tau * tau
+                   | Leq of tau * (int * polarity) * tau
+
+
+(** Association lists, used for printing recursive types. The first element
+  is a type that has been visited. The second element is the string
+  representation of that type (so far). If the string option is set, then
+  this type occurs within itself, and is associated with the recursive var
+  name stored in the option. When walking a type, add it to an association
+  list.
+
+  Example : suppose we have the constraint 'a = ref('a). The type is unified
+  via cyclic unification, and would loop infinitely if we attempted to print
+  it. What we want to do is print the type u rv. ref(rv). This is accomplished
+  in the following manner:
+
+  -- ref('a) is visited. It is not in the association list, so it is added
+  and the string "ref(" is stored in the second element. We recurse to print
+  the first argument of the constructor.
+
+  -- In the recursive call, we see that 'a (or ref('a)) is already in the
+  association list, so the type is recursive. We check the string option,
+  which is None, meaning that this is the first recurrence of the type. We
+  create a new recursive variable, rv and set the string option to 'rv. Next,
+  we prepend u rv. to the string representation we have seen before, "ref(",
+  and return "rv" as the string representation of this type.
+
+  -- The string so far is "u rv.ref(". The recursive call returns, and we
+  complete the type by printing the result of the call, "rv", and ")"
+
+  In a type where the recursive variable appears twice, e.g. 'a = pair('a,'a),
+  the second time we hit 'a, the string option will be set, so we know to
+  reuse the same recursive variable name.
+*)
+type association = tau * string ref * string option ref
+
+module PathHash =
+struct
+  type t = int list
+  let equal t t' = t = t'
+  let hash t = Hashtbl.hash t
+end
+
+module PH = H.Make (PathHash)
+
+(***********************************************************************)
+(*                                                                     *)
+(* Global Variables                                                    *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Print the instantiations constraints. *)
+let print_constraints : bool ref = ref false
+
+(** If true, print all constraints (including induced) and show
+    additional debug output. *)
+let debug = ref false
+
+(** Just debug all the constraints (including induced) *)
+let debug_constraints = ref false
+
+(** Debug smart alias queries *)
+let debug_aliases = ref false
+
+let smart_aliases = ref false
+
+(** If true, make the flow step a no-op *)
+let no_flow = ref false
+
+(** If true, disable subtyping (unification at all levels) *)
+let no_sub = ref false
+
+(** If true, treat indexed edges as regular subtyping *)
+let analyze_mono = ref true
+
+(** A list of equality constraints. *)
+let eq_worklist : tconstraint Q.t = Q.create ()
+
+(** A list of leq constraints. *)
+let leq_worklist : tconstraint Q.t = Q.create ()
+
+let path_worklist : (lblinfo path) Q.t = Q.create ()
+
+let path_hash : (lblinfo path) PH.t = PH.create 32
+
+(** A count of the constraints introduced from the AST. Used for debugging. *)
+let toplev_count = ref 0
+
+(** A hashtable containing stamp pairs of labels that must be aliased. *)
+let cached_aliases : (int * int,unit) H.t = H.create 64
+
+(** A hashtable mapping pairs of tau's to their join node. *)
+let join_cache : (int * int, tau) H.t = H.create 64
+
+(***********************************************************************)
+(*                                                                     *)
+(* Utility Functions                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+let find = U.deref
+
+let die s =
+  Printf.printf "*******\nAssertion failed: %s\n*******\n" s;
+  assert false
+
+let fresh_appsite : (unit -> int) =
+  let appsite_index = ref 0 in
+    fun () ->
+      incr appsite_index;
+      !appsite_index
+
+(** Generate a unique integer. *)
+let fresh_index : (unit -> int) =
+  let counter = ref 0 in
+    fun () ->
+      incr counter;
+      !counter
+
+let fresh_stamp : (unit -> int) =
+  let stamp = ref 0 in
+    fun () ->
+      incr stamp;
+      !stamp
+
+(** Return a unique integer representation of a tau *)
+let get_stamp (t : tau) : int =
+  match find t with
+      Var v -> v.v_stamp
+    | Ref r -> r.r_stamp
+    | Pair p -> p.p_stamp
+    | Fun f -> f.f_stamp
+
+(** Negate a polarity. *)
+let negate (p : polarity) : polarity =
+  match p with
+      Pos -> Neg
+    | Neg -> Pos
+    | Sub -> die "negate"
+
+(** Consistency checks for inferred types *)
+let pair_or_var (t : tau) =
+  match find t with
+      Pair _ -> true
+    | Var _ -> true
+    | _ -> false
+
+let ref_or_var (t : tau) =
+  match find t with
+      Ref _ -> true
+    | Var _ -> true
+    | _ -> false
+
+let fun_or_var (t : tau) =
+  match find t with
+      Fun _ -> true
+    | Var _ -> true
+    |  _ -> false
+
+
+
+(** Apply [f] structurally down [t]. Guaranteed to terminate, even if [t]
+    is recursive *)
+let iter_tau f t =
+  let visited : (int,tau) H.t = H.create 4 in
+  let rec iter_tau' t =
+    if H.mem visited (get_stamp t) then () else
+      begin
+        f t;
+        H.add visited (get_stamp t) t;
+        match U.deref t with
+            Pair p ->
+              iter_tau' p.ptr;
+              iter_tau' p.lam
+          | Fun f ->
+              List.iter iter_tau' (f.args);
+              iter_tau' f.ret
+          | Ref r -> iter_tau' r.points_to
+          | _ -> ()
+      end
+  in
+    iter_tau' t
+
+(* Extract a label's bounds according to [positive] and [upper]. *)
+let get_bounds (p :polarity ) (upper : bool) (l : label) : lblinfo boundset =
+  let li = find l in
+    match p with
+        Pos -> if upper then li.p_ubounds else li.p_lbounds
+      | Neg -> if upper then li.n_ubounds else li.n_lbounds
+      | Sub -> if upper then li.m_ubounds else li.m_lbounds
+
+let equal_tau (t : tau) (t' : tau) =
+  get_stamp t = get_stamp t'
+
+let get_label_stamp (l : label) : int =
+  (find l).l_stamp
+
+(** Return true if [t] is global (treated monomorphically) *)
+let get_global (t : tau) : bool =
+  match find t with
+      Var v -> v.v_global
+    | Ref r -> r.r_global
+    | Pair p -> p.p_global
+    | Fun f -> f.f_global
+
+let is_ret_label l = (find l).l_ret  || (find l).l_global (* todo - check *)
+
+let is_param_label l = (find l).l_param || (find l).l_global
+
+let is_global_label l = (find l).l_global
+
+let is_seeded_label l = (find l).l_seeded
+
+let set_global_label (l : label) (b : bool) : unit =
+  assert ((not (is_global_label l)) || b);
+  (U.deref l).l_global <- b
+
+(** Aliases for set_global *)
+let global_tau = get_global
+
+
+(** Get_global for lvalues *)
+let global_lvalue lv = get_global lv.contents
+
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Printing Functions                                                  *)
+(*                                                                     *)
+(***********************************************************************)
+
+let string_of_configuration (c, i, i') =
+  let context = match c with
+      Open -> "O"
+    | Closed -> "C"
+  in
+    Printf.sprintf "(%s,%d,%d)" context i i'
+
+let string_of_polarity p =
+  match p with
+      Pos -> "+"
+    | Neg -> "-"
+    | Sub -> "M"
+
+(** Convert a label to a string, short representation *)
+let string_of_label (l : label) : string =
+  "\"" ^ (find l).l_name ^ "\""
+
+(** Return true if the element [e] is present in the association list,
+    according to uref equality *)
+let rec assoc_list_mem (e : tau) (l : association list) =
+  match l with
+    | [] -> None
+    | (h, s, so) :: t ->
+        if U.equal (h,e) then Some (s, so) else assoc_list_mem e t
+
+(** Given a tau, create a unique recursive variable name. This should always
+    return the same name for a given tau *)
+let fresh_recvar_name (t : tau) : string =
+  match find t with
+      Pair p -> "rvp" ^ string_of_int p.p_stamp
+    | Ref r -> "rvr" ^ string_of_int r.r_stamp
+    | Fun f -> "rvf" ^ string_of_int f.f_stamp
+    | _ -> die "fresh_recvar_name"
+
+
+(** Return a string representation of a tau, using association lists. *)
+let string_of_tau (t : tau) : string =
+  let tau_map : association list ref = ref [] in
+  let rec string_of_tau' t =
+    match assoc_list_mem t !tau_map with
+        Some (s, so) -> (* recursive type. see if a var name has been set *)
+          begin
+            match !so with
+                None ->
+                  let rv = fresh_recvar_name t in
+                    s := "u " ^ rv ^ "." ^ !s;
+                    so := Some rv;
+                    rv
+              | Some rv -> rv
+          end
+      | None -> (* type's not recursive. Add it to the assoc list and cont. *)
+          let s = ref ""
+          and so : string option ref = ref None in
+            tau_map := (t, s, so) :: !tau_map;
+            begin
+              match find t with
+                  Var v -> s := v.v_name;
+                | Pair p ->
+                    assert (ref_or_var p.ptr);
+                    assert (fun_or_var p.lam);
+                    s := "{";
+                    s := !s ^ string_of_tau' p.ptr;
+                    s := !s ^ ",";
+                    s := !s ^ string_of_tau' p.lam;
+                    s := !s ^"}"
+                | Ref r ->
+                    assert (pair_or_var r.points_to);
+                    s := "ref(|";
+                    s := !s ^ string_of_label r.rl;
+                    s := !s ^ "|,";
+                    s := !s ^ string_of_tau' r.points_to;
+                    s := !s ^ ")"
+                | Fun f ->
+                    assert (pair_or_var f.ret);
+                    let rec string_of_args = function
+                        h :: [] ->
+                          assert (pair_or_var h);
+                          s := !s ^ string_of_tau' h
+                      | h :: t ->
+                          assert (pair_or_var h);
+                          s := !s ^ string_of_tau' h ^ ",";
+                          string_of_args t
+                      | [] -> ()
+                    in
+                      s := "fun(|";
+                      s := !s ^ string_of_label f.fl;
+                      s := !s ^ "|,";
+                      s := !s ^ "<";
+                      if List.length f.args > 0 then string_of_args f.args
+                      else s := !s ^ "void";
+                      s := !s ^">,";
+                      s := !s ^ string_of_tau' f.ret;
+                      s := !s ^ ")"
+            end;
+            tau_map := List.tl !tau_map;
+            !s
+  in
+    string_of_tau' t
+
+(** Convert an lvalue to a string *)
+let rec string_of_lvalue (lv : lvalue) : string =
+  let contents = string_of_tau lv.contents
+  and l = string_of_label lv.l in
+    assert (pair_or_var lv.contents); (* do a consistency check *)
+    Printf.sprintf "[%s]^(%s)" contents l
+
+let print_path (p : lblinfo path) : unit =
+  let string_of_pkind = function
+      Positive -> "p"
+    | Negative -> "n"
+    | Match -> "m"
+    | Seed -> "s"
+  in
+    Printf.printf
+      "%s --%s--> %s (%d) : "
+      (string_of_label p.head)
+      (string_of_pkind p.kind)
+      (string_of_label p.tail)
+      (PathHash.hash p)
+
+(** Print a list of tau elements, comma separated *)
+let rec print_tau_list (l : tau list) : unit =
+  let rec print_t_strings = function
+      h :: [] -> print_endline h
+    | h :: t ->
+        print_string h;
+        print_string ", ";
+        print_t_strings t
+    | [] -> ()
+  in
+    print_t_strings (List.map string_of_tau l)
+
+let print_constraint (c : tconstraint) =
+  match c with
+      Unification (t, t') ->
+        let lhs = string_of_tau t
+        and rhs = string_of_tau t' in
+          Printf.printf "%s == %s\n" lhs rhs
+    | Leq (t, (i, p), t') ->
+        let lhs = string_of_tau t
+        and rhs = string_of_tau t' in
+          Printf.printf "%s <={%d,%s} %s\n" lhs i (string_of_polarity p) rhs
+
+(***********************************************************************)
+(*                                                                     *)
+(* Type Operations -- these do not create any constraints              *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Create an lvalue with label [lbl] and tau contents [t]. *)
+let make_lval (lbl, t : label * tau) : lvalue =
+  {l = lbl; contents = t}
+
+let make_label_int (is_global : bool) (name :string) (vio : Cil.varinfo option) : label =
+  let locc =
+    match vio with
+        Some vi -> C.add (fresh_index (), name, vi) C.empty
+      | None -> C.empty
+  in
+    U.uref {
+      l_name = name;
+      l_global = is_global;
+      l_stamp = fresh_stamp ();
+      loc = locc;
+      aliases = locc;
+      p_ubounds = B.empty;
+      p_lbounds = B.empty;
+      n_ubounds = B.empty;
+      n_lbounds = B.empty;
+      m_ubounds = B.empty;
+      m_lbounds = B.empty;
+      m_upath = P.empty;
+      m_lpath = P.empty;
+      n_upath = P.empty;
+      n_lpath = P.empty;
+      p_upath = P.empty;
+      p_lpath = P.empty;
+      l_seeded = false;
+      l_ret = false;
+      l_param = false
+    }
+
+(** Create a new label with name [name]. Also adds a fresh constant
+    with name [name] to this label's aliases set. *)
+let make_label (is_global : bool) (name : string) (vio : Cil.varinfo option) : label =
+  make_label_int is_global name vio
+
+(** Create a new label with an unspecified name and an empty alias set. *)
+let fresh_label (is_global : bool) : label =
+  let index = fresh_index () in
+    make_label_int is_global ("l_" ^ string_of_int index) None
+
+(** Create a fresh bound (edge in the constraint graph). *)
+let make_bound (i, a : int * label) : lblinfo bound =
+  {index = i; info = a}
+
+let make_tau_bound (i, a : int * tau) : tinfo bound =
+  {index = i; info = a}
+
+(** Create a fresh named variable with name '[name]. *)
+let make_var (b: bool) (name : string) : tau =
+  U.uref (Var {v_name = ("'" ^ name);
+               v_hole = H.create 8;
+               v_stamp = fresh_index ();
+               v_global = b;
+               v_mlbs = B.empty;
+               v_mubs = B.empty;
+               v_plbs = B.empty;
+               v_pubs = B.empty;
+               v_nlbs = B.empty;
+               v_nubs = B.empty})
+
+(** Create a fresh unnamed variable (name will be 'fv). *)
+let fresh_var (is_global : bool) : tau =
+  make_var is_global ("fv" ^ string_of_int (fresh_index ()))
+
+(** Create a fresh unnamed variable (name will be 'fi). *)
+let fresh_var_i (is_global : bool) : tau =
+  make_var is_global ("fi" ^ string_of_int (fresh_index()))
+
+(** Create a Fun constructor. *)
+let make_fun (lbl, a, r : label * (tau list) * tau) : tau =
+  U.uref (Fun {fl = lbl;
+               f_stamp = fresh_index ();
+               f_global = false;
+               args = a;
+               ret = r })
+
+(** Create a Ref constructor. *)
+let make_ref (lbl,pt : label * tau) : tau =
+  U.uref (Ref {rl = lbl;
+               r_stamp = fresh_index ();
+               r_global = false;
+               points_to = pt})
+
+(** Create a Pair constructor. *)
+let make_pair (p,f : tau * tau) : tau =
+  U.uref (Pair {ptr = p;
+                p_stamp = fresh_index ();
+                p_global = false;
+                lam = f})
+
+(** Copy the toplevel constructor of [t], putting fresh variables in each
+    argement of the constructor. *)
+let copy_toplevel (t : tau) : tau =
+  match find t with
+      Pair _ -> make_pair (fresh_var_i false, fresh_var_i false)
+    | Ref  _ -> make_ref (fresh_label false, fresh_var_i false)
+    | Fun  f ->
+        let fresh_fn = fun _ -> fresh_var_i false in
+          make_fun (fresh_label false,
+                    List.map fresh_fn f.args, fresh_var_i false)
+    | _ -> die "copy_toplevel"
+
+
+let has_same_structure (t : tau) (t' : tau) =
+  match find t, find t' with
+      Pair _, Pair _ -> true
+    | Ref _, Ref _ -> true
+    | Fun _, Fun _ -> true
+    | Var _, Var _ -> true
+    | _ -> false
+
+
+let pad_args (f, f' : finfo * finfo) : unit =
+  let padding = ref ((List.length f.args) - (List.length f'.args))
+  in
+    if !padding == 0 then ()
+    else
+      let to_pad =
+        if !padding > 0 then f' else (padding := -(!padding); f)
+      in
+        for i = 1 to !padding do
+          to_pad.args <- to_pad.args @ [fresh_var false]
+        done
+
+
+let pad_args2 (fi, tlr : finfo * tau list ref) : unit =
+  let padding = ref (List.length fi.args - List.length !tlr)
+  in
+    if !padding == 0 then ()
+    else
+      if !padding > 0 then
+        for i = 1 to !padding do
+          tlr := !tlr @ [fresh_var false]
+        done
+      else
+        begin
+          padding := -(!padding);
+          for i = 1 to !padding do
+            fi.args <- fi.args @ [fresh_var false]
+          done
+        end
+
+(***********************************************************************)
+(*                                                                     *)
+(* Constraint Generation/ Resolution                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+(** Make the type a global type *)
+let set_global (t : tau) (b : bool) : unit =
+  let set_global_down t =
+    match find t with
+        Var v -> v.v_global <- true
+      | Ref r -> set_global_label r.rl true
+      | Fun f -> set_global_label f.fl true
+      | _ -> ()
+  in
+    if !debug && b then Printf.printf "Set global: %s\n" (string_of_tau t);
+    assert ((not (get_global t)) || b);
+    if b then iter_tau set_global_down t;
+    match find t with
+        Var v -> v.v_global <- b
+      | Ref r -> r.r_global <- b
+      | Pair p -> p.p_global <- b
+      | Fun f -> f.f_global <- b
+
+
+let rec unify_int (t, t' : tau * tau) : unit =
+  if equal_tau t t' then ()
+  else
+    let ti, ti' = find t, find t' in
+      U.unify combine (t, t');
+      match ti, ti' with
+          Var v, Var v' ->
+            set_global t' (v.v_global || get_global t');
+            merge_vholes (v, v');
+            merge_vlbs (v, v');
+            merge_vubs (v, v')
+        | Var v, _ ->
+            set_global t' (v.v_global || get_global t');
+            trigger_vhole v t';
+            notify_vlbs t v;
+            notify_vubs t v
+        | _, Var v ->
+            set_global t (v.v_global || get_global t);
+            trigger_vhole v t;
+            notify_vlbs t' v;
+            notify_vubs t' v
+        | Ref r, Ref r' ->
+            set_global t (r.r_global || r'.r_global);
+            unify_ref (r, r')
+        | Fun f, Fun f' ->
+            set_global t (f.f_global || f'.f_global);
+            unify_fun (f, f')
+        | Pair p, Pair p' -> ()
+        | _ -> raise Inconsistent
+and notify_vlbs (t : tau) (vi : vinfo) : unit =
+  let notify p bounds =
+    List.iter
+      (fun b ->
+         add_constraint (Unification (b.info,copy_toplevel t));
+         add_constraint (Leq (b.info, (b.index, p), t)))
+      bounds
+  in
+    notify Sub (B.elements vi.v_mlbs);
+    notify Pos (B.elements vi.v_plbs);
+    notify Neg (B.elements vi.v_nlbs)
+and notify_vubs (t : tau) (vi : vinfo) : unit =
+  let notify p bounds =
+    List.iter
+      (fun b ->
+         add_constraint (Unification (b.info,copy_toplevel t));
+         add_constraint (Leq (t, (b.index, p), b.info)))
+      bounds
+  in
+    notify Sub (B.elements vi.v_mubs);
+    notify Pos (B.elements vi.v_pubs);
+    notify Neg (B.elements vi.v_nubs)
+and unify_ref (ri,ri' : rinfo * rinfo) : unit =
+  add_constraint (Unification (ri.points_to, ri'.points_to))
+and unify_fun (fi, fi' : finfo * finfo) : unit =
+  let rec union_args  = function
+      _, [] -> false
+    | [], _ -> true
+    | h :: t, h' :: t' ->
+        add_constraint (Unification (h, h'));
+        union_args(t, t')
+  in
+    unify_label(fi.fl, fi'.fl);
+    add_constraint (Unification (fi.ret, fi'.ret));
+    if union_args (fi.args, fi'.args) then fi.args <- fi'.args;
+and unify_label (l, l' : label * label) : unit =
+  let pick_name (li, li' : lblinfo * lblinfo) =
+    if String.length li.l_name > 1 && String.sub (li.l_name) 0 2 = "l_" then
+      li.l_name <- li'.l_name
+    else ()
+  in
+  let combine_label (li, li' : lblinfo *lblinfo) : lblinfo =
+    let rm_self b = not (li.l_stamp = get_label_stamp b.info)
+    in
+      pick_name (li, li');
+      li.l_global <- li.l_global || li'.l_global;
+      li.aliases <- C.union li.aliases li'.aliases;
+      li.p_ubounds <- B.union li.p_ubounds li'.p_ubounds;
+      li.p_lbounds <- B.union li.p_lbounds li'.p_lbounds;
+      li.n_ubounds <- B.union li.n_ubounds li'.n_ubounds;
+      li.n_lbounds <- B.union li.n_lbounds li'.n_lbounds;
+      li.m_ubounds <- B.union li.m_ubounds (B.filter rm_self li'.m_ubounds);
+      li.m_lbounds <- B.union li.m_lbounds (B.filter rm_self li'.m_lbounds);
+      li.m_upath <- P.union li.m_upath li'.m_upath;
+      li.m_lpath<- P.union li.m_lpath li'.m_lpath;
+      li.n_upath <- P.union li.n_upath li'.n_upath;
+      li.n_lpath <- P.union li.n_lpath li'.n_lpath;
+      li.p_upath <- P.union li.p_upath li'.p_upath;
+      li.p_lpath <- P.union li.p_lpath li'.p_lpath;
+      li.l_seeded <- li.l_seeded || li'.l_seeded;
+      li.l_ret <- li.l_ret || li'.l_ret;
+      li.l_param <- li.l_param || li'.l_param;
+      li
+  in
+    if !debug_constraints then
+       Printf.printf "%s == %s\n" (string_of_label l) (string_of_label l');
+    U.unify combine_label (l, l')
+and merge_vholes (vi, vi' : vinfo * vinfo) : unit =
+  H.iter
+    (fun i -> fun _ -> H.replace vi'.v_hole i ())
+    vi.v_hole
+and merge_vlbs (vi, vi' : vinfo * vinfo) : unit =
+  vi'.v_mlbs <- B.union vi.v_mlbs vi'.v_mlbs;
+  vi'.v_plbs <- B.union vi.v_plbs vi'.v_plbs;
+  vi'.v_nlbs <- B.union vi.v_nlbs vi'.v_nlbs
+and merge_vubs (vi, vi' : vinfo * vinfo) : unit =
+  vi'.v_mubs <- B.union vi.v_mubs vi'.v_mubs;
+  vi'.v_pubs <- B.union vi.v_pubs vi'.v_pubs;
+  vi'.v_nubs <- B.union vi.v_nubs vi'.v_nubs
+and trigger_vhole (vi : vinfo) (t : tau) =
+  let add_self_loops (t : tau) : unit =
+    match find t with
+        Var v ->
+          H.iter
+            (fun i -> fun _ -> H.replace v.v_hole i ())
+            vi.v_hole
+      | Ref r ->
+          H.iter
+            (fun i -> fun _ ->
+               leq_label (r.rl, (i, Pos), r.rl);
+               leq_label (r.rl, (i, Neg), r.rl))
+            vi.v_hole
+      | Fun f ->
+          H.iter
+            (fun i -> fun _ ->
+               leq_label (f.fl, (i, Pos), f.fl);
+               leq_label (f.fl, (i, Neg), f.fl))
+            vi.v_hole
+      | _ -> ()
+  in
+    iter_tau add_self_loops t
+(** Pick the representative info for two tinfo's. This function prefers the
+  first argument when both arguments are the same structure, but when
+  one type is a structure and the other is a var, it picks the structure.
+  All other actions (e.g., updating the info) is done in unify_int *)
+and combine (ti, ti' : tinfo * tinfo) : tinfo =
+  match ti, ti' with
+      Var _, _ -> ti'
+    | _, _ -> ti
+and leq_int (t, (i, p), t') : unit =
+  if equal_tau t t' then ()
+  else
+    let ti, ti' = find t, find t' in
+      match ti, ti' with
+          Var v, Var v' ->
+            begin
+              match p with
+                  Pos ->
+                    v.v_pubs <- B.add (make_tau_bound (i, t')) v.v_pubs;
+                    v'.v_plbs <- B.add (make_tau_bound (i, t)) v'.v_plbs
+                | Neg ->
+                    v.v_nubs <- B.add (make_tau_bound (i, t')) v.v_nubs;
+                    v'.v_nlbs <- B.add (make_tau_bound (i, t)) v'.v_nlbs
+                | Sub ->
+                    v.v_mubs <- B.add (make_tau_bound (i, t')) v.v_mubs;
+                    v'.v_mlbs <- B.add (make_tau_bound (i, t)) v'.v_mlbs
+            end
+        | Var v, _ ->
+            add_constraint (Unification (t, copy_toplevel t'));
+            add_constraint (Leq (t, (i, p), t'))
+        | _, Var v ->
+            add_constraint (Unification (t', copy_toplevel t));
+            add_constraint (Leq (t, (i, p), t'))
+        | Ref r, Ref r' -> leq_ref (r, (i, p), r')
+        | Fun f, Fun f' -> add_constraint (Unification (t, t'))
+        | Pair pr, Pair pr' ->
+            add_constraint (Leq (pr.ptr, (i, p), pr'.ptr));
+            add_constraint (Leq (pr.lam, (i, p), pr'.lam))
+        | _ -> raise Inconsistent
+and leq_ref (ri, (i, p), ri') : unit =
+  let add_self_loops (t : tau) : unit =
+    match find t with
+        Var v -> H.replace v.v_hole i ()
+      | Ref r ->
+          leq_label (r.rl, (i, Pos), r.rl);
+          leq_label (r.rl, (i, Neg), r.rl)
+      | Fun f ->
+          leq_label (f.fl, (i, Pos), f.fl);
+          leq_label (f.fl, (i, Neg), f.fl)
+      | _ -> ()
+  in
+    iter_tau add_self_loops ri.points_to;
+    add_constraint (Unification (ri.points_to, ri'.points_to));
+    leq_label(ri.rl, (i, p), ri'.rl)
+and leq_label (l,(i, p), l') : unit =
+  if !debug_constraints then
+    Printf.printf
+      "%s <={%d,%s} %s\n"
+      (string_of_label l) i (string_of_polarity p) (string_of_label l');
+  let li, li' = find l, find l' in
+    match p with
+        Pos ->
+          li.l_ret <- true;
+          li.p_ubounds <- B.add (make_bound (i, l')) li.p_ubounds;
+          li'.p_lbounds <- B.add (make_bound (i, l)) li'.p_lbounds
+      | Neg ->
+          li'.l_param <- true;
+          li.n_ubounds <- B.add (make_bound (i, l')) li.n_ubounds;
+          li'.n_lbounds <- B.add (make_bound (i, l)) li'.n_lbounds
+      | Sub ->
+          if U.equal (l, l') then ()
+          else
+            begin
+              li.m_ubounds <- B.add (make_bound(0, l')) li.m_ubounds;
+              li'.m_lbounds <- B.add (make_bound(0, l)) li'.m_lbounds
+            end
+and add_constraint_int (c : tconstraint) (toplev : bool) =
+  if !debug_constraints && toplev then
+    begin
+      Printf.printf "%d:>" !toplev_count;
+      print_constraint c;
+      incr toplev_count
+    end
+  else
+    if !debug_constraints then print_constraint c else ();
+  begin
+    match c with
+        Unification _ -> Q.add c eq_worklist
+      | Leq _ -> Q.add c leq_worklist
+  end;
+  solve_constraints ()
+and add_constraint (c : tconstraint) =
+  add_constraint_int c false
+and add_toplev_constraint (c : tconstraint) =
+  if !print_constraints && not !debug_constraints then
+    begin
+      Printf.printf "%d:>" !toplev_count;
+      incr toplev_count;
+      print_constraint c
+    end
+  else ();
+  add_constraint_int c true
+and fetch_constraint () : tconstraint option =
+  try Some (Q.take eq_worklist)
+  with Q.Empty -> (try Some (Q.take leq_worklist)
+                   with Q.Empty -> None)
+(** The main solver loop. *)
+and solve_constraints () : unit =
+  match fetch_constraint () with
+      Some c ->
+        begin
+          match c with
+              Unification (t, t') -> unify_int (t, t')
+            | Leq (t, (i, p), t') ->
+                if !no_sub then unify_int (t, t')
+                else
+                  if !analyze_mono then leq_int (t, (0, Sub), t')
+                  else leq_int (t, (i, p), t')
+        end;
+        solve_constraints ()
+    | None -> ()
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Interface Functions                                                 *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Return the contents of the lvalue. *)
+let rvalue (lv : lvalue) : tau =
+  lv.contents
+
+(** Dereference the rvalue. If it does not have enough structure to support
+  the operation, then the correct structure is added via new unification
+  constraints. *)
+let rec deref (t : tau) : lvalue =
+  match U.deref t with
+      Pair p ->
+        begin
+          match U.deref p.ptr with
+              Var _ ->
+                let is_global = global_tau p.ptr in
+                let points_to = fresh_var is_global in
+                let l = fresh_label is_global in
+                let r = make_ref (l, points_to)
+                in
+                  add_toplev_constraint (Unification (p.ptr, r));
+                  make_lval (l, points_to)
+            | Ref r -> make_lval (r.rl, r.points_to)
+            | _ -> raise WellFormed
+        end
+    | Var v ->
+        let is_global = global_tau t in
+          add_toplev_constraint
+            (Unification (t, make_pair (fresh_var is_global,
+                                        fresh_var is_global)));
+          deref t
+    | _ -> raise WellFormed
+
+(** Form the union of [t] and [t'], if it doesn't exist already. *)
+let join (t : tau) (t' : tau) : tau =
+  try H.find join_cache (get_stamp t, get_stamp t')
+  with Not_found ->
+    let t'' = fresh_var false in
+      add_toplev_constraint (Leq (t, (0, Sub), t''));
+      add_toplev_constraint (Leq (t', (0, Sub), t''));
+      H.add join_cache (get_stamp t, get_stamp t') t'';
+      t''
+
+(** Form the union of a list [tl], expected to be the initializers of some
+  structure or array type. *)
+let join_inits (tl : tau list) : tau =
+  let t' = fresh_var false in
+    List.iter
+      (fun t -> add_toplev_constraint (Leq (t, (0, Sub), t')))
+      tl;
+    t'
+
+(** Take the address of an lvalue. Does not add constraints. *)
+let address (lv  : lvalue) : tau =
+  make_pair (make_ref (lv.l, lv.contents), fresh_var false)
+
+(** For this version of golf, instantiation is handled at [apply] *)
+let instantiate (lv : lvalue) (i : int) : lvalue =
+  lv
+
+(** Constraint generated from assigning [t] to [lv]. *)
+let assign (lv : lvalue) (t : tau) : unit =
+  add_toplev_constraint (Leq (t, (0, Sub), lv.contents))
+
+let assign_ret (i : int) (lv : lvalue) (t : tau) : unit =
+  add_toplev_constraint (Leq (t, (i, Pos), lv.contents))
+
+(** Project out the first (ref) component or a pair. If the argument [t] has
+  no discovered structure, raise NoContents. *)
+let proj_ref (t : tau) : tau =
+  match U.deref t with
+      Pair p -> p.ptr
+    | Var v -> raise NoContents
+    | _ ->  raise WellFormed
+
+(* Project out the second (fun) component of a pair. If the argument [t] has
+   no discovered structure, create it on the fly by adding constraints. *)
+let proj_fun (t : tau) : tau =
+  match U.deref t with
+      Pair p -> p.lam
+    | Var v ->
+        let p, f = fresh_var false, fresh_var false in
+          add_toplev_constraint (Unification (t, make_pair(p, f)));
+          f
+    | _ -> raise WellFormed
+
+let get_args (t : tau) : tau list =
+  match U.deref t with
+      Fun f -> f.args
+    | _ -> raise WellFormed
+
+let get_finfo (t : tau) : finfo =
+  match U.deref t with
+      Fun f -> f
+    | _ -> raise WellFormed
+
+(** Function type [t] is applied to the arguments [actuals]. Unifies the
+  actuals with the formals of [t]. If no functions have been discovered for
+  [t] yet, create a fresh one and unify it with t. The result is the return
+  value of the function plus the index of this application site. *)
+let apply (t : tau) (al : tau list) : (tau * int) =
+  let i = fresh_appsite () in
+  let f = proj_fun t in
+  let actuals = ref al in
+  let fi,ret =
+    match U.deref f with
+        Fun fi -> fi, fi.ret
+      | Var v ->
+          let new_l, new_ret, new_args =
+            fresh_label false, fresh_var false,
+            List.map (function _ -> fresh_var false) !actuals
+          in
+          let new_fun = make_fun (new_l, new_args, new_ret) in
+            add_toplev_constraint (Unification (new_fun, f));
+            (get_finfo new_fun, new_ret)
+      | _ -> raise WellFormed
+  in
+    pad_args2 (fi, actuals);
+    List.iter2
+      (fun actual -> fun formal ->
+         add_toplev_constraint (Leq (actual,(i, Neg), formal)))
+      !actuals fi.args;
+    (ret, i)
+
+(** Create a new function type with name [name], list of formal arguments
+  [formals], and return value [ret]. Adds no constraints. *)
+let make_function (name : string) (formals : lvalue list) (ret : tau) : tau =
+  let f = make_fun (make_label false name None,
+                    List.map (fun x -> rvalue x) formals,
+                    ret)
+  in
+    make_pair (fresh_var false, f)
+
+(** Create an lvalue. If [is_global] is true, the lvalue will be treated
+    monomorphically. *)
+let make_lvalue (is_global : bool) (name : string) (vio : Cil.varinfo option) : lvalue =
+  if !debug && is_global then
+    Printf.printf "Making global lvalue : %s\n" name
+  else ();
+  make_lval (make_label is_global name vio, make_var is_global name)
+
+(** Create a fresh non-global named variable. *)
+let make_fresh (name : string) : tau =
+  make_var false name
+
+(** The default type for constants. *)
+let bottom () : tau =
+  make_var false "bottom"
+
+(** Unify the result of a function with its return value. *)
+let return (t : tau) (t' : tau) =
+  add_toplev_constraint (Leq (t', (0, Sub), t))
+
+(***********************************************************************)
+(*                                                                     *)
+(* Query/Extract Solutions                                             *)
+(*                                                                     *)
+(***********************************************************************)
+
+let make_summary = leq_label
+
+let path_signature k l l' b : int list =
+  let ksig =
+    match k with
+        Positive -> 1
+      | Negative -> 2
+      | _ -> 3
+  in
+    [ksig;
+     get_label_stamp l;
+     get_label_stamp l';
+     if b then 1 else 0]
+
+let make_path (k, l, l', b) =
+  let psig = path_signature k l l' b in
+    if PH.mem path_hash psig then ()
+    else
+      let new_path = {kind = k; head = l; tail = l'; reached_global = b}
+      and li, li' = find l, find l' in
+        PH.add path_hash psig new_path;
+        Q.add new_path path_worklist;
+        begin
+          match k with
+              Positive ->
+                li.p_upath <- P.add new_path li.p_upath;
+                li'.p_lpath <- P.add new_path li'.p_lpath
+            | Negative ->
+                li.n_upath <- P.add new_path li.n_upath;
+                li'.n_lpath <- P.add new_path li'.n_lpath
+            | _ ->
+                li.m_upath <- P.add new_path li.m_upath;
+                li'.m_lpath <- P.add new_path li'.m_lpath
+        end;
+        if !debug then
+          begin
+            print_string "Discovered path : ";
+            print_path new_path;
+            print_newline ()
+          end
+
+let backwards_tabulate (l : label) : unit =
+  let rec loop () =
+    let rule1 p =
+      if !debug then print_endline "rule1";
+      B.iter
+        (fun lb ->
+           make_path (Match, lb.info, p.tail,
+                      p.reached_global || is_global_label p.head))
+        (find p.head).m_lbounds
+    and rule2 p =
+      if !debug then print_endline "rule2";
+      B.iter
+        (fun lb ->
+           make_path (Negative, lb.info, p.tail,
+                      p.reached_global || is_global_label p.head))
+        (find p.head).n_lbounds
+    and rule2m p =
+      if !debug then print_endline "rule2m";
+      B.iter
+        (fun lb ->
+           make_path (Match, lb.info, p.tail,
+                      p.reached_global || is_global_label p.head))
+        (find p.head).n_lbounds
+    and rule3 p =
+      if !debug then print_endline "rule3";
+      B.iter
+        (fun lb ->
+           make_path (Positive, lb.info, p.tail,
+                      p.reached_global || is_global_label p.head))
+        (find p.head).p_lbounds
+    and rule4 p =
+      if !debug then print_endline "rule4";
+      B.iter
+        (fun lb ->
+           make_path(Negative, lb.info, p.tail,
+                     p.reached_global || is_global_label p.head))
+        (find p.head).m_lbounds
+    and rule5 p =
+      if !debug then print_endline "rule5";
+      B.iter
+        (fun lb ->
+           make_path (Positive, lb.info, p.tail,
+                      p.reached_global || is_global_label p.head))
+        (find p.head).m_lbounds
+    and rule6 p =
+      if !debug then print_endline "rule6";
+      B.iter
+        (fun lb ->
+           if is_seeded_label lb.info then ()
+           else
+             begin
+               (find lb.info).l_seeded <- true; (* set seeded *)
+               make_path (Seed, lb.info, lb.info,
+                          is_global_label lb.info)
+             end)
+        (find p.head).p_lbounds
+    and rule7 p =
+      if !debug then print_endline "rule7";
+      if not (is_ret_label p.tail && is_param_label p.head) then ()
+      else
+        B.iter
+          (fun lb ->
+             B.iter
+               (fun ub ->
+                  if lb.index = ub.index then
+                    begin
+                      if !debug then
+                        Printf.printf "New summary : %s %s\n"
+                          (string_of_label lb.info)
+                          (string_of_label ub.info);
+                      make_summary (lb.info, (0, Sub), ub.info);
+                      (* rules 1, 4, and 5 *)
+                      P.iter
+                        (fun ubp -> (* rule 1 *)
+                           make_path (Match, lb.info, ubp.tail,
+                                      ubp.reached_global))
+                        (find ub.info).m_upath;
+                      P.iter
+                        (fun ubp -> (* rule 4 *)
+                           make_path (Negative, lb.info, ubp.tail,
+                                      ubp.reached_global))
+                        (find ub.info).n_upath;
+                      P.iter
+                        (fun ubp -> (* rule 5 *)
+                           make_path (Positive, lb.info, ubp.tail,
+                                      ubp.reached_global))
+                        (find ub.info).p_upath
+                    end)
+               (find p.tail).p_ubounds)
+          (find p.head).n_lbounds
+    in
+    let matched_backward_rules p =
+      rule1 p;
+      if p.reached_global then rule2m p else rule2 p;
+      rule3 p;
+      rule6 p;
+      rule7 p
+    and negative_backward_rules p =
+      rule2 p;
+      rule3 p;
+      rule4 p;
+      rule6 p;
+      rule7 p
+    and positive_backward_rules p =
+      rule3 p;
+      rule5 p;
+      rule6 p;
+      rule7 p
+    in (* loop *)
+      if Q.is_empty path_worklist then ()
+      else
+        let p = Q.take path_worklist in
+          if !debug then
+            begin
+              print_string "Processing path: ";
+              print_path p;
+              print_newline ()
+            end;
+          begin
+            match p.kind with
+                Positive ->
+                  if is_global_label p.tail then matched_backward_rules p
+                  else positive_backward_rules p
+              | Negative -> negative_backward_rules p
+              | _ -> matched_backward_rules p
+          end;
+          loop ()
+  in (* backwards_tabulate *)
+    if !debug then
+      begin
+        Printf.printf "Tabulating for %s..." (string_of_label l);
+        if is_global_label l then print_string "(global)";
+        print_newline ()
+      end;
+    make_path (Seed, l, l, is_global_label l);
+    loop ()
+
+let collect_ptsets (l : label) : constantset = (* todo -- cache aliases *)
+  let li = find l
+  and collect init s =
+    P.fold (fun x a -> C.union a (find x.head).aliases) s init
+  in
+    backwards_tabulate l;
+    collect (collect (collect li.aliases li.m_lpath) li.n_lpath) li.p_lpath
+
+let extract_ptlabel (lv : lvalue) : label option =
+  try
+    match find (proj_ref lv.contents) with
+        Var v -> None
+      | Ref r ->  Some r.rl;
+      | _ -> raise WellFormed
+  with NoContents -> None
+
+let points_to_aux (t : tau) : constant list =
+  try
+    match find (proj_ref t) with
+        Var v -> []
+      | Ref r -> C.elements (collect_ptsets r.rl)
+      | _ -> raise WellFormed
+  with NoContents -> []
+
+let points_to_names (lv : lvalue) : string list =
+  List.map (fun (_, str, _) -> str) (points_to_aux lv.contents)
+
+let points_to (lv : lvalue) : Cil.varinfo list =
+  let rec get_vinfos l : Cil.varinfo list = match l with
+    | (_, _, h) :: t -> h :: get_vinfos t
+    | [] -> []
+  in
+    get_vinfos (points_to_aux lv.contents)
+
+let epoints_to (t : tau) : Cil.varinfo list =
+  let rec get_vinfos l : Cil.varinfo list = match l with
+    | (_, _, h) :: t -> h :: get_vinfos t
+    | [] -> []
+  in
+    get_vinfos (points_to_aux t)
+
+let smart_alias_query (l : label) (l' : label) : bool =
+  (* Set of dead configurations *)
+  let dead_configs : config_map = CH.create 16 in
+    (* the set of discovered configurations *)
+  let discovered : config_map = CH.create 16 in
+  let rec filter_match (i : int) =
+    B.filter (fun (b : lblinfo bound) -> i = b.index)
+  in
+  let rec simulate c l l' =
+    let config = (c, get_label_stamp l, get_label_stamp l') in
+      if U.equal (l, l') then
+        begin
+          if !debug then
+            Printf.printf
+              "%s and %s are aliased\n"
+              (string_of_label l)
+              (string_of_label l');
+          raise APFound
+        end
+      else if CH.mem discovered config then ()
+      else
+        begin
+          if !debug_aliases then
+            Printf.printf
+              "Exploring configuration %s\n"
+              (string_of_configuration config);
+          CH.add discovered config ();
+          B.iter
+            (fun lb -> simulate c lb.info l')
+            (get_bounds Sub false l); (* epsilon closure of l *)
+          B.iter
+            (fun lb -> simulate c l lb.info)
+            (get_bounds Sub false l'); (* epsilon closure of l' *)
+          B.iter
+            (fun lb ->
+               let matching =
+                 filter_match lb.index (get_bounds Pos false l')
+               in
+                 B.iter
+                   (fun b -> simulate Closed lb.info b.info)
+                   matching;
+                 if is_global_label l' then (* positive self-loops on l' *)
+                   simulate Closed lb.info l')
+            (get_bounds Pos false l); (* positive transitions on l *)
+          if is_global_label l then
+            B.iter
+              (fun lb -> simulate Closed l lb.info)
+              (get_bounds Pos false l'); (* positive self-loops on l *)
+          begin
+            match c with  (* negative transitions on l, only if Open *)
+                Open ->
+                  B.iter
+                    (fun lb ->
+                       let matching =
+                         filter_match lb.index (get_bounds Neg false l')
+                       in
+                         B.iter
+                           (fun b -> simulate Open lb.info b.info)
+                           matching ;
+                         if is_global_label l' then (* neg self-loops on l' *)
+                           simulate Open lb.info l')
+                    (get_bounds Neg false l);
+                  if is_global_label l then
+                    B.iter
+                      (fun lb -> simulate Open l lb.info)
+                      (get_bounds Neg false l') (* negative self-loops on l *)
+              | _ -> ()
+          end;
+          (* if we got this far, then the configuration was not used *)
+          CH.add dead_configs config ();
+        end
+  in
+    try
+      begin
+        if H.mem cached_aliases (get_label_stamp l, get_label_stamp l') then
+          true
+        else
+          begin
+            simulate Open l l';
+            if !debug then
+              Printf.printf
+                "%s and %s are NOT aliased\n"
+                (string_of_label l)
+                (string_of_label l');
+            false
+          end
+      end
+    with APFound ->
+      CH.iter
+        (fun config -> fun _ ->
+           if not (CH.mem dead_configs config) then
+             H.add
+               cached_aliases
+               (get_label_stamp l, get_label_stamp l')
+               ())
+        discovered;
+      true
+
+(** todo : uses naive alias query for now *)
+let may_alias (t1 : tau) (t2 : tau) : bool =
+  try
+    let l1 =
+      match find (proj_ref t1) with
+          Ref r -> r.rl
+        | Var v -> raise NoContents
+        | _ -> raise WellFormed
+    and l2 =
+      match find (proj_ref t2) with
+          Ref r -> r.rl
+        | Var v -> raise NoContents
+        | _ -> raise WellFormed
+    in
+      not (C.is_empty (C.inter (collect_ptsets l1) (collect_ptsets l2)))
+  with NoContents -> false
+
+let alias_query (b : bool) (lvl : lvalue list) : int * int =
+  let naive_count = ref 0 in
+  let smart_count = ref 0 in
+  let lbls = List.map extract_ptlabel lvl in (* label option list *)
+  let ptsets =
+    List.map
+      (function
+           Some l -> collect_ptsets l
+         | None -> C.empty)
+      lbls in
+  let record_alias s lo s' lo' =
+    match lo, lo' with
+        Some l, Some l' ->
+          if !debug_aliases then
+            Printf.printf
+              "Checking whether %s and %s are aliased...\n"
+              (string_of_label l)
+              (string_of_label l');
+          if C.is_empty (C.inter s s') then ()
+          else
+            begin
+              incr naive_count;
+              if !smart_aliases && smart_alias_query l l' then
+                incr smart_count
+            end
+      | _ -> ()
+  in
+  let rec check_alias sets labels =
+    match sets,labels with
+        s :: st, l :: lt ->
+          List.iter2 (record_alias s l) ptsets lbls;
+          check_alias st lt
+      | [], [] -> ()
+      | _ -> die "check_alias"
+  in
+    check_alias ptsets lbls;
+    (!naive_count, !smart_count)
+
+let alias_frequency (lvl : (lvalue * bool) list) : int * int =
+  let extract_lbl (lv, b : lvalue * bool) = (lv.l, b) in
+  let naive_count = ref 0 in
+  let smart_count = ref 0 in
+  let lbls = List.map extract_lbl lvl in
+  let ptsets =
+    List.map
+      (fun (lbl, b) ->
+         if b then (find lbl).loc (* symbol access *)
+         else collect_ptsets lbl)
+      lbls in
+  let record_alias s (l, b) s' (l', b') =
+    if !debug_aliases then
+      Printf.printf
+        "Checking whether %s and %s are aliased...\n"
+        (string_of_label l)
+        (string_of_label l');
+    if C.is_empty (C.inter s s') then ()
+    else
+      begin
+        if !debug_aliases then
+          Printf.printf
+            "%s and %s are aliased naively...\n"
+            (string_of_label l)
+            (string_of_label l');
+        incr naive_count;
+        if !smart_aliases then
+          if b || b' || smart_alias_query l l' then incr smart_count
+          else
+            Printf.printf
+              "%s and %s are not aliased by smart queries...\n"
+              (string_of_label l)
+              (string_of_label l');
+      end
+  in
+  let rec check_alias sets labels =
+    match sets, labels with
+        s :: st, l :: lt ->
+          List.iter2 (record_alias s l) ptsets lbls;
+          check_alias st lt
+      | [], [] -> ()
+      | _ -> die "check_alias"
+  in
+    check_alias ptsets lbls;
+    (!naive_count, !smart_count)
+
+
+(** an interface for extracting abstract locations from this analysis *)
+
+type absloc = label
+
+let absloc_of_lvalue (l : lvalue) : absloc = l.l
+let absloc_eq (a1, a2) = smart_alias_query a1 a2
+let absloc_print_name = ref true
+let d_absloc () (p : absloc) =
+  let a = find p in
+    if !absloc_print_name then Pretty.dprintf "%s" a.l_name
+    else Pretty.dprintf "%d" a.l_stamp
+
+let phonyAddrOf (lv : lvalue) : lvalue =
+  make_lval (fresh_label true, address lv)
+
+(* transitive closure of points to, starting from l *)
+let rec tauPointsTo (l : tau) : absloc list =
+  match find l with
+      Var _ -> []
+    | Ref r -> r.rl :: tauPointsTo r.points_to
+    | _ -> []
+
+let rec absloc_points_to (l : lvalue) : absloc list =
+  tauPointsTo l.contents
+
+
+(** The following definitions are only introduced for the
+    compatability with Olf. *)
+
+exception UnknownLocation
+
+let finished_constraints () = ()
+let apply_undefined (_ : tau list) = (fresh_var true, 0)
+let assign_undefined (_ : lvalue) = ()
+
+let absloc_epoints_to = tauPointsTo
diff --git a/cil/src/ext/pta/golf.mli b/cil/src/ext/pta/golf.mli
new file mode 100644
index 00000000..569855c5
--- /dev/null
+++ b/cil/src/ext/pta/golf.mli
@@ -0,0 +1,83 @@
+(*
+ *
+ * Copyright (c) 2001-2002,
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+type lvalue
+type tau
+type absloc
+
+(* only for compatability with Olf *)
+exception UnknownLocation
+
+val debug : bool ref
+val debug_constraints : bool ref
+val debug_aliases : bool ref
+val smart_aliases : bool ref
+val finished_constraints : unit -> unit (* only for compatability with Olf *)
+val print_constraints : bool ref
+val no_flow : bool ref
+val no_sub : bool ref
+val analyze_mono : bool ref
+val solve_constraints : unit -> unit
+val rvalue : lvalue -> tau
+val deref : tau -> lvalue
+val join : tau -> tau -> tau
+val join_inits : tau list -> tau
+val address : lvalue -> tau
+val instantiate : lvalue -> int -> lvalue
+val assign : lvalue -> tau -> unit
+val assign_ret : int -> lvalue -> tau -> unit
+val apply : tau -> tau list -> (tau * int)
+val apply_undefined : tau list -> (tau * int) (* only for compatability with Olf *)
+val assign_undefined : lvalue -> unit (* only for compatability with Olf *)
+val make_function :  string -> lvalue list -> tau -> tau
+val make_lvalue : bool -> string -> (Cil.varinfo option) -> lvalue
+val bottom : unit -> tau
+val return : tau -> tau -> unit
+val make_fresh : string -> tau
+val points_to_names : lvalue -> string list
+val points_to : lvalue -> Cil.varinfo list
+val epoints_to : tau -> Cil.varinfo list
+val string_of_lvalue : lvalue -> string
+val global_lvalue : lvalue -> bool
+val alias_query : bool -> lvalue list -> int * int
+val alias_frequency : (lvalue * bool) list -> int * int
+
+val may_alias : tau -> tau -> bool
+
+val absloc_points_to : lvalue -> absloc list
+val absloc_epoints_to : tau -> absloc list
+val absloc_of_lvalue : lvalue -> absloc
+val absloc_eq : (absloc * absloc) -> bool
+val d_absloc : unit -> absloc -> Pretty.doc
+val phonyAddrOf : lvalue -> lvalue
diff --git a/cil/src/ext/pta/olf.ml b/cil/src/ext/pta/olf.ml
new file mode 100644
index 00000000..0d770028
--- /dev/null
+++ b/cil/src/ext/pta/olf.ml
@@ -0,0 +1,1108 @@
+(*
+ *
+ * Copyright (c) 2001-2002,
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(* Exceptions                                                          *)
+(*                                                                     *)
+(***********************************************************************)
+
+exception Inconsistent (* raised if constraint system is inconsistent *)
+exception WellFormed   (* raised if types are not well-formed *)
+exception NoContents
+exception APFound      (* raised if an alias pair is found, a control
+                          flow exception *)
+exception ReachedTop   (* raised if top (from an undefined function)
+                          flows to a c_absloc during the flow step *)
+exception UnknownLocation
+
+let solve_constraints () = () (* only for compatability with Golf *)
+
+open Cil
+
+module U = Uref
+module S = Setp
+module H = Hashtbl
+module Q = Queue
+
+(** Generic bounds *)
+type 'a bound = {info : 'a U.uref}
+
+module Bound =
+struct
+  type 'a t = 'a bound
+  let compare (x : 'a t) (y : 'a t) =
+    Pervasives.compare (U.deref x.info) (U.deref y.info)
+end
+
+module B = S.Make (Bound)
+
+type 'a boundset = 'a B.t
+
+(** Abslocs, which identify elements in points-to sets *)
+(** jk : I'd prefer to make this an 'a absloc and specialize it to
+    varinfo for use with the Cil frontend, but for now, this will do *)
+type absloc = int * string * Cil.varinfo option
+
+module Absloc =
+struct
+  type t = absloc
+  let compare (xid, _, _) (yid, _, _) = xid - yid
+end
+
+module C = Set.Make (Absloc)
+
+(** Sets of abslocs. Set union is used when two c_abslocs containing
+    absloc sets are unified *)
+type abslocset = C.t
+
+let d_absloc () (a: absloc) : Pretty.doc =
+  let i,s,_ = a in
+  Pretty.dprintf "<%d, %s>" i s
+
+type c_abslocinfo = {
+  mutable l_name: string;   (** name of the location *)
+  loc : absloc;
+  l_stamp : int;
+  mutable l_top : bool;
+  mutable aliases : abslocset;
+  mutable lbounds : c_abslocinfo boundset;
+  mutable ubounds : c_abslocinfo boundset;
+  mutable flow_computed : bool
+}
+and c_absloc = c_abslocinfo U.uref
+
+(** The type of lvalues. *)
+type lvalue = {
+  l: c_absloc;
+  contents: tau
+}
+and vinfo = {
+  v_stamp : int;
+  v_name : string;
+  mutable v_top : bool;
+  mutable v_lbounds : tinfo boundset;
+  mutable v_ubounds : tinfo boundset
+}
+and rinfo = {
+  r_stamp : int;
+  rl : c_absloc;
+  points_to : tau
+}
+and finfo = {
+  f_stamp : int;
+  fl : c_absloc;
+  ret : tau;
+  mutable args : tau list
+}
+and pinfo = {
+  p_stamp : int;
+  ptr : tau;
+  lam : tau
+}
+and tinfo =
+    Var of vinfo
+  | Ref of rinfo
+  | Fun of finfo
+  | Pair of pinfo
+and tau = tinfo U.uref
+
+type tconstraint =
+    Unification of tau * tau
+  | Leq of tau * tau
+
+(** Association lists, used for printing recursive types. The first
+    element is a type that has been visited. The second element is the
+    string representation of that type (so far). If the string option is
+    set, then this type occurs within itself, and is associated with the
+    recursive var name stored in the option. When walking a type, add it
+    to an association list.
+
+    Example: suppose we have the constraint 'a = ref('a). The type is
+    unified via cyclic unification, and would loop infinitely if we
+    attempted to print it. What we want to do is print the type u
+    rv. ref(rv). This is accomplished in the following manner:
+
+    -- ref('a) is visited. It is not in the association list, so it is
+    added and the string "ref(" is stored in the second element. We
+    recurse to print the first argument of the constructor.
+
+    -- In the recursive call, we see that 'a (or ref('a)) is already
+    in the association list, so the type is recursive. We check the
+    string option, which is None, meaning that this is the first
+    recurrence of the type. We create a new recursive variable, rv and
+    set the string option to 'rv. Next, we prepend u rv. to the string
+    representation we have seen before, "ref(", and return "rv" as the
+    string representation of this type.
+
+    -- The string so far is "u rv.ref(". The recursive call returns,
+    and we complete the type by printing the result of the call, "rv",
+    and ")"
+
+    In a type where the recursive variable appears twice, e.g. 'a =
+    pair('a,'a), the second time we hit 'a, the string option will be
+    set, so we know to reuse the same recursive variable name.
+*)
+type association = tau * string ref * string option ref
+
+(** The current state of the solver engine either adding more
+    constraints, or finished adding constraints and querying graph *)
+type state =
+    AddingConstraints
+  | FinishedConstraints
+
+(***********************************************************************)
+(*                                                                     *)
+(* Global Variables                                                    *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** A count of the constraints introduced from the AST. Used for
+    debugging. *)
+let toplev_count = ref 0
+
+let solver_state : state ref = ref AddingConstraints
+
+(** Print the instantiations constraints. *)
+let print_constraints : bool ref = ref false
+
+(** If true, print all constraints (including induced) and show
+    additional debug output. *)
+let debug = ref false
+
+(** Just debug all the constraints (including induced) *)
+let debug_constraints = ref false
+
+(** Debug the flow step *)
+let debug_flow_step = ref false
+
+(** Compatibility with GOLF *)
+let debug_aliases = ref false
+let smart_aliases = ref false
+let no_flow = ref false
+let analyze_mono = ref false
+
+(** If true, disable subtyping (unification at all levels) *)
+let no_sub = ref false
+
+(** A list of equality constraints. *)
+let eq_worklist : tconstraint Q.t = Q.create ()
+
+(** A list of leq constraints. *)
+let leq_worklist : tconstraint Q.t = Q.create ()
+
+(** A hashtable containing stamp pairs of c_abslocs that must be aliased. *)
+let cached_aliases : (int * int, unit) H.t = H.create 64
+
+(** A hashtable mapping pairs of tau's to their join node. *)
+let join_cache : (int * int, tau) H.t = H.create 64
+
+(** *)
+let label_prefix = "l_"
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Utility Functions                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+let starts_with s p =
+  let n = String.length p in
+    if String.length s < n then false
+    else String.sub s 0 n = p
+
+
+let die s =
+  Printf.printf "*******\nAssertion failed: %s\n*******\n" s;
+  assert false
+
+let insist b s =
+  if not b then die s else ()
+
+
+let can_add_constraints () =
+  !solver_state = AddingConstraints
+
+let can_query_graph () =
+  !solver_state = FinishedConstraints
+
+let finished_constraints () =
+  insist (!solver_state = AddingConstraints) "inconsistent states";
+  solver_state := FinishedConstraints
+
+let find = U.deref
+
+(** return the prefix of the list up to and including the first
+    element satisfying p. if no element satisfies p, return the empty
+    list *)
+let rec keep_until p l =
+  match l with
+      [] -> []
+    | x :: xs -> if p x then [x] else x :: keep_until p xs
+
+
+(** Generate a unique integer. *)
+let fresh_index : (unit -> int) =
+  let counter = ref 0 in
+    fun () ->
+      incr counter;
+      !counter
+
+let fresh_stamp : (unit -> int) =
+  let stamp = ref 0 in
+    fun () ->
+      incr stamp;
+      !stamp
+
+(** Return a unique integer representation of a tau *)
+let get_stamp (t : tau) : int =
+  match find t with
+      Var v -> v.v_stamp
+    | Ref r -> r.r_stamp
+    | Pair p -> p.p_stamp
+    | Fun f -> f.f_stamp
+
+(** Consistency checks for inferred types *)
+let  pair_or_var (t : tau) =
+  match find t with
+      Pair _ -> true
+    | Var _ -> true
+    | _ -> false
+
+let ref_or_var (t : tau) =
+   match find t with
+       Ref _ -> true
+     | Var _ -> true
+     | _ -> false
+
+let fun_or_var (t : tau) =
+  match find t with
+      Fun _ -> true
+    | Var _ -> true
+    |  _ -> false
+
+
+(** Apply [f] structurally down [t]. Guaranteed to terminate, even if [t]
+    is recursive *)
+let iter_tau f t =
+  let visited : (int, tau) H.t = H.create 4 in
+  let rec iter_tau' t =
+    if H.mem visited (get_stamp t) then () else
+      begin
+        f t;
+        H.add visited (get_stamp t) t;
+        match find t with
+            Pair p ->
+              iter_tau' p.ptr;
+              iter_tau' p.lam
+          | Fun f ->
+              List.iter iter_tau' f.args;
+              iter_tau' f.ret;
+          | Ref r -> iter_tau' r.points_to
+          | _ -> ()
+      end
+  in
+    iter_tau' t
+
+let equal_absloc = function
+    (i, _, _), (i', _, _) -> i = i'
+
+let equal_c_absloc l l' =
+  (find l).l_stamp = (find l').l_stamp
+
+let equal_tau (t : tau) (t' : tau) =
+  get_stamp t = get_stamp t'
+
+let top_c_absloc l =
+  (find l).l_top
+
+let get_flow_computed l =
+  (find l).flow_computed
+
+let set_flow_computed l =
+  (find l).flow_computed <- true
+
+let rec top_tau (t : tau) =
+  match find t with
+      Pair p -> top_tau p.ptr || top_tau p.lam
+    | Ref r -> top_c_absloc r.rl
+    | Fun f -> top_c_absloc f.fl
+    | Var v -> v.v_top
+
+let get_c_absloc_stamp (l : c_absloc) : int =
+  (find l).l_stamp
+
+let set_top_c_absloc (l : c_absloc) (b: bool) : unit =
+  (find l).l_top <- b
+
+let get_aliases (l : c_absloc) =
+  if top_c_absloc l then raise ReachedTop
+  else (find l).aliases
+
+(***********************************************************************)
+(*                                                                     *)
+(* Printing Functions                                                  *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Convert a c_absloc to a string, short representation *)
+let string_of_c_absloc (l : c_absloc) : string =
+  "\"" ^
+    (find l).l_name ^
+    if top_c_absloc l then "(top)" else "" ^
+      "\""
+
+(** Return true if the element [e] is present in the association list,
+    according to uref equality *)
+let rec assoc_list_mem (e : tau) (l : association list) =
+  match l with
+      [] -> None
+    | (h, s, so) :: t ->
+        if U.equal (h, e) then Some (s, so)
+        else assoc_list_mem e t
+
+(** Given a tau, create a unique recursive variable name. This should
+    always return the same name for a given tau *)
+let fresh_recvar_name (t : tau) : string =
+  match find t with
+      Pair p -> "rvp" ^ string_of_int p.p_stamp
+    | Ref r -> "rvr" ^ string_of_int r.r_stamp
+    | Fun f -> "rvf" ^ string_of_int f.f_stamp
+    | _ -> die "fresh_recvar_name"
+
+
+(** Return a string representation of a tau, using association lists. *)
+let string_of_tau (t : tau) : string =
+  let tau_map : association list ref = ref [] in
+  let rec string_of_tau' t =
+    match assoc_list_mem t !tau_map with
+        Some (s, so) -> (* recursive type. see if a var name has been set *)
+          begin
+            match !so with
+                None ->
+                  let rv = fresh_recvar_name t in
+                    s := "u " ^ rv ^ "." ^ !s;
+                    so := Some rv;
+                    rv
+              | Some rv -> rv
+          end
+      | None -> (* type's not recursive. Add it to the assoc list and cont. *)
+          let s = ref ""
+          and so : string option ref = ref None in
+            tau_map := (t, s, so) :: !tau_map;
+            begin
+              match find t with
+                  Var v -> s := v.v_name
+                | Pair p ->
+                    insist (ref_or_var p.ptr) "wellformed";
+                    insist (fun_or_var p.lam) "wellformed";
+                    s := "{";
+                    s := !s ^ string_of_tau' p.ptr;
+                    s := !s ^ ",";
+                    s := !s ^ string_of_tau' p.lam;
+                    s := !s ^ "}"
+                | Ref r ->
+                    insist (pair_or_var r.points_to) "wellformed";
+                    s := "ref(|";
+                    s := !s ^ string_of_c_absloc r.rl;
+                    s := !s ^ "|,";
+                    s := !s ^ string_of_tau' r.points_to;
+                    s := !s ^ ")"
+                | Fun f ->
+                    let rec string_of_args = function
+                        [] -> ()
+                      | h :: [] ->
+                          insist (pair_or_var h) "wellformed";
+                          s := !s ^ string_of_tau' h
+                      | h :: t ->
+                          insist (pair_or_var h) "wellformed";
+                          s := !s ^ string_of_tau' h ^ ",";
+                          string_of_args t
+                    in
+                      insist (pair_or_var f.ret) "wellformed";
+                      s := "fun(|";
+                      s := !s ^ string_of_c_absloc f.fl;
+                      s := !s ^ "|,";
+                      s := !s ^ "<";
+                      if List.length f.args > 0 then string_of_args f.args
+                      else s := !s ^ "void";
+                      s := !s ^ ">,";
+                      s := !s ^ string_of_tau' f.ret;
+                      s := !s ^ ")"
+            end;
+            tau_map := List.tl !tau_map;
+            !s
+  in
+    string_of_tau' t
+
+(** Convert an lvalue to a string *)
+let rec string_of_lvalue (lv : lvalue) : string =
+  let contents = string_of_tau lv.contents
+  and l = string_of_c_absloc lv.l
+  in
+    insist (pair_or_var lv.contents) "inconsistency at string_of_lvalue";
+    (* do a consistency check *)
+    Printf.sprintf "[%s]^(%s)" contents l
+
+(** Print a list of tau elements, comma separated *)
+let rec print_tau_list (l : tau list) : unit =
+  let rec print_t_strings = function
+      [] -> ()
+    | h :: [] -> print_endline h
+    | h :: t ->
+        print_string h;
+        print_string ", ";
+        print_t_strings t
+  in
+    print_t_strings (List.map string_of_tau l)
+
+let print_constraint (c : tconstraint) =
+  match c with
+      Unification (t, t') ->
+        let lhs = string_of_tau t in
+        let rhs = string_of_tau t' in
+          Printf.printf "%s == %s\n" lhs rhs
+    | Leq (t, t') ->
+        let lhs = string_of_tau t in
+        let rhs = string_of_tau t' in
+          Printf.printf "%s <= %s\n" lhs  rhs
+
+(***********************************************************************)
+(*                                                                     *)
+(* Type Operations -- these do not create any constraints              *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Create an lvalue with c_absloc [lbl] and tau contents [t]. *)
+let make_lval (loc, t : c_absloc * tau) : lvalue =
+  {l = loc; contents = t}
+
+let make_c_absloc_int (is_top : bool) (name : string) (vio : Cil.varinfo option) : c_absloc =
+  let my_absloc = (fresh_index (), name, vio) in
+  let locc = C.add my_absloc C.empty
+  in
+    U.uref {
+      l_name = name;
+      l_top = is_top;
+      l_stamp = fresh_stamp ();
+      loc = my_absloc;
+      aliases = locc;
+      ubounds = B.empty;
+      lbounds = B.empty;
+      flow_computed = false
+    }
+
+(** Create a new c_absloc with name [name]. Also adds a fresh absloc
+    with name [name] to this c_absloc's aliases set. *)
+let make_c_absloc (is_top : bool) (name : string) (vio : Cil.varinfo option) =
+  make_c_absloc_int is_top name vio
+
+let fresh_c_absloc (is_top : bool) : c_absloc =
+  let index = fresh_index () in
+    make_c_absloc_int is_top (label_prefix ^ string_of_int index) None
+
+(** Create a fresh bound (edge in the constraint graph). *)
+let make_bound (a : c_absloc) : c_abslocinfo bound =
+  {info = a}
+
+let make_tau_bound (t : tau) : tinfo bound =
+  {info = t}
+
+(** Create a fresh named variable with name '[name]. *)
+let make_var (is_top : bool) (name : string) : tau =
+  U.uref (Var {v_name = ("'" ^ name);
+               v_top = is_top;
+               v_stamp = fresh_index ();
+               v_lbounds = B.empty;
+               v_ubounds = B.empty})
+
+let fresh_var  (is_top : bool) : tau =
+  make_var is_top ("fi" ^ string_of_int (fresh_index ()))
+
+(** Create a fresh unnamed variable (name will be 'fi). *)
+let fresh_var_i (is_top : bool) : tau =
+  make_var is_top ("fi" ^ string_of_int (fresh_index ()))
+
+(** Create a Fun constructor. *)
+let make_fun (lbl, a, r : c_absloc * (tau list) * tau) : tau =
+  U.uref (Fun {fl = lbl;
+               f_stamp = fresh_index ();
+               args = a;
+               ret = r})
+
+(** Create a Ref constructor. *)
+let make_ref (lbl, pt : c_absloc * tau) : tau =
+  U.uref (Ref {rl = lbl;
+               r_stamp = fresh_index ();
+               points_to = pt})
+
+(** Create a Pair constructor. *)
+let make_pair (p, f : tau * tau) : tau =
+  U.uref (Pair {ptr = p;
+                p_stamp = fresh_index ();
+                lam = f})
+
+(** Copy the toplevel constructor of [t], putting fresh variables in each
+    argement of the constructor. *)
+let copy_toplevel (t : tau) : tau =
+  match find t with
+      Pair _ -> make_pair (fresh_var_i false, fresh_var_i false)
+    | Ref  _ -> make_ref (fresh_c_absloc false, fresh_var_i false)
+    | Fun f ->
+        make_fun (fresh_c_absloc false,
+                  List.map (fun _ -> fresh_var_i false) f.args,
+                  fresh_var_i false)
+    | _ -> die "copy_toplevel"
+
+let has_same_structure (t : tau) (t' : tau) =
+  match find t, find t' with
+      Pair _, Pair _ -> true
+    | Ref _, Ref _ -> true
+    | Fun _, Fun _ -> true
+    | Var _, Var _ -> true
+    | _ -> false
+
+let pad_args (fi, tlr : finfo * tau list ref) : unit =
+  let padding = List.length fi.args - List.length !tlr
+  in
+    if padding == 0 then ()
+    else
+      if padding > 0 then
+        for i = 1 to padding do
+          tlr := !tlr @ [fresh_var false]
+        done
+      else
+        for i = 1 to -padding do
+          fi.args <- fi.args @ [fresh_var false]
+        done
+
+(***********************************************************************)
+(*                                                                     *)
+(* Constraint Generation/ Resolution                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+let set_top (b : bool) (t : tau) : unit =
+  let set_top_down t =
+    match find t with
+        Var v -> v.v_top <- b
+      | Ref r -> set_top_c_absloc r.rl b
+      | Fun f -> set_top_c_absloc f.fl b
+      | Pair p -> ()
+  in
+    iter_tau set_top_down t
+
+let rec unify_int (t, t' : tau * tau) : unit =
+  if equal_tau t t' then ()
+  else
+    let ti, ti' = find t, find t' in
+      U.unify combine (t, t');
+      match ti, ti' with
+          Var v, Var v' ->
+            set_top (v.v_top || v'.v_top) t';
+            merge_v_lbounds (v, v');
+            merge_v_ubounds (v, v')
+        | Var v, _ ->
+            set_top (v.v_top || top_tau t') t';
+            notify_vlbounds t v;
+            notify_vubounds t v
+        | _, Var v ->
+            set_top (v.v_top || top_tau t) t;
+            notify_vlbounds t' v;
+            notify_vubounds t' v
+        | Ref r, Ref r' -> unify_ref (r, r')
+        | Fun f, Fun f' -> unify_fun (f, f')
+        | Pair p, Pair p' -> unify_pair (p, p')
+        | _ -> raise Inconsistent
+and notify_vlbounds (t : tau) (vi : vinfo) : unit =
+  let notify bounds =
+    List.iter
+      (fun b ->
+         add_constraint (Unification (b.info, copy_toplevel t));
+         add_constraint (Leq (b.info, t)))
+      bounds
+  in
+    notify (B.elements vi.v_lbounds)
+and notify_vubounds (t : tau) (vi : vinfo) : unit =
+  let notify bounds =
+    List.iter
+      (fun b ->
+         add_constraint (Unification (b.info, copy_toplevel t));
+         add_constraint (Leq (t, b.info)))
+      bounds
+  in
+    notify (B.elements vi.v_ubounds)
+and unify_ref (ri, ri' : rinfo * rinfo) : unit =
+  unify_c_abslocs (ri.rl, ri'.rl);
+  add_constraint (Unification (ri.points_to, ri'.points_to))
+and unify_fun (fi, fi' : finfo * finfo) : unit =
+  let rec union_args  = function
+      _, [] -> false
+    | [], _ -> true
+    | h :: t, h' :: t' ->
+        add_constraint (Unification (h, h'));
+        union_args(t, t')
+  in
+    unify_c_abslocs (fi.fl, fi'.fl);
+    add_constraint (Unification (fi.ret, fi'.ret));
+    if union_args (fi.args, fi'.args) then fi.args <- fi'.args
+and unify_pair (pi, pi' : pinfo * pinfo) : unit =
+  add_constraint (Unification (pi.ptr, pi'.ptr));
+  add_constraint (Unification (pi.lam, pi'.lam))
+and unify_c_abslocs (l, l' : c_absloc * c_absloc) : unit =
+  let pick_name (li, li' : c_abslocinfo * c_abslocinfo) =
+    if starts_with li.l_name label_prefix then li.l_name <- li'.l_name
+    else () in
+  let combine_c_absloc (li, li' : c_abslocinfo * c_abslocinfo) : c_abslocinfo =
+    pick_name (li, li');
+    li.l_top <- li.l_top || li'.l_top;
+    li.aliases <- C.union li.aliases li'.aliases;
+    li.ubounds <- B.union li.ubounds li'.ubounds;
+    li.lbounds <- B.union li.lbounds li'.lbounds;
+    li
+  in
+    if !debug_constraints then
+      Printf.printf
+        "%s == %s\n"
+        (string_of_c_absloc l)
+        (string_of_c_absloc l');
+    U.unify combine_c_absloc (l, l')
+and merge_v_lbounds (vi, vi' : vinfo * vinfo) : unit =
+  vi'.v_lbounds <- B.union vi.v_lbounds vi'.v_lbounds;
+and merge_v_ubounds (vi, vi' : vinfo * vinfo) : unit =
+  vi'.v_ubounds <- B.union vi.v_ubounds vi'.v_ubounds;
+(** Pick the representative info for two tinfo's. This function
+    prefers the first argument when both arguments are the same
+    structure, but when one type is a structure and the other is a
+    var, it picks the structure.  All other actions (e.g., updating
+    the info) is done in unify_int *)
+and combine (ti, ti' : tinfo * tinfo) : tinfo =
+  match ti, ti' with
+      Var _, _ -> ti'
+    | _, _ -> ti
+and leq_int (t, t') : unit =
+  if equal_tau t t' then ()
+  else
+    let ti, ti' = find t, find t' in
+      match ti, ti' with
+          Var v, Var v' ->
+            v.v_ubounds <- B.add (make_tau_bound t') v.v_ubounds;
+            v'.v_lbounds <- B.add (make_tau_bound t) v'.v_lbounds
+        | Var v, _ ->
+            add_constraint (Unification (t, copy_toplevel t'));
+            add_constraint (Leq (t, t'))
+        | _, Var v ->
+            add_constraint (Unification (t', copy_toplevel t));
+            add_constraint (Leq (t, t'))
+        | Ref r, Ref r' -> leq_ref (r, r')
+        | Fun f, Fun f' ->
+            (* TODO: check, why not do subtyping here? *)
+            add_constraint (Unification (t, t'))
+        | Pair pr, Pair pr' ->
+            add_constraint (Leq (pr.ptr, pr'.ptr));
+            add_constraint (Leq (pr.lam, pr'.lam))
+        | _ -> raise Inconsistent
+and leq_ref (ri, ri') : unit =
+  leq_c_absloc (ri.rl, ri'.rl);
+  add_constraint (Unification (ri.points_to, ri'.points_to))
+and leq_c_absloc (l, l') : unit =
+  let li, li' = find l, find l' in
+    if !debug_constraints then
+      Printf.printf
+        "%s <= %s\n"
+        (string_of_c_absloc l)
+        (string_of_c_absloc l');
+    if U.equal (l, l') then ()
+    else
+      begin
+        li.ubounds <- B.add (make_bound l') li.ubounds;
+        li'.lbounds <- B.add (make_bound l) li'.lbounds
+      end
+and add_constraint_int (c : tconstraint) (toplev : bool) =
+  if !debug_constraints && toplev then
+    begin
+      Printf.printf "%d:>" !toplev_count;
+      print_constraint c;
+      incr toplev_count
+    end
+  else
+    if !debug_constraints then print_constraint c else ();
+  insist (can_add_constraints ()) 
+    "can't add constraints after compute_results is called";
+  begin
+    match c with
+        Unification _ -> Q.add c eq_worklist
+      | Leq _ -> Q.add c leq_worklist
+  end;
+  solve_constraints () (* solve online *)
+and add_constraint (c : tconstraint) =
+  add_constraint_int c false
+and add_toplev_constraint (c : tconstraint) =
+  if !print_constraints && not !debug_constraints then
+    begin
+      Printf.printf "%d:>" !toplev_count;
+      incr toplev_count;
+      print_constraint c
+    end
+  else ();
+  add_constraint_int c true
+and fetch_constraint () : tconstraint option =
+  try Some (Q.take eq_worklist)
+  with Q.Empty ->
+    begin
+      try Some (Q.take leq_worklist)
+      with Q.Empty -> None
+    end
+(** The main solver loop. *)
+and solve_constraints () : unit =
+  match fetch_constraint () with
+      None -> ()
+    | Some c ->
+        begin
+          match c with
+              Unification (t, t') -> unify_int (t, t')
+            | Leq (t, t') ->
+                if !no_sub then unify_int (t, t')
+                else leq_int (t, t')
+        end;
+        solve_constraints ()
+
+(***********************************************************************)
+(*                                                                     *)
+(* Interface Functions                                                 *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Return the contents of the lvalue. *)
+let rvalue (lv : lvalue) : tau =
+  lv.contents
+
+(** Dereference the rvalue. If it does not have enough structure to
+    support the operation, then the correct structure is added via new
+    unification constraints. *)
+let rec deref (t : tau) : lvalue =
+  match find t with
+      Pair p ->
+        begin
+          match find p.ptr with
+            | Var _ ->
+                let is_top = top_tau p.ptr in
+                let points_to = fresh_var is_top in
+                let l = fresh_c_absloc is_top in
+                let r = make_ref (l, points_to)
+                in
+                  add_toplev_constraint (Unification (p.ptr, r));
+                  make_lval (l, points_to)
+            | Ref r -> make_lval (r.rl, r.points_to)
+            | _ -> raise WellFormed
+        end
+    | Var v ->
+        let is_top = top_tau t in
+          add_toplev_constraint
+            (Unification (t, make_pair (fresh_var is_top, fresh_var is_top)));
+          deref t
+    | _ -> raise WellFormed
+
+
+(** Form the union of [t] and [t'], if it doesn't exist already. *)
+let join (t : tau) (t' : tau) : tau =
+  let s, s' = get_stamp t, get_stamp t' in
+    try H.find join_cache (s, s')
+    with Not_found ->
+      let t'' = fresh_var false in
+        add_toplev_constraint (Leq (t, t''));
+        add_toplev_constraint (Leq (t', t''));
+        H.add join_cache (s, s') t'';
+        t''
+
+(** Form the union of a list [tl], expected to be the initializers of some
+  structure or array type. *)
+let join_inits (tl : tau list) : tau =
+  let t' = fresh_var false in
+    List.iter (function t -> add_toplev_constraint (Leq (t, t'))) tl;
+    t'
+
+(** Take the address of an lvalue. Does not add constraints. *)
+let address (lv  : lvalue) : tau =
+  make_pair (make_ref (lv.l, lv.contents), fresh_var false )
+
+(** No instantiation in this analysis *)
+let instantiate (lv : lvalue) (i : int) : lvalue =
+  lv
+
+(** Constraint generated from assigning [t] to [lv]. *)
+let assign (lv : lvalue) (t : tau) : unit =
+  add_toplev_constraint (Leq (t, lv.contents))
+
+let assign_ret (i : int) (lv : lvalue) (t : tau) : unit =
+  add_toplev_constraint (Leq (t, lv.contents))
+
+(** Project out the first (ref) component or a pair. If the argument
+    [t] has no discovered structure, raise NoContents. *)
+let proj_ref (t : tau) : tau =
+  match find t with
+      Pair p -> p.ptr
+    | Var v -> raise NoContents
+    | _ ->  raise WellFormed
+
+(* Project out the second (fun) component of a pair. If the argument
+   [t] has no discovered structure, create it on the fly by adding
+   constraints. *)
+let proj_fun (t : tau) : tau =
+  match find t with
+      Pair p -> p.lam
+    | Var v ->
+        let p, f = fresh_var false, fresh_var false in
+          add_toplev_constraint (Unification (t, make_pair (p, f)));
+          f
+    | _ -> raise WellFormed
+
+let get_args (t : tau) : tau list =
+  match find t with
+      Fun f -> f.args
+    | _ -> raise WellFormed
+
+let get_finfo (t : tau) : finfo =
+  match find t with
+      Fun f -> f
+    | _ -> raise WellFormed
+
+(** Function type [t] is applied to the arguments [actuals]. Unifies
+    the actuals with the formals of [t]. If no functions have been
+    discovered for [t] yet, create a fresh one and unify it with
+    t. The result is the return value of the function plus the index
+    of this application site.
+
+    For this analysis, the application site is always 0 *)
+let apply (t : tau) (al : tau list) : (tau * int) =
+  let f = proj_fun t in
+  let actuals = ref al in
+  let fi, ret =
+    match find f with
+        Fun fi -> fi, fi.ret
+      | Var v ->
+          let new_l, new_ret, new_args =
+            fresh_c_absloc false,
+            fresh_var false,
+            List.map (function _ -> fresh_var false) !actuals
+          in
+          let new_fun = make_fun (new_l, new_args, new_ret) in
+            add_toplev_constraint (Unification (new_fun, f));
+            (get_finfo new_fun, new_ret)
+      | _ -> raise WellFormed
+  in
+    pad_args (fi, actuals);
+    List.iter2
+      (fun actual -> fun formal ->
+         add_toplev_constraint (Leq (actual, formal)))
+      !actuals fi.args;
+    (ret, 0)
+
+let make_undefined_lvalue () =
+  make_lval (make_c_absloc false "undefined" None,
+             make_var true "undefined")
+
+let make_undefined_rvalue () =
+  make_var true "undefined"
+
+let assign_undefined (lv : lvalue) : unit =
+  assign lv (make_undefined_rvalue ())
+
+let apply_undefined (al : tau list) : (tau * int) =
+    List.iter
+      (fun actual ->  assign (make_undefined_lvalue ()) actual)
+      al;
+   (fresh_var true, 0)
+
+(** Create a new function type with name [name], list of formal
+    arguments [formals], and return value [ret]. Adds no constraints. *)
+let make_function (name : string) (formals : lvalue list) (ret : tau) : tau =
+  let f = make_fun (make_c_absloc false name None,
+                    List.map (fun x -> rvalue x) formals,
+                    ret)
+  in
+    make_pair (fresh_var false, f)
+
+(** Create an lvalue. *)
+let make_lvalue (b : bool ) (name : string) (vio : Cil.varinfo option) =
+  make_lval (make_c_absloc false name vio,
+             make_var false name)
+
+(** Create a fresh named variable. *)
+let make_fresh (name : string) : tau =
+  make_var false name
+
+(** The default type for abslocs. *)
+let bottom () : tau =
+  make_var false "bottom"
+
+(** Unify the result of a function with its return value. *)
+let return (t : tau) (t' : tau) =
+  add_toplev_constraint (Leq (t', t))
+
+(***********************************************************************)
+(*                                                                     *)
+(* Query/Extract Solutions                                             *)
+(*                                                                     *)
+(***********************************************************************)
+
+module IntHash = Hashtbl.Make (struct
+                                 type t = int
+                                 let equal x y = x = y
+                                 let hash x = x
+                               end)
+
+(** todo : reached_top !! *)
+let collect_ptset_fast (l : c_absloc) : abslocset =
+  let onpath : unit IntHash.t = IntHash.create 101 in
+  let path : c_absloc list ref = ref [] in
+  let compute_path (i : int) =
+    keep_until (fun l -> i = get_c_absloc_stamp l) !path in
+  let collapse_cycle (cycle : c_absloc list) =
+    match cycle with
+        l :: ls ->
+          List.iter (fun l' -> unify_c_abslocs (l, l')) ls;
+          C.empty
+      | [] -> die "collapse cycle" in
+  let rec flow_step (l : c_absloc) : abslocset =
+    let stamp = get_c_absloc_stamp l in
+      if IntHash.mem onpath stamp then (* already seen *)
+        collapse_cycle (compute_path stamp)
+      else
+        let li = find l in
+          IntHash.add onpath stamp ();
+          path := l :: !path;
+          B.iter
+            (fun lb -> li.aliases <- C.union li.aliases (flow_step lb.info))
+            li.lbounds;
+          path := List.tl !path;
+          IntHash.remove onpath stamp;
+          li.aliases
+  in
+    insist (can_query_graph ()) "collect_ptset_fast can't query graph";
+    if get_flow_computed l then get_aliases l
+    else
+      begin
+        set_flow_computed l;
+        flow_step l
+      end
+
+(** this is a quadratic flow step. keep it for debugging the fast
+    version above. *)
+let collect_ptset_slow (l : c_absloc) : abslocset =
+  let onpath : unit IntHash.t = IntHash.create 101 in
+  let rec flow_step (l : c_absloc) : abslocset =
+    if top_c_absloc l then raise ReachedTop
+    else
+      let stamp = get_c_absloc_stamp l in
+        if IntHash.mem onpath stamp then C.empty
+        else
+          let li = find l in
+            IntHash.add onpath stamp ();
+            B.iter
+              (fun lb -> li.aliases <- C.union li.aliases (flow_step lb.info))
+              li.lbounds;
+            li.aliases
+  in
+    insist (can_query_graph ()) "collect_ptset_slow can't query graph";
+    if get_flow_computed l then get_aliases l
+    else
+      begin
+        set_flow_computed l;
+        flow_step l
+      end
+
+let collect_ptset =
+  collect_ptset_slow
+  (* if !debug_flow_step then collect_ptset_slow
+     else collect_ptset_fast *)
+
+let may_alias (t1 : tau) (t2 : tau) : bool =
+  let get_l (t : tau) : c_absloc =
+    match find (proj_ref t) with
+        Ref r -> r.rl
+      | Var v -> raise NoContents
+      | _ ->  raise WellFormed
+  in
+    try
+      let l1 = get_l t1
+      and l2 = get_l t2 in
+        equal_c_absloc l1 l2 ||
+          not (C.is_empty (C.inter (collect_ptset l1) (collect_ptset l2)))
+    with
+        NoContents -> false
+      | ReachedTop -> raise UnknownLocation
+
+let points_to_aux (t : tau) : absloc list =
+  try
+    match find (proj_ref t) with
+        Var v -> []
+      | Ref r -> C.elements (collect_ptset r.rl)
+      | _ -> raise WellFormed
+  with
+      NoContents -> []
+    | ReachedTop -> raise UnknownLocation
+
+let points_to (lv : lvalue) : Cil.varinfo list =
+  let rec get_vinfos l : Cil.varinfo list =
+    match l with
+        [] -> []
+      | (_, _, Some h) :: t -> h :: get_vinfos t
+      | (_, _, None) :: t -> get_vinfos t
+  in
+    get_vinfos (points_to_aux lv.contents)
+
+let epoints_to (t : tau) : Cil.varinfo list =
+  let rec get_vinfos l : Cil.varinfo list = match l with
+      [] -> []
+    | (_, _, Some h) :: t -> h :: get_vinfos t
+    | (_, _, None) :: t -> get_vinfos t
+  in
+    get_vinfos (points_to_aux t)
+
+let points_to_names (lv : lvalue) : string list =
+  List.map (fun v -> v.vname) (points_to lv)
+
+let absloc_points_to (lv : lvalue) : absloc list =
+  points_to_aux lv.contents
+
+let absloc_epoints_to (t : tau) : absloc list =
+  points_to_aux t
+
+let absloc_of_lvalue (lv : lvalue) : absloc =
+  (find lv.l).loc
+
+let absloc_eq = equal_absloc
diff --git a/cil/src/ext/pta/olf.mli b/cil/src/ext/pta/olf.mli
new file mode 100644
index 00000000..43794825
--- /dev/null
+++ b/cil/src/ext/pta/olf.mli
@@ -0,0 +1,80 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+type lvalue
+type tau
+type absloc
+
+(** Raised if a pointer flows to an undefined function.
+  We assume that such a function can have any effect on the pointer's contents
+*)
+exception UnknownLocation
+
+val debug : bool ref
+val debug_constraints : bool ref
+val debug_aliases : bool ref
+val smart_aliases : bool ref
+val finished_constraints : unit -> unit
+val print_constraints : bool ref
+val no_flow : bool ref
+val no_sub : bool ref
+val analyze_mono : bool ref
+val solve_constraints : unit -> unit (* only for compatability with Golf *)
+val rvalue : lvalue -> tau
+val deref : tau -> lvalue
+val join : tau -> tau -> tau
+val join_inits : tau list -> tau
+val address : lvalue -> tau
+val instantiate : lvalue -> int -> lvalue
+val assign : lvalue -> tau -> unit
+val assign_ret : int -> lvalue -> tau -> unit
+val apply : tau -> tau list -> (tau * int)
+val apply_undefined : tau list -> (tau * int)
+val assign_undefined : lvalue -> unit
+val make_function :  string -> lvalue list -> tau -> tau
+val make_lvalue : bool -> string -> (Cil.varinfo option) -> lvalue
+val bottom : unit -> tau
+val return : tau -> tau -> unit
+val make_fresh : string -> tau
+val points_to_names : lvalue -> string list
+val points_to : lvalue -> Cil.varinfo list
+val epoints_to : tau -> Cil.varinfo list   
+val string_of_lvalue : lvalue -> string
+val may_alias : tau -> tau -> bool
+
+val absloc_points_to : lvalue -> absloc list
+val absloc_epoints_to : tau -> absloc list
+val absloc_of_lvalue : lvalue -> absloc 
+val absloc_eq : (absloc * absloc) -> bool
+val d_absloc : unit -> absloc -> Pretty.doc
diff --git a/cil/src/ext/pta/ptranal.ml b/cil/src/ext/pta/ptranal.ml
new file mode 100644
index 00000000..c91bda81
--- /dev/null
+++ b/cil/src/ext/pta/ptranal.ml
@@ -0,0 +1,597 @@
+(* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
+
+(*
+ *
+ * Copyright (c) 2001-2002,
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+exception Bad_return
+exception Bad_function
+
+
+open Cil
+
+module H = Hashtbl
+
+module A = Olf
+exception UnknownLocation = A.UnknownLocation
+
+type access = A.lvalue * bool
+
+type access_map = (lval, access) H.t
+
+(** a mapping from varinfo's back to fundecs *)
+module VarInfoKey =
+struct
+  type t = varinfo
+  let compare v1 v2 = v1.vid - v2.vid
+end
+
+module F = Map.Make (VarInfoKey)
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Global Variables                                                    *)
+(*                                                                     *)
+(***********************************************************************)
+
+let model_strings = ref false
+let print_constraints = A.print_constraints
+let debug_constraints = A.debug_constraints
+let debug_aliases = A.debug_aliases
+let smart_aliases = A.smart_aliases
+let debug = A.debug
+let analyze_mono = A.analyze_mono
+let no_flow = A.no_flow
+let no_sub = A.no_sub
+let fun_ptrs_as_funs = ref false
+let show_progress = ref false
+let debug_may_aliases = ref false
+
+let found_undefined = ref false
+
+let conservative_undefineds = ref false
+
+let current_fundec : fundec option ref = ref None
+
+let fun_access_map : (fundec, access_map) H.t = H.create 64
+
+(* A mapping from varinfos to fundecs *)
+let fun_varinfo_map = ref F.empty
+
+let current_ret : A.tau option ref = ref None
+
+let lvalue_hash : (varinfo,A.lvalue) H.t = H.create 64
+
+let expressions : (exp,A.tau) H.t = H.create 64
+
+let lvalues : (lval,A.lvalue) H.t = H.create 64
+
+let fresh_index : (unit -> int) =
+  let count = ref 0 in
+    fun () ->
+      incr count;
+      !count
+
+let alloc_names = [
+  "malloc";
+  "calloc";
+  "realloc";
+  "xmalloc";
+  "__builtin_alloca";
+  "alloca";
+  "kmalloc"
+]
+
+let all_globals : varinfo list ref = ref []
+let all_functions : fundec list ref = ref []
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Utility Functions                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+let is_undefined_fun = function
+    Lval (lh, o) ->
+      if isFunctionType (typeOfLval (lh, o))  then
+        match lh with
+            Var v -> v.vstorage = Extern
+          | _ -> false
+      else false
+  | _ -> false
+
+let is_alloc_fun = function
+    Lval (lh, o) ->
+      if isFunctionType (typeOfLval (lh, o)) then
+        match lh with
+            Var v -> List.mem v.vname alloc_names
+          | _ -> false
+      else false
+  | _ -> false
+
+let next_alloc = function
+    Lval (Var v, o) ->
+      let name = Printf.sprintf "%s@%d" v.vname (fresh_index ())
+      in
+        A.address (A.make_lvalue false name (Some v)) (* check *)
+  | _ -> raise Bad_return
+
+let is_effect_free_fun = function
+    Lval (lh, o) when isFunctionType (typeOfLval (lh, o)) ->
+      begin
+        match lh with
+            Var v ->
+              begin
+                try ("CHECK_" = String.sub v.vname 0 6)
+                with Invalid_argument _ -> false
+              end
+          | _ -> false
+      end
+  | _ -> false
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* AST Traversal Functions                                             *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* should do nothing, might need to worry about Index case *)
+(* let analyzeOffset (o : offset ) : A.tau = A.bottom () *)
+
+let analyze_var_decl (v : varinfo ) : A.lvalue =
+  try H.find lvalue_hash v
+  with Not_found ->
+    let lv = A.make_lvalue false v.vname (Some v)
+    in
+      H.add lvalue_hash v lv;
+      lv
+
+let isFunPtrType (t : typ) : bool =
+  match t with
+      TPtr (t, _) -> isFunctionType t
+    | _ -> false
+
+let rec analyze_lval (lv : lval ) : A.lvalue =
+  let find_access (l : A.lvalue) (is_var : bool) : A.lvalue =
+    match !current_fundec with
+        None -> l
+      | Some f ->
+          let accesses = H.find fun_access_map f in
+            if H.mem accesses lv then l
+            else
+              begin
+                H.add accesses lv (l, is_var);
+                l
+              end in
+  let result =
+    match lv with
+        Var v, _ -> (* instantiate every syntactic occurrence of a function *)
+          let alv =
+            if isFunctionType (typeOfLval lv) then
+              A.instantiate (analyze_var_decl v) (fresh_index ())
+            else analyze_var_decl v
+          in
+            find_access alv true
+      | Mem e, _ ->
+          (* assert (not (isFunctionType(typeOf(e))) ); *)
+          let alv =
+            if !fun_ptrs_as_funs && isFunPtrType (typeOf e) then
+              analyze_expr_as_lval e
+            else A.deref (analyze_expr e)
+          in
+            find_access alv false
+  in
+    H.replace lvalues lv result;
+    result
+and analyze_expr_as_lval (e : exp) : A.lvalue =
+  match e with
+      Lval l ->  analyze_lval l
+    | _ -> assert false (* todo -- other kinds of expressions? *)
+and analyze_expr (e : exp ) : A.tau =
+  let result =
+    match e with
+        Const (CStr s) ->
+          if !model_strings then
+            A.address (A.make_lvalue
+                         false
+                         s
+                         (Some (makeVarinfo false s charConstPtrType)))
+          else A.bottom ()
+      | Const c -> A.bottom ()
+      | Lval l -> A.rvalue (analyze_lval l)
+      | SizeOf _ -> A.bottom ()
+      | SizeOfStr _ -> A.bottom ()
+      | AlignOf _ -> A.bottom ()
+      | UnOp (op, e, t) -> analyze_expr e
+      | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e')
+      | CastE (t, e) -> analyze_expr e
+      | AddrOf l ->
+          if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then
+            A.rvalue (analyze_lval l)
+          else A.address (analyze_lval l)
+      | StartOf l -> A.address (analyze_lval l)
+      | AlignOfE _ -> A.bottom ()
+      | SizeOfE _ -> A.bottom ()
+ in
+  H.add expressions e result;
+  result
+
+
+(* check *)
+let rec analyze_init (i : init ) : A.tau =
+  match i with
+      SingleInit e -> analyze_expr e
+    | CompoundInit (t, oi) ->
+        A.join_inits (List.map (function (_, i) -> analyze_init i) oi)
+
+let analyze_instr (i : instr ) : unit =
+  match i with
+      Set (lval, rhs, l) ->
+        A.assign (analyze_lval lval) (analyze_expr rhs)
+    | Call (res, fexpr, actuals, l) ->
+        if not (isFunctionType (typeOf fexpr)) then
+          () (* todo : is this a varargs? *)
+        else if is_alloc_fun fexpr then
+          begin
+            if !debug then print_string "Found allocation function...\n";
+            match res with
+                Some r -> A.assign (analyze_lval r) (next_alloc fexpr)
+              | None -> ()
+          end
+        else if is_effect_free_fun fexpr then
+          List.iter (fun e -> ignore (analyze_expr e)) actuals
+        else (* todo : check to see if the thing is an undefined function *)
+          let fnres, site =
+            if is_undefined_fun fexpr & !conservative_undefineds then
+              A.apply_undefined (List.map analyze_expr actuals)
+            else
+              A.apply (analyze_expr fexpr) (List.map analyze_expr actuals)
+          in
+            begin
+              match res with
+                  Some r ->
+                    begin
+                      A.assign_ret site (analyze_lval r) fnres;
+                      found_undefined := true;
+                    end
+                | None -> ()
+            end
+    | Asm _ -> ()
+
+let rec analyze_stmt (s : stmt ) : unit =
+  match s.skind with
+      Instr il -> List.iter analyze_instr il
+    | Return (eo, l) ->
+        begin
+          match eo with
+              Some e ->
+                begin
+                  match !current_ret with
+                      Some ret -> A.return ret (analyze_expr e)
+                    | None -> raise Bad_return
+                end
+            | None -> ()
+        end
+    | Goto (s', l) -> () (* analyze_stmt(!s') *)
+    | If (e, b, b', l) ->
+        (* ignore the expression e; expressions can't be side-effecting *)
+        analyze_block b;
+        analyze_block b'
+    | Switch (e, b, sl, l) ->
+        analyze_block b;
+        List.iter analyze_stmt sl
+(*
+    | Loop (b, l, _, _) -> analyze_block b
+*)
+    | While (_, b, _) -> analyze_block b
+    | DoWhile (_, b, _) -> analyze_block b
+    | For (bInit, _, bIter, b, _) ->
+	analyze_block bInit;
+	analyze_block bIter;
+	analyze_block b
+    | Block b -> analyze_block b
+    | TryFinally (b, h, _) ->
+        analyze_block b;
+        analyze_block h
+    | TryExcept (b, (il, _), h, _) ->
+        analyze_block b;
+        List.iter analyze_instr il;
+        analyze_block h
+    | Break l -> ()
+    | Continue l -> ()
+
+
+and analyze_block (b : block ) : unit =
+  List.iter analyze_stmt b.bstmts
+
+let analyze_function (f : fundec ) : unit =
+  let oldlv = analyze_var_decl f.svar in
+  let ret = A.make_fresh (f.svar.vname ^ "_ret") in
+  let formals = List.map analyze_var_decl f.sformals in
+  let newf = A.make_function f.svar.vname formals ret in
+    if !show_progress then
+      Printf.printf "Analyzing function %s\n" f.svar.vname;
+    fun_varinfo_map := F.add f.svar f (!fun_varinfo_map);
+    current_fundec := Some f;
+    H.add fun_access_map f (H.create 8);
+    A.assign oldlv newf;
+    current_ret := Some ret;
+    analyze_block f.sbody
+
+let analyze_global (g : global ) : unit =
+  match g with
+      GVarDecl (v, l) -> () (* ignore (analyze_var_decl(v)) -- no need *)
+    | GVar (v, init, l) ->
+        all_globals := v :: !all_globals;
+        begin
+          match init.init with
+              Some i -> A.assign (analyze_var_decl v) (analyze_init i)
+            | None -> ignore (analyze_var_decl v)
+        end
+    | GFun (f, l) ->
+        all_functions := f :: !all_functions;
+        analyze_function f
+    | _ -> ()
+
+let analyze_file (f : file) : unit =
+  iterGlobals f analyze_global
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* High-level Query Interface                                          *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Same as analyze_expr, but no constraints. *)
+let rec traverse_expr (e : exp) : A.tau =
+  H.find expressions e
+
+and traverse_expr_as_lval (e : exp) : A.lvalue =
+  match e with
+    | Lval l -> traverse_lval l
+    | _ -> assert false (* todo -- other kinds of expressions? *)
+
+and traverse_lval (lv : lval ) : A.lvalue =
+  H.find lvalues lv
+
+let may_alias (e1 : exp) (e2 : exp) : bool =
+  let tau1,tau2 = traverse_expr e1, traverse_expr e2 in
+  let result = A.may_alias tau1 tau2 in
+    if !debug_may_aliases then
+      begin
+        let doc1 = d_exp () e1 in
+        let doc2 = d_exp () e2 in
+        let s1 = Pretty.sprint ~width:30 doc1 in
+        let s2 = Pretty.sprint ~width:30 doc2 in
+          Printf.printf
+            "%s and %s may alias? %s\n"
+            s1
+            s2
+            (if result then "yes" else "no")
+      end;
+    result
+
+let resolve_lval (lv : lval) : varinfo list =
+  A.points_to (traverse_lval lv)
+
+let resolve_exp (e : exp) : varinfo list =
+  A.epoints_to (traverse_expr e)
+
+let resolve_funptr (e : exp) : fundec list =
+  let varinfos = A.epoints_to (traverse_expr e) in
+    List.fold_left
+      (fun fdecs -> fun vinf ->
+         try F.find vinf !fun_varinfo_map :: fdecs
+         with Not_found -> fdecs)
+      []
+      varinfos
+
+let count_hash_elts h =
+  let result = ref 0 in
+    H.iter (fun _ -> fun _ -> incr result) lvalue_hash;
+    !result
+
+let compute_may_aliases (b : bool) : unit =
+  let rec compute_may_aliases_aux (exps : exp list) =
+    match exps with
+        [] -> ()
+      | h :: t ->
+          ignore (List.map (may_alias h) t);
+          compute_may_aliases_aux t
+  and exprs : exp list ref = ref [] in
+    H.iter (fun e -> fun _ -> exprs := e :: !exprs) expressions;
+    compute_may_aliases_aux !exprs
+
+
+let compute_results (show_sets : bool) : unit =
+  let total_pointed_to = ref 0
+  and total_lvalues = H.length lvalue_hash
+  and counted_lvalues = ref 0
+  and lval_elts : (string * (string list)) list ref = ref [] in
+  let print_result (name, set) =
+    let rec print_set s =
+      match s with
+          [] -> ()
+        | h :: [] -> print_string h
+        | h :: t ->
+            print_string (h ^ ", ");
+            print_set t
+    and ptsize = List.length set in
+      total_pointed_to := !total_pointed_to + ptsize;
+      if ptsize > 0 then
+        begin
+          print_string (name ^ "(" ^ (string_of_int ptsize) ^ ") -> ");
+          print_set set;
+          print_newline ()
+        end
+  in
+  (* Make the most pessimistic assumptions about globals if an
+     undefined function is present. Such a function can write to every
+     global variable *)
+  let hose_globals () : unit =
+    List.iter
+      (fun vd -> A.assign_undefined (analyze_var_decl vd))
+      !all_globals
+  in
+  let show_progress_fn (counted : int ref) (total : int) : unit =
+    incr counted;
+    if !show_progress then
+      Printf.printf "Computed flow for %d of %d sets\n" !counted total
+  in
+    if !conservative_undefineds && !found_undefined then hose_globals ();
+    A.finished_constraints ();
+    if show_sets then
+      begin
+        print_endline "Computing points-to sets...";
+        Hashtbl.iter
+          (fun vinf -> fun lv ->
+             show_progress_fn counted_lvalues total_lvalues;
+             try lval_elts := (vinf.vname, A.points_to_names lv) :: !lval_elts
+             with A.UnknownLocation -> ())
+          lvalue_hash;
+        List.iter print_result !lval_elts;
+        Printf.printf
+          "Total number of things pointed to: %d\n"
+          !total_pointed_to
+      end;
+    if !debug_may_aliases then
+      begin
+        Printf.printf "Printing may alias relationships\n";
+        compute_may_aliases true
+      end
+
+let print_types () : unit =
+  print_string "Printing inferred types of lvalues...\n";
+  Hashtbl.iter
+    (fun vi -> fun lv ->
+       Printf.printf "%s : %s\n" vi.vname (A.string_of_lvalue lv))
+    lvalue_hash
+
+
+
+(** Alias queries. For each function, gather sets of locals, formals, and
+    globals. Do n^2 work for each of these functions, reporting whether or not
+    each pair of values is aliased. Aliasing is determined by taking points-to
+    set intersections.
+*)
+let compute_aliases = compute_may_aliases
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Abstract Location Interface                                         *)
+(*                                                                     *)
+(***********************************************************************)
+
+type absloc = A.absloc
+
+let rec lvalue_of_varinfo (vi : varinfo) : A.lvalue =
+  H.find lvalue_hash vi
+
+let lvalue_of_lval = traverse_lval
+let tau_of_expr = traverse_expr
+
+(** return an abstract location for a varinfo, resp. lval *)
+let absloc_of_varinfo vi =
+  A.absloc_of_lvalue (lvalue_of_varinfo vi)
+
+let absloc_of_lval lv =
+  A.absloc_of_lvalue (lvalue_of_lval lv)
+
+let absloc_e_points_to e =
+  A.absloc_epoints_to (tau_of_expr e)
+
+let absloc_lval_aliases lv =
+  A.absloc_points_to (lvalue_of_lval lv)
+
+(* all abslocs that e transitively points to *)
+let absloc_e_transitive_points_to (e : Cil.exp) : absloc list =
+  let rec lv_trans_ptsto (worklist : varinfo list) (acc : varinfo list) : absloc list =
+    match worklist with
+        [] -> List.map absloc_of_varinfo acc
+      | vi :: wklst'' ->
+          if List.mem vi acc then lv_trans_ptsto wklst'' acc
+          else
+            lv_trans_ptsto
+              (List.rev_append
+                 (A.points_to (lvalue_of_varinfo vi))
+                 wklst'')
+              (vi :: acc)
+  in
+    lv_trans_ptsto (A.epoints_to (tau_of_expr e)) []
+
+let absloc_eq a b = A.absloc_eq (a, b)
+
+let d_absloc: unit -> absloc -> Pretty.doc = A.d_absloc
+
+
+let ptrAnalysis = ref false
+let ptrResults = ref false
+let ptrTypes = ref false
+
+
+
+(** Turn this into a CIL feature *)
+let feature : featureDescr = {
+  fd_name = "ptranal";
+  fd_enabled = ptrAnalysis;
+  fd_description = "alias analysis";
+  fd_extraopt = [
+    ("--ptr_may_aliases",
+     Arg.Unit (fun _ -> debug_may_aliases := true),
+     "Print out results of may alias queries");
+    ("--ptr_unify", Arg.Unit (fun _ -> no_sub := true),
+     "Make the alias analysis unification-based");
+    ("--ptr_model_strings", Arg.Unit (fun _ -> model_strings := true),
+     "Make the alias analysis model string constants");
+    ("--ptr_conservative",
+     Arg.Unit (fun _ -> conservative_undefineds := true),
+     "Treat undefineds conservatively in alias analysis");
+    ("--ptr_results", Arg.Unit (fun _ -> ptrResults := true),
+     "print the results of the alias analysis");
+    ("--ptr_mono", Arg.Unit (fun _ -> analyze_mono := true),
+     "run alias analysis monomorphically");
+    ("--ptr_types",Arg.Unit (fun _ -> ptrTypes := true),
+     "print inferred points-to analysis types")
+  ];
+  fd_doit = (function (f: file) ->
+               analyze_file f;
+               compute_results !ptrResults;
+               if !ptrTypes then print_types ());
+  fd_post_check = false (* No changes *)
+}
diff --git a/cil/src/ext/pta/ptranal.mli b/cil/src/ext/pta/ptranal.mli
new file mode 100644
index 00000000..36eb7a54
--- /dev/null
+++ b/cil/src/ext/pta/ptranal.mli
@@ -0,0 +1,156 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(* Flags                                                               *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Print extra debugging info *)
+val debug : bool ref
+
+(** Debug constraints (print all constraints) *)
+val debug_constraints : bool ref
+
+(** Debug smart alias queries *)
+val debug_aliases : bool ref
+
+(** Debug may alias queries *)
+val debug_may_aliases : bool ref
+
+val smart_aliases : bool ref
+
+(** Print out the top level constraints *)
+val print_constraints : bool ref
+
+(** Make the analysis monomorphic *)
+val analyze_mono : bool ref
+
+(** Disable subtyping *)
+val no_sub : bool ref
+
+(** Make the flow step a no-op *)
+val no_flow : bool ref 
+
+(** Show the progress of the flow step *)
+val show_progress : bool ref 
+
+(** Treat undefined functions conservatively *)
+val conservative_undefineds : bool ref
+
+(***********************************************************************)
+(*                                                                     *)
+(* Building the Points-to Graph                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Analyze a file *)
+val analyze_file : Cil.file -> unit
+
+(** Print the type of each lvalue in the program *)
+val print_types : unit -> unit
+
+(***********************************************************************)
+(*                                                                     *)
+(* High-level Query Interface                                          *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** If undefined functions are analyzed conservatively, any of the 
+  high-level queries may raise this exception *)
+exception UnknownLocation
+
+val may_alias : Cil.exp -> Cil.exp -> bool
+
+val resolve_lval : Cil.lval -> (Cil.varinfo list)
+
+val resolve_exp : Cil.exp -> (Cil.varinfo list)
+
+val resolve_funptr : Cil.exp -> (Cil.fundec list)
+
+(***********************************************************************)
+(*                                                                     *)
+(* Low-level Query Interface                                           *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** type for abstract locations *)
+type absloc 
+
+(** Give an abstract location for a varinfo *)
+val absloc_of_varinfo : Cil.varinfo -> absloc
+
+(** Give an abstract location for an Cil lvalue *)
+val absloc_of_lval : Cil.lval -> absloc
+
+(** may the two abstract locations be aliased? *)
+val absloc_eq : absloc -> absloc -> bool
+
+val absloc_e_points_to  : Cil.exp -> absloc list
+val absloc_e_transitive_points_to : Cil.exp -> absloc list 
+
+val absloc_lval_aliases : Cil.lval -> absloc list
+
+(** Print a string representing an absloc, for debugging. *)
+val d_absloc : unit -> absloc -> Pretty.doc
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Printing results                                                    *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Compute points to sets for variables. If true is passed, print the sets. *)
+val compute_results : bool -> unit
+
+(*
+
+Deprecated these. -- jk
+
+(** Compute alias relationships. If true is passed, print all alias pairs. *)
+ val compute_aliases : bool -> unit
+
+(** Compute alias frequncy *)
+val compute_alias_frequency : unit -> unit
+
+
+*)
+
+val compute_aliases : bool  -> unit
+
+
+val feature: Cil.featureDescr
diff --git a/cil/src/ext/pta/setp.ml b/cil/src/ext/pta/setp.ml
new file mode 100644
index 00000000..a39b9722
--- /dev/null
+++ b/cil/src/ext/pta/setp.ml
@@ -0,0 +1,342 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* $Id: setp.ml,v 1.3 2003-02-19 19:26:31 jkodumal Exp $ *)
+
+(* Sets over ordered types *)
+
+module type PolyOrderedType =
+  sig
+    type 'a t
+    val compare: 'a t -> 'a t -> int
+  end
+
+module type S =
+  sig
+    type 'a elt
+    type 'a t
+    val empty: 'a t
+    val is_empty: 'a t -> bool
+    val mem: 'a elt -> 'a t -> bool
+    val add: 'a elt -> 'a t -> 'a t
+    val singleton: 'a elt -> 'a t
+    val remove: 'a elt -> 'a t -> 'a t
+    val union: 'a t -> 'a t -> 'a t
+    val inter: 'a t -> 'a t -> 'a t
+    val diff: 'a t -> 'a t -> 'a t
+    val compare: 'a t -> 'a t -> int
+    val equal: 'a t -> 'a t -> bool
+    val subset: 'a t -> 'a t -> bool
+    val iter: ('a elt -> unit) -> 'a t -> unit
+    val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b
+    val for_all: ('a elt -> bool) -> 'a t -> bool
+    val exists: ('a elt -> bool) -> 'a t -> bool
+    val filter: ('a elt -> bool) -> 'a t -> 'a t
+    val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t
+    val cardinal: 'a t -> int
+    val elements: 'a t -> 'a elt list
+    val min_elt: 'a t -> 'a elt
+    val max_elt: 'a t -> 'a elt
+    val choose: 'a t -> 'a elt
+  end
+
+module Make(Ord: PolyOrderedType) =
+  struct
+    type 'a elt = 'a Ord.t
+    type 'a t = Empty | Node of 'a t * 'a elt * 'a t * int
+
+    (* Sets are represented by balanced binary trees (the heights of the
+       children differ by at most 2 *)
+
+    let height = function
+        Empty -> 0
+      | Node(_, _, _, h) -> h
+
+    (* Creates a new node with left son l, value x and right son r.
+       l and r must be balanced and | height l - height r | <= 2.
+       Inline expansion of height for better speed. *)
+
+    let create l x r =
+      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
+      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
+      Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
+
+    (* Same as create, but performs one step of rebalancing if necessary.
+       Assumes l and r balanced.
+       Inline expansion of create for better speed in the most frequent case
+       where no rebalancing is required. *)
+
+    let bal l x r =
+      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
+      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
+      if hl > hr + 2 then begin
+        match l with
+          Empty -> invalid_arg "Set.bal"
+        | Node(ll, lv, lr, _) ->
+            if height ll >= height lr then
+              create ll lv (create lr x r)
+            else begin
+              match lr with
+                Empty -> invalid_arg "Set.bal"
+              | Node(lrl, lrv, lrr, _)->
+                  create (create ll lv lrl) lrv (create lrr x r)
+            end
+      end else if hr > hl + 2 then begin
+        match r with
+          Empty -> invalid_arg "Set.bal"
+        | Node(rl, rv, rr, _) ->
+            if height rr >= height rl then
+              create (create l x rl) rv rr
+            else begin
+              match rl with
+                Empty -> invalid_arg "Set.bal"
+              | Node(rll, rlv, rlr, _) ->
+                  create (create l x rll) rlv (create rlr rv rr)
+            end
+      end else
+        Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
+
+    (* Same as bal, but repeat rebalancing until the final result
+       is balanced. *)
+
+    let rec join l x r =
+      match bal l x r with
+        Empty -> invalid_arg "Set.join"
+      | Node(l', x', r', _) as t' ->
+          let d = height l' - height r' in
+          if d < -2 || d > 2 then join l' x' r' else t'
+
+    (* Merge two trees l and r into one.
+       All elements of l must precede the elements of r.
+       Assumes | height l - height r | <= 2. *)
+
+    let rec merge t1 t2 =
+      match (t1, t2) with
+        (Empty, t) -> t
+      | (t, Empty) -> t
+      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
+          bal l1 v1 (bal (merge r1 l2) v2 r2)
+
+    (* Same as merge, but does not assume anything about l and r. *)
+
+    let rec concat t1 t2 =
+      match (t1, t2) with
+        (Empty, t) -> t
+      | (t, Empty) -> t
+      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
+          join l1 v1 (join (concat r1 l2) v2 r2)
+
+    (* Splitting *)
+
+    let rec split x = function
+        Empty ->
+          (Empty, None, Empty)
+      | Node(l, v, r, _) ->
+          let c = Ord.compare x v in
+          if c = 0 then (l, Some v, r)
+          else if c < 0 then
+            let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
+          else
+            let (lr, vr, rr) = split x r in (join l v lr, vr, rr)
+
+    (* Implementation of the set operations *)
+
+    let empty = Empty
+
+    let is_empty = function Empty -> true | _ -> false
+
+    let rec mem x = function
+        Empty -> false
+      | Node(l, v, r, _) ->
+          let c = Ord.compare x v in
+          c = 0 || mem x (if c < 0 then l else r)
+
+    let rec add x = function
+        Empty -> Node(Empty, x, Empty, 1)
+      | Node(l, v, r, _) as t ->
+          let c = Ord.compare x v in
+          if c = 0 then t else
+          if c < 0 then bal (add x l) v r else bal l v (add x r)
+
+    let singleton x = Node(Empty, x, Empty, 1)
+
+    let rec remove x = function
+        Empty -> Empty
+      | Node(l, v, r, _) ->
+          let c = Ord.compare x v in
+          if c = 0 then merge l r else
+          if c < 0 then bal (remove x l) v r else bal l v (remove x r)
+
+    let rec union s1 s2 =
+      match (s1, s2) with
+        (Empty, t2) -> t2
+      | (t1, Empty) -> t1
+      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
+          if h1 >= h2 then
+            if h2 = 1 then add v2 s1 else begin
+              let (l2, _, r2) = split v1 s2 in
+              join (union l1 l2) v1 (union r1 r2)
+            end
+          else
+            if h1 = 1 then add v1 s2 else begin
+              let (l1, _, r1) = split v2 s1 in
+              join (union l1 l2) v2 (union r1 r2)
+            end
+
+    let rec inter s1 s2 =
+      match (s1, s2) with
+        (Empty, t2) -> Empty
+      | (t1, Empty) -> Empty
+      | (Node(l1, v1, r1, _), t2) ->
+          match split v1 t2 with
+            (l2, None, r2) ->
+              concat (inter l1 l2) (inter r1 r2)
+          | (l2, Some _, r2) ->
+              join (inter l1 l2) v1 (inter r1 r2)
+
+    let rec diff s1 s2 =
+      match (s1, s2) with
+        (Empty, t2) -> Empty
+      | (t1, Empty) -> t1
+      | (Node(l1, v1, r1, _), t2) ->
+          match split v1 t2 with
+            (l2, None, r2) ->
+              join (diff l1 l2) v1 (diff r1 r2)
+          | (l2, Some _, r2) ->
+              concat (diff l1 l2) (diff r1 r2)
+
+    let rec compare_aux l1 l2 =
+        match (l1, l2) with
+        ([], []) -> 0
+      | ([], _)  -> -1
+      | (_, []) -> 1
+      | (Empty :: t1, Empty :: t2) ->
+          compare_aux t1 t2
+      | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) ->
+          let c = Ord.compare v1 v2 in
+          if c <> 0 then c else compare_aux (r1::t1) (r2::t2)
+      | (Node(l1, v1, r1, _) :: t1, t2) ->
+          compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2
+      | (t1, Node(l2, v2, r2, _) :: t2) ->
+          compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)
+
+    let compare s1 s2 =
+      compare_aux [s1] [s2]
+
+    let equal s1 s2 =
+      compare s1 s2 = 0
+
+    let rec subset s1 s2 =
+      match (s1, s2) with
+        Empty, _ ->
+          true
+      | _, Empty ->
+          false
+      | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
+          let c = Ord.compare v1 v2 in
+          if c = 0 then
+            subset l1 l2 && subset r1 r2
+          else if c < 0 then
+            subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
+          else
+            subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
+
+    let rec iter f = function
+        Empty -> ()
+      | Node(l, v, r, _) -> iter f l; f v; iter f r
+
+    let rec fold f s accu =
+      match s with
+        Empty -> accu
+      | Node(l, v, r, _) -> fold f l (f v (fold f r accu))
+
+    let rec for_all p = function
+        Empty -> true
+      | Node(l, v, r, _) -> p v && for_all p l && for_all p r
+
+    let rec exists p = function
+        Empty -> false
+      | Node(l, v, r, _) -> p v || exists p l || exists p r
+
+    let filter p s =
+      let rec filt accu = function
+        | Empty -> accu
+        | Node(l, v, r, _) ->
+            filt (filt (if p v then add v accu else accu) l) r in
+      filt Empty s
+
+    let partition p s =
+      let rec part (t, f as accu) = function
+        | Empty -> accu
+        | Node(l, v, r, _) ->
+            part (part (if p v then (add v t, f) else (t, add v f)) l) r in
+      part (Empty, Empty) s
+
+    let rec cardinal = function
+        Empty -> 0
+      | Node(l, v, r, _) -> cardinal l + 1 + cardinal r
+
+    let rec elements_aux accu = function
+        Empty -> accu
+      | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
+
+    let elements s =
+      elements_aux [] s
+
+    let rec min_elt = function
+        Empty -> raise Not_found
+      | Node(Empty, v, r, _) -> v
+      | Node(l, v, r, _) -> min_elt l
+
+    let rec max_elt = function
+        Empty -> raise Not_found
+      | Node(l, v, Empty, _) -> v
+      | Node(l, v, r, _) -> max_elt r
+
+    let choose = min_elt
+
+  end
diff --git a/cil/src/ext/pta/setp.mli b/cil/src/ext/pta/setp.mli
new file mode 100644
index 00000000..a3b30313
--- /dev/null
+++ b/cil/src/ext/pta/setp.mli
@@ -0,0 +1,180 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* $Id: setp.mli,v 1.3 2003-02-19 19:26:31 jkodumal Exp $ *)
+
+(** Sets over ordered types.
+
+   This module implements the set data structure, given a total ordering
+   function over the set elements. All operations over sets
+   are purely applicative (no side-effects).
+   The implementation uses balanced binary trees, and is therefore
+   reasonably efficient: insertion and membership take time
+   logarithmic in the size of the set, for instance. 
+*)
+
+module type PolyOrderedType = 
+  sig
+    type 'a t
+      (** The type of the set elements. *)
+    val compare :  'a t -> 'a t -> int
+      (** A total ordering function over the set elements.
+          This is a two-argument function [f] such that
+          [f e1 e2] is zero if the elements [e1] and [e2] are equal,
+          [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+          and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+          Example: a suitable ordering function is
+          the generic structural comparison function {!Pervasives.compare}. *)
+  end
+(** Input signature of the functor {!Set.Make}. *)
+
+module type S =
+  sig
+    type 'a elt
+    (** The type of the set elements. *)
+
+    type 'a t
+    (** The type of sets. *)
+
+    val empty: 'a t
+    (** The empty set. *)
+
+    val is_empty: 'a t -> bool
+    (** Test whether a set is empty or not. *)
+
+    val mem: 'a elt -> 'a t -> bool
+      (** [mem x s] tests whether [x] belongs to the set [s]. *)
+
+    val add: 'a elt -> 'a t -> 'a t
+    (** [add x s] returns a set containing all elements of [s],
+       plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+
+    val singleton: 'a elt -> 'a t
+    (** [singleton x] returns the one-element set containing only [x]. *)
+
+    val remove: 'a elt -> 'a t -> 'a t
+    (** [remove x s] returns a set containing all elements of [s],
+       except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+
+    val union: 'a t -> 'a t -> 'a t
+    (** Set union. *)
+
+    val inter: 'a t -> 'a t -> 'a t
+    (** Set interseection. *)
+
+    (** Set difference. *)
+    val diff: 'a t -> 'a t -> 'a t
+
+    val compare: 'a t -> 'a t -> int
+    (** Total ordering between sets. Can be used as the ordering function
+       for doing sets of sets. *)
+
+    val equal: 'a t -> 'a t -> bool
+    (** [equal s1 s2] tests whether the sets [s1] and [s2] are
+       equal, that is, contain equal elements. *)
+
+    val subset: 'a t -> 'a t -> bool
+    (** [subset s1 s2] tests whether the set [s1] is a subset of
+       the set [s2]. *)
+
+    val iter: ('a elt -> unit) -> 'a t -> unit
+    (** [iter f s] applies [f] in turn to all elements of [s].
+       The order in which the elements of [s] are presented to [f]
+       is unspecified. *)
+
+    val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b
+    (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
+       where [x1 ... xN] are the elements of [s].
+       The order in which elements of [s] are presented to [f] is
+       unspecified. *)
+
+    val for_all: ('a elt -> bool) -> 'a t -> bool
+    (** [for_all p s] checks if all elements of the set
+       satisfy the predicate [p]. *)
+
+    val exists: ('a elt -> bool) -> 'a t -> bool
+    (** [exists p s] checks if at least one element of
+       the set satisfies the predicate [p]. *)
+        
+    val filter: ('a elt -> bool) -> 'a t -> 'a t
+    (** [filter p s] returns the set of all elements in [s]
+       that satisfy predicate [p]. *)
+
+    val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t
+    (** [partition p s] returns a pair of sets [(s1, s2)], where
+       [s1] is the set of all the elements of [s] that satisfy the
+       predicate [p], and [s2] is the set of all the elements of
+       [s] that do not satisfy [p]. *)
+
+    val cardinal: 'a t -> int
+    (** Return the number of elements of a set. *)
+
+    val elements: 'a t -> 'a elt list
+    (** Return the list of all elements of the given set.
+       The returned list is sorted in increasing order with respect
+       to the ordering [Ord.compare], where [Ord] is the argument
+       given to {!Set.Make}. *)
+
+    val min_elt: 'a t -> 'a elt
+    (** Return the smallest element of the given set
+       (with respect to the [Ord.compare] ordering), or raise
+       [Not_found] if the set is empty. *)
+
+    val max_elt: 'a t -> 'a elt
+    (** Same as {!Set.S.min_elt}, but returns the largest element of the
+       given set. *)
+
+    val choose: 'a t -> 'a elt
+    (** Return one element of the given set, or raise [Not_found] if
+       the set is empty. Which element is chosen is unspecified,
+       but equal elements will be chosen for equal sets. *)
+  end
+(** Output signature of the functor {!Set.Make}. *)
+
+module Make (Ord : PolyOrderedType) : S with type 'a elt = 'a Ord.t
+(** Functor building an implementation of the set structure
+   given a totally ordered type. *)
diff --git a/cil/src/ext/pta/steensgaard.ml b/cil/src/ext/pta/steensgaard.ml
new file mode 100644
index 00000000..63686934
--- /dev/null
+++ b/cil/src/ext/pta/steensgaard.ml
@@ -0,0 +1,1417 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(*                                                                     *)
+(* This file is currently unused by CIL.  It is included in the        *)
+(*   distribution for reference only.                                  *)
+(*                                                                     *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Type Declarations                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+exception Inconsistent of string
+exception Bad_cache
+exception No_contents
+exception Bad_proj
+exception Bad_type_copy
+exception Instantiation_cycle
+
+module U = Uref
+module S = Setp
+module H = Hashtbl
+module Q = Queue
+
+(** Polarity kinds-- positive, negative, or nonpolar. *)
+type polarity = Pos 
+		| Neg 
+		| Non
+
+(** Label bounds. The polymorphic type is a hack for recursive modules *)  
+type 'a bound = {index : int; info : 'a} 
+
+(** The 'a type may in general contain urefs, which makes Pervasives.compare
+  incorrect. However, the bounds will always be correct because if two tau's
+  get unified, their cached instantiations will be re-entered into the 
+  worklist, ensuring that any labels find the new bounds *)
+module Bound =
+struct 
+  type 'a t = 'a bound
+  let compare (x : 'a t) (y : 'a t) = 
+    Pervasives.compare x y
+end
+
+module B = S.Make(Bound)
+
+type 'a boundset = 'a B.t
+
+(** Constants, which identify elements in points-to sets *)
+type constant = int * string
+
+module Constant =
+struct
+  type t = constant
+
+  let compare ((xid,_) : t) ((yid,_) : t) =
+    Pervasives.compare xid yid
+end
+
+module C = Set.Make(Constant)
+
+(** Sets of constants. Set union is used when two labels containing 
+  constant sets are unified *)
+type constantset = C.t
+
+type lblinfo = {
+  mutable l_name: string;
+  (** Name of this label *)
+  mutable aliases: constantset;
+  (** Set of constants (tags) for checking aliases *)
+  p_bounds: label boundset U.uref; 
+  (** Set of umatched (p) lower bounds *)
+  n_bounds: label boundset U.uref; 
+  (** Set of unmatched (n) lower bounds *)
+  mutable p_cached: bool;
+  (** Flag indicating whether all reachable p edges have been locally cached *)
+  mutable n_cached: bool;
+  (** Flag indicating whether all reachable n edges have been locally cached *)
+  mutable on_path: bool;
+  (** For cycle detection during reachability queries *)
+}
+
+(** Constructor labels *)
+and label = lblinfo U.uref 
+
+(** The type of lvalues. *)
+type lvalue = {
+  l: label; 
+  contents: tau
+}
+
+(** Data for variables. *)
+and vinfo = {
+  v_name: string; 
+  mutable v_global: bool; 
+  v_cache: cache
+} 
+
+(** Data for ref constructors.  *)
+and rinfo = {
+  rl: label; 
+  mutable r_global: bool; 
+  points_to: tau; 
+  r_cache: cache
+}
+
+(** Data for fun constructors. *)
+and finfo = {
+  fl: label; 
+  mutable f_global: bool; 
+  args: tau list ref; 
+  ret: tau; 
+  f_cache: cache
+}
+
+(* Data for pairs. Note there is no label. *)
+and pinfo = {
+  mutable p_global: bool; 
+  ptr: tau; 
+  lam: tau; 
+  p_cache: cache
+}
+
+(** Type constructors discovered by type inference *)
+and tinfo = Wild
+            | Var of vinfo
+	    | Ref of rinfo
+	    | Fun of finfo
+	    | Pair of pinfo 
+ 
+(** The top-level points-to type. *)
+and tau = tinfo U.uref
+
+(** The instantiation constraint cache. The index is used as a key. *)
+and cache = (int,polarity * tau) H.t
+
+(* Type of semi-unification constraints *)
+type su_constraint = Instantiation of tau * (int * polarity) * tau
+		     | Unification of tau * tau
+
+(** Association lists, used for printing recursive types. The first element 
+  is a type that has been visited. The second element is the string
+  representation of that type (so far). If the string option is set, then 
+  this type occurs within itself, and is associated with the recursive var
+  name stored in the option. When walking a type, add it to an association 
+  list. 
+
+  Example : suppose we have the constraint 'a = ref('a). The type is unified
+  via cyclic unification, and would loop infinitely if we attempted to print
+  it. What we want to do is print the type u rv. ref(rv). This is accomplished
+  in the following manner:
+  
+  -- ref('a) is visited. It is not in the association list, so it is added
+  and the string "ref(" is stored in the second element. We recurse to print
+  the first argument of the constructor.
+
+  -- In the recursive call, we see that 'a (or ref('a)) is already in the
+  association list, so the type is recursive. We check the string option,
+  which is None, meaning that this is the first recurrence of the type. We
+  create a new recursive variable, rv and set the string option to 'rv. Next,
+  we prepend u rv. to the string representation we have seen before, "ref(",
+  and return "rv" as the string representation of this type.
+
+  -- The string so far is "u rv.ref(". The recursive call returns, and we
+  complete the type by printing the result of the call, "rv", and ")"
+
+  In a type where the recursive variable appears twice, e.g. 'a = pair('a,'a),
+  the second time we hit 'a, the string option will be set, so we know to 
+  reuse the same recursive variable name.
+*)
+type association = tau * string ref * string option ref
+  
+(***********************************************************************)
+(*                                                                     *)
+(* Global Variables                                                    *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Print the instantiations constraints (loops with cyclic structures). *)
+let print_constraints : bool ref = ref false
+
+(** Solve constraints as they are introduced. If this is false, constraints
+  are solved in batch fashion at calls to solveConstraints. *)
+let solve_online : bool ref = ref true
+
+(** If true, print all constraints (including induced) and show additional 
+ debug output. *)
+let debug = ref false			       
+let debug_constraints = debug
+
+(** If true, print out extra verbose debug information (including contents
+  of label sets *)
+let verbose_debug = ref false
+
+
+(** If true, make the flow step a no-op *)
+let no_flow = ref false
+
+let no_sub = ref false
+
+(** If true, do not add instantiation constraints *)
+let analyze_mono = ref false
+
+(** A counter for generating unique integers. *)
+let counter : int ref = ref 0
+
+(** A list of equality constraints. *)
+let eq_worklist : su_constraint Q.t = Q.create()
+
+(** A list of instantiation constraints. *)
+let inst_worklist : su_constraint Q.t = Q.create()
+
+(***********************************************************************)
+(*                                                                     *)
+(* Utility Functions                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Consistency check for inferred types *)
+let  pair_or_var (t : tau) = 
+  match (U.deref t) with
+    | Pair _ -> true
+    | Var _ -> true
+    | _ -> false
+
+let ref_or_var (t : tau) =
+   match (U.deref t) with
+     | Ref _ -> true
+     | Var _ -> true
+     | _ -> false
+
+let fun_or_var (t : tau) =
+  match (U.deref t) with
+    | Fun _ -> true
+    | Var _ -> true
+    |  _ -> false
+
+(** Generate a unique integer. *)
+let fresh_index () : int = 
+  incr counter; 
+  !counter
+
+(** Negate a polarity. *)
+let negate (p : polarity) : polarity =
+  match p with
+    | Pos -> Neg
+    | Neg -> Pos
+    | Non -> Non
+
+(** Compute the least-upper-bounds of two polarities. *)
+let lub (p,p' : polarity * polarity) : polarity = 
+  match p with
+    | Pos -> 
+	begin
+	  match p' with 
+	    | Pos -> Pos
+	    | _ -> Non
+	end
+    | Neg -> 
+	begin
+	  match p' with
+	    | Neg -> Neg 
+	    | _ -> Non
+	end
+    | Non -> Non
+
+(** Extract the cache from a type *)
+let get_cache (t : tau) : cache =
+  match U.deref t with 
+    | Wild -> raise Bad_cache
+    | Var v -> v.v_cache
+    | Ref r -> r.r_cache
+    | Pair p -> p.p_cache
+    | Fun f -> f.f_cache
+
+(** Determine whether or not a type is global *)
+let get_global (t : tau) : bool = 
+  match U.deref t with
+    |  Wild -> false
+    | Var v -> v.v_global
+    | Ref r -> r.r_global
+    | Pair p -> p.p_global
+    | Fun f -> f.f_global
+
+(** Return true if a type is monomorphic (global). *)
+let global_tau = get_global
+
+let global_lvalue lv = get_global lv.contents
+
+(** Return true if e is a member of l (according to uref equality) *)
+let rec ulist_mem e l =
+  match l with
+    | [] -> false
+    | h :: t -> if (U.equal(h,e)) then true else ulist_mem e t 
+
+(** Convert a polarity to a string *)
+let string_of_polarity p = 
+    match p with 
+      | Pos -> "+"
+      | Neg -> "-"
+      | Non -> "T"
+
+(** Convert a label to a string, short representation *)
+let string_of_label2 (l : label) : string = 
+  "\"" ^ (U.deref l).l_name ^ "\""
+
+(** Convert a label to a string, long representation *)
+let string_of_label (l : label ) : string =
+  let rec constset_to_string = function
+    | (_,s) :: [] -> s
+    | (_,s) :: t -> s ^ "," ^ (constset_to_string t)
+    | [] -> ""
+  in
+  let aliases = constset_to_string (C.elements ((U.deref l).aliases))
+  in
+    if ( (aliases = "") || (not !verbose_debug))
+    then string_of_label2 l 
+    else aliases
+
+(** Return true if the element [e] is present in the association list *)
+let rec assoc_list_mem (e : tau) (l : association list) =
+  match l with
+    | [] -> None
+    | (h,s,so) :: t -> 
+	if (U.equal(h,e)) then (Some (s,so)) else assoc_list_mem e t
+	
+(** Given a tau, create a unique recursive variable name. This should always
+  return the same name for a given tau *)
+let fresh_recvar_name (t : tau) : string =	    
+  match U.deref t with
+    | Pair p -> "rvp" ^ string_of_int((Hashtbl.hash p)) 
+    | Ref r -> "rvr" ^ string_of_int((Hashtbl.hash r)) 
+    | Fun f -> "rvf" ^ string_of_int((Hashtbl.hash f))
+    | _ -> raise (Inconsistent ("recvar_name"))
+
+(** Return a string representation of a tau, using association lists. *)
+let string_of_tau (t : tau ) : string = 
+  let tau_map : association list ref = ref [] in
+  let rec string_of_tau' t = 
+    match (assoc_list_mem t (!tau_map)) with
+      | Some (s,so) -> (* recursive type. see if a var name has been set *)
+	  begin
+	    match (!so) with
+	      | None ->
+		  begin
+		    let rv = fresh_recvar_name(t) in
+		      s := "u " ^ rv ^ "." ^ (!s);
+		      so := Some (rv);
+		      rv
+		  end
+	      | Some rv -> rv
+	  end
+      | None -> (* type's not recursive. Add it to the assoc list and cont. *)
+	  let s = ref "" in
+	  let so : string option ref = ref None in
+	    begin
+	      tau_map := (t,s,so) :: (!tau_map);
+
+	      (match (U.deref t) with
+		| Wild -> s := "_"; 
+		| Var v -> s := v.v_name;
+		| Pair p -> 
+		    begin
+		      assert (ref_or_var(p.ptr));
+		      assert (fun_or_var(p.lam));
+		      s := "{";
+		      s := (!s) ^ (string_of_tau' p.ptr);
+		      s := (!s) ^ ",";
+		      s := (!s) ^ (string_of_tau' p.lam);
+		      s := (!s) ^"}"
+		
+		    end
+		| Ref r ->
+		    begin
+		      assert(pair_or_var(r.points_to));
+		      s := "ref(|";
+		      s := (!s) ^ (string_of_label r.rl);
+		      s := (!s) ^ "|,";
+		      s := (!s) ^ (string_of_tau' r.points_to);
+		      s := (!s) ^ ")"
+		    
+		    end
+		| Fun f ->
+		    begin
+		      assert(pair_or_var(f.ret));
+		      let rec string_of_args = function
+			| h :: [] ->
+			    begin
+			      assert(pair_or_var(h));
+			      s := (!s) ^ (string_of_tau' h)
+			    end
+			| h :: t -> 
+			    begin
+			      assert(pair_or_var(h));
+			      s := (!s) ^ (string_of_tau' h) ^ ",";
+			      string_of_args t
+			    end
+			| [] -> ()
+		      in
+			s := "fun(|";
+			s := (!s) ^ (string_of_label f.fl);
+			s := (!s) ^ "|,";
+			s := (!s) ^ "<";
+			if (List.length !(f.args) > 0) 
+			then
+			  string_of_args !(f.args)
+			else
+			  s := (!s) ^ "void";
+			s := (!s) ^">,";
+			s := (!s) ^ (string_of_tau' f.ret);
+			s := (!s) ^ ")"
+		    end);
+	      tau_map := List.tl (!tau_map);
+	      !s
+	    end
+  in
+    string_of_tau' t
+
+(** Convert an lvalue to a string *)	
+let rec string_of_lvalue (lv : lvalue) : string =
+  let contents = (string_of_tau(lv.contents)) in
+  let l = (string_of_label lv.l) in
+    assert(pair_or_var(lv.contents));
+    Printf.sprintf "[%s]^(%s)" contents l
+	      
+(** Print a list of tau elements, comma separated *)
+let rec print_tau_list (l : tau list) : unit = 
+  let t_strings = List.map string_of_tau l in
+  let rec print_t_strings = function
+    | h :: [] -> print_string h; print_newline();
+    | h :: t -> print_string h; print_string ", "; print_t_strings t
+    | [] -> ()
+  in
+    print_t_strings t_strings
+
+(** Print a constraint. *)
+let print_constraint (c : su_constraint) = 
+  match c with 
+    | Unification (t,t') -> 
+	let lhs = string_of_tau t in
+	let rhs = string_of_tau t' in 
+	  Printf.printf "%s == %s\n" lhs rhs
+    | Instantiation (t,(i,p),t') ->
+	let lhs = string_of_tau t in
+	let rhs = string_of_tau t' in
+	let index = string_of_int i in
+	let pol = string_of_polarity p in
+	  Printf.printf "%s <={%s,%s} %s\n" lhs index pol rhs
+
+(* If [positive] is true, return the p-edge bounds, otherwise, return
+   the n-edge bounds. *)    
+let get_bounds (positive : bool) (l : label) : label boundset U.uref =
+  if (positive) then
+    (U.deref l).p_bounds
+  else
+    (U.deref l).n_bounds
+
+(** Used for cycle detection during the flow step. Returns true if the
+ label [l] is found on the current path. *)
+let on_path (l : label) : bool =
+  (U.deref l).on_path
+
+(** Used for cycle detection during the flow step. Identifies [l] as being
+  on/off the current path. *) 
+let set_on_path (l : label) (b : bool) : unit =
+  (U.deref l).on_path <- b
+
+(** Make the type a global type *)
+let set_global (t : tau) (b : bool) : bool =
+  if (!debug && b) 
+  then 
+    Printf.printf "Setting a new global : %s\n" (string_of_tau t);
+  begin
+    assert ( (not (get_global(t)) ) || b );
+    (match U.deref t with
+       | Wild -> ()
+       | Var v -> v.v_global <- b
+       | Ref r -> r.r_global <- b
+       | Pair p -> p.p_global <- b
+       | Fun f -> f.f_global <- b);
+    b
+  end
+
+(** Return a label's bounds as a string *)
+let string_of_bounds (is_pos : bool) (l : label) : string =
+  let bounds = 
+    if (is_pos) then
+      U.deref ((U.deref l).p_bounds)
+    else
+      U.deref ((U.deref l).n_bounds)
+  in
+    B.fold (fun b -> fun res -> res ^ (string_of_label2 b.info) ^ " "
+	   ) bounds ""
+    
+(***********************************************************************)
+(*                                                                     *)
+(* Type Operations -- these do not create any constraints              *)
+(*                                                                     *)
+(***********************************************************************)
+
+let wild_val = U.uref Wild
+
+(** The wild (don't care) value. *)
+let wild () : tau =
+  wild_val
+
+(** Create an lvalue with label [lbl] and tau contents [t]. *)
+let make_lval (lbl,t : label * tau) : lvalue = 
+  {l = lbl; contents = t}
+
+(** Create a new label with name [name]. Also adds a fresh constant
+ with name [name] to this label's aliases set. *)  
+let make_label (name : string) : label =
+  U.uref {
+    l_name = name;
+    aliases = (C.add (fresh_index(),name) C.empty); 
+    p_bounds = U.uref (B.empty); 
+    n_bounds = U.uref (B.empty);
+    p_cached = false;
+    n_cached = false;
+    on_path = false
+ }
+
+(** Create a new label with an unspecified name and an empty alias set. *) 
+let fresh_label () : label =
+  U.uref {
+    l_name = "l_" ^ (string_of_int (fresh_index()));
+    aliases = (C.empty); 
+    p_bounds = U.uref (B.empty); 
+    n_bounds = U.uref (B.empty);
+    p_cached = false;
+    n_cached = false;
+    on_path = false
+ }
+
+(** Create a fresh bound. *)
+let make_bound (i,a : int * 'a) : 'a bound = 
+  {index = i; info = a }
+
+(** Create a fresh named variable with name '[name]. *)
+let make_var (b: bool) (name : string) : tau =
+   U.uref (Var {v_name = ("'" ^name); 
+		v_global = b; 
+		v_cache = H.create 4})
+
+(** Create a fresh unnamed variable (name will be 'fv). *)
+let fresh_var () : tau =
+  make_var false ("fv" ^ (string_of_int (fresh_index())) )
+
+(** Create a fresh unnamed variable (name will be 'fi). *)
+let fresh_var_i () : tau = 
+ make_var false ("fi" ^ (string_of_int (fresh_index())) )
+
+(** Create a Fun constructor. *)
+let make_fun (lbl,a,r : label * (tau list) * tau) : tau =
+  U.uref (Fun {fl = lbl ; 
+	       f_global = false; 
+	       args = ref a; 
+	       ret = r;
+	       f_cache = H.create 4})
+
+(** Create a Ref constructor. *)
+let make_ref (lbl,pt : label * tau) : tau =
+  U.uref (Ref {rl = lbl ; 
+	       r_global = false; 
+	       points_to = pt; 
+	       r_cache = H.create 4})
+
+(** Create a Pair constructor. *)
+let make_pair (p,f : tau * tau) : tau =
+  U.uref (Pair {ptr = p; 
+		p_global = false;
+		lam = f; 
+		p_cache = H.create 4})
+
+(** Copy the toplevel constructor of [t], putting fresh variables in each
+  argement of the constructor. *)
+let copy_toplevel (t : tau) : tau = 
+  match U.deref t with
+    | Pair _ -> 
+	make_pair (fresh_var_i(), fresh_var_i())
+    | Ref  _ -> 
+	make_ref (fresh_label(),fresh_var_i())
+    | Fun  f -> 
+	let fresh_fn = fun _ -> fresh_var_i()
+	in
+	  make_fun (fresh_label(), List.map fresh_fn !(f.args) , fresh_var_i())
+    | _ -> raise Bad_type_copy
+
+let pad_args (l,l' : (tau list ref) * (tau list ref)) : unit =
+  let padding = ref ((List.length (!l)) - (List.length (!l')))
+  in
+    if (!padding == 0) then ()
+    else 
+      let to_pad = 
+	if (!padding > 0) then l' else (padding := -(!padding);l)
+      in
+	for i = 1 to (!padding)  do
+	  to_pad := (!to_pad) @ [fresh_var()]
+	done
+
+(***********************************************************************)
+(*                                                                     *)
+(* Constraint Generation/ Resolution                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Returns true if the constraint has no effect, i.e. either the left-hand
+  side or the right-hand side is wild. *)
+let wild_constraint (t,t' : tau * tau) : bool = 
+  let ti,ti' = U.deref t, U.deref t' in
+    match ti,ti' with
+      | Wild, _ -> true
+      | _, Wild -> true
+      | _ -> false
+
+exception Cycle_found
+
+(** Cycle detection between instantiations. Returns true if there is a cycle
+  from t to t' *)
+let exists_cycle (t,t' : tau * tau) : bool =
+  let visited : tau list ref = ref [] in
+  let rec exists_cycle' t =
+    if (ulist_mem t (!visited))
+    then
+      begin (*
+	print_string "Instantiation cycle found :";
+	print_tau_list (!visited);
+	print_newline();
+	print_string (string_of_tau t);
+	print_newline(); *)
+	(* raise Instantiation_cycle *) 
+	(* visited := List.tl (!visited) *) (* check *)
+      end
+    else
+      begin
+	visited := t :: (!visited);
+	if (U.equal(t,t')) 
+	then raise Cycle_found
+	else
+	  H.iter (fun _ -> fun (_,t'') -> 
+		    if (U.equal (t,t'')) then () 
+		    else
+		      ignore (exists_cycle' t'')
+		 ) (get_cache t) ;
+	visited := List.tl (!visited)
+      end
+  in
+    try
+      exists_cycle' t;
+      false
+    with
+      | Cycle_found -> true
+	
+exception Subterm
+  
+(** Returns true if [t'] is a proper subterm of [t] *)
+let proper_subterm (t,t') = 
+  let visited : tau list ref = ref [] in
+  let rec proper_subterm' t = 
+    if (ulist_mem t (!visited)) 
+    then () (* recursive type *)
+    else
+      if (U.equal (t,t'))
+      then raise Subterm
+      else
+	begin
+	  visited := t :: (!visited);
+	  (
+	    match (U.deref t) with
+	      | Wild -> ()
+	      | Var _ -> ()
+	      | Ref r ->
+		  proper_subterm' r.points_to
+	      | Pair p ->
+		  proper_subterm' p.ptr;
+		  proper_subterm' p.lam
+	      | Fun f ->
+		  proper_subterm' f.ret;
+		  List.iter (proper_subterm') !(f.args)
+	  );
+	  visited := List.tl (!visited)
+	  end
+  in
+    try
+      if (U.equal(t,t')) then false 
+      else
+	begin
+	  proper_subterm' t;
+	  false
+	end
+    with
+      | Subterm -> true
+
+(** The extended occurs check. Search for a cycle of instantiations from [t]
+  to [t']. If such a cycle exists, check to see that [t'] is a proper subterm
+  of [t]. If it is, then return true *)
+let eoc (t,t') : bool =
+  if (exists_cycle(t,t') && proper_subterm(t,t'))
+  then
+    begin
+      if (!debug)
+      then
+	Printf.printf "Occurs check : %s occurs within %s\n" (string_of_tau t')
+	  (string_of_tau t)
+      else 
+	();
+      true 
+    end
+  else
+   false
+  
+(** Resolve an instantiation constraint *)
+let rec instantiate_int (t,(i,p),t' : tau * (int * polarity) * tau) =
+  if  ( wild_constraint(t,t') || (not (store(t,(i,p),t'))) || 
+	U.equal(t,t') )
+  then ()
+  else 
+    let ti,ti' = U.deref t, U.deref t' in
+      match ti,ti' with 
+	| Ref r, Ref r' -> 
+	    instantiate_ref(r,(i,p),r')
+	| Fun f, Fun f' -> 
+	    instantiate_fun(f,(i,p),f')
+	| Pair pr, Pair pr' ->
+	    begin
+	      add_constraint_int (Instantiation (pr.ptr,(i,p),pr'.ptr));
+	      add_constraint_int (Instantiation (pr.lam,(i,p),pr'.lam))
+	    end
+	| Var v, _ -> ()
+	| _,Var v' -> 
+	    if eoc(t,t')
+	    then 
+	      add_constraint_int (Unification (t,t'))
+	    else
+	      begin
+		unstore(t,i);
+		add_constraint_int (Unification ((copy_toplevel t),t'));
+		add_constraint_int (Instantiation (t,(i,p),t')) 
+	      end
+	| _ -> raise (Inconsistent("instantiate"))
+
+(** Apply instantiations to the ref's label, and structurally down the type.
+  Contents of ref constructors are instantiated with polarity Non. *)
+and instantiate_ref (ri,(i,p),ri') : unit =
+  add_constraint_int (Instantiation(ri.points_to,(i,Non),ri'.points_to));
+  instantiate_label (ri.rl,(i,p),ri'.rl)
+
+(** Apply instantiations to the fun's label, and structurally down the type. 
+   Flip the polarity for the function's args. If the lengths of the argument
+   lists don't match, extend the shorter list as necessary.  *)
+and instantiate_fun (fi,(i,p),fi') : unit =
+    pad_args (fi.args, fi'.args);
+    assert(List.length !(fi.args) == List.length !(fi'.args));
+    add_constraint_int (Instantiation (fi.ret,(i,p),fi'.ret));
+    List.iter2 (fun t ->fun t' -> 
+		  add_constraint_int (Instantiation(t,(i,negate p),t'))) 
+      !(fi.args) !(fi'.args);
+    instantiate_label (fi.fl,(i,p),fi'.fl)
+
+(** Instantiate a label. Update the label's bounds with new flow edges. 
+ *)
+and instantiate_label (l,(i,p),l' : label * (int * polarity) * label) : unit =
+  if (!debug) then
+    Printf.printf "%s <= {%d,%s} %s\n" (string_of_label l) i 
+      (string_of_polarity p) (string_of_label l');
+  let li,li' = U.deref l, U.deref l' in
+    match p with
+      | Pos ->
+	  U.update (li'.p_bounds, 
+		    B.add(make_bound (i,l)) (U.deref li'.p_bounds)
+		   )
+      | Neg -> 
+	  U.update (li.n_bounds, 
+		    B.add(make_bound (i,l')) (U.deref li.n_bounds)
+		   )
+      | Non ->
+	  begin
+	    U.update (li'.p_bounds, 
+		      B.add(make_bound (i,l)) (U.deref li'.p_bounds)
+		     );
+	    U.update (li.n_bounds, 
+		      B.add(make_bound (i,l')) (U.deref li.n_bounds)
+		     )
+	  end
+	     
+(** Resolve a unification constraint. Does the uref unification after grabbing
+  a copy of the information before the two infos are unified. The other 
+  interesting feature of this function is the way 'globalness' is propagated.
+  If a non-global is unified with a global, the non-global becomes global. 
+  If the ecr became global, there is a problem because none of its cached 
+  instantiations know that the type became monomorphic. In this case, they
+  must be re-inserted via merge-cache. Merge-cache always reinserts cached
+  instantiations from the non-ecr type, i.e. the type that was 'killed' by the
+  unification. *)
+and unify_int (t,t' : tau * tau) : unit = 
+  if (wild_constraint(t,t') || U.equal(t,t')) 
+  then ()
+  else 
+    let ti, ti' = U.deref t, U.deref t' in
+      begin
+	U.unify combine (t,t');
+	match ti,ti' with
+	  | Var v, _ -> 
+	      begin 
+		if (set_global t' (v.v_global || (get_global t')))
+		then (H.iter (merge_cache t') (get_cache t'))
+		else ();
+		H.iter (merge_cache t') v.v_cache
+	      end
+	  | _, Var v ->
+	      begin 
+		if (set_global t (v.v_global || (get_global t)))
+		then (H.iter (merge_cache t) (get_cache t))
+		else ();
+		H.iter (merge_cache t) v.v_cache
+	      end
+	  | Ref r, Ref r' -> 
+	      begin
+		if (set_global t (r.r_global || r'.r_global))
+		then (H.iter (merge_cache t) (get_cache t))
+		else ();
+		H.iter (merge_cache t) r'.r_cache;
+		unify_ref(r,r')
+	      end
+	  | Fun f, Fun f' -> 
+	      begin
+		if (set_global t (f.f_global || f'.f_global))
+		then (H.iter (merge_cache t) (get_cache t))
+		else (); 
+		H.iter (merge_cache t) f'.f_cache;
+		unify_fun (f,f');
+	      end
+	  | Pair p, Pair p' ->
+	      begin
+		if (set_global t (p.p_global || p'.p_global))
+		then (H.iter (merge_cache t) (get_cache t))
+		else (); 
+		H.iter (merge_cache t) p'.p_cache;
+		add_constraint_int (Unification (p.ptr,p'.ptr));
+		add_constraint_int (Unification (p.lam,p'.lam))
+	      end
+	  | _ -> raise (Inconsistent("unify"))
+      end
+
+(** Unify the ref's label, and apply unification structurally down the type. *)
+and unify_ref (ri,ri' : rinfo * rinfo) : unit =
+  add_constraint_int (Unification (ri.points_to,ri'.points_to));
+  unify_label(ri.rl,ri'.rl) 
+
+(** Unify the fun's label, and apply unification structurally down the type, 
+  at arguments and return value. When combining two lists of different lengths,
+  always choose the longer list for the representative. *)
+and unify_fun (li,li' : finfo * finfo) : unit = 
+  let rec union_args  = function
+    | _, [] -> false
+    | [], _ -> true
+    | h :: t, h' :: t' -> 
+	add_constraint_int (Unification (h,h')); union_args(t,t') 
+  in
+    begin
+      unify_label(li.fl,li'.fl);
+      add_constraint_int (Unification (li.ret,li'.ret));
+      if (union_args(!(li.args),!(li'.args))) 
+      then li.args := !(li'.args);
+    end
+
+(** Unify two labels, combining the set of constants denoting aliases. *)
+and unify_label (l,l' : label * label) : unit =
+  let pick_name (li,li' : lblinfo * lblinfo) = 
+    if ( (String.length li.l_name) > 1 && (String.sub (li.l_name) 0 2) = "l_") 
+    then 
+      li.l_name <- li'.l_name
+    else ()
+  in
+  let combine_label (li,li' : lblinfo *lblinfo) : lblinfo =
+    let p_bounds = U.deref (li.p_bounds) in
+    let p_bounds' = U.deref (li'.p_bounds) in
+    let n_bounds = U.deref (li.n_bounds) in
+    let n_bounds' = U.deref (li'.n_bounds) in 
+      begin
+	pick_name(li,li');
+	li.aliases <- C.union (li.aliases) (li'.aliases);
+	U.update (li.p_bounds, (B.union p_bounds p_bounds'));
+	U.update (li.n_bounds, (B.union n_bounds n_bounds'));
+	li
+    end
+  in(*
+    if (!debug) then
+      begin
+	Printf.printf "Unifying %s with %s...\n" 
+	  (string_of_label l) (string_of_label l');
+	Printf.printf "pbounds : %s\n" (string_of_bounds true l);
+	Printf.printf "nbounds : %s\n" (string_of_bounds false l);
+	Printf.printf "pbounds : %s\n" (string_of_bounds true l');
+	Printf.printf "nbounds : %s\n\n" (string_of_bounds false l')
+      end; *)
+    U.unify combine_label (l,l')
+    (* if (!debug) then
+      begin
+	Printf.printf "pbounds : %s\n" (string_of_bounds true l);
+	Printf.printf "nbounds : %s\n" (string_of_bounds false l)
+      end *)
+
+(** Re-assert a cached instantiation constraint, since the old type was 
+  killed by a unification *)
+and merge_cache (rep : tau) (i : int) (p,t' : polarity * tau) : unit =
+  add_constraint_int (Instantiation (rep,(i,p),t'))
+      
+(** Pick the representative info for two tinfo's. This function prefers the
+  first argument when both arguments are the same structure, but when
+  one type is a structure and the other is a var, it picks the structure. *)
+and combine (ti,ti' : tinfo * tinfo) : tinfo = 
+  match ti,ti' with
+    | Var _, _ -> ti'
+    | _,_ -> ti 
+
+(** Add a new constraint induced by other constraints. *)
+and add_constraint_int (c : su_constraint) =
+  if (!print_constraints && !debug) then print_constraint c else (); 
+  begin
+    match c with
+      | Instantiation _ ->
+	  Q.add c inst_worklist
+      | Unification _ ->
+	  Q.add c eq_worklist
+  end;
+  if (!debug) then solve_constraints() else ()
+  
+(** Add a new constraint introduced through this module's interface (a 
+  top-level constraint). *)
+and add_constraint (c : su_constraint) =
+  begin
+    add_constraint_int (c);
+    if (!print_constraints && not (!debug)) then print_constraint c else (); 
+    if (!solve_online) then solve_constraints() else ()
+  end
+
+
+(* Fetch constraints, preferring equalities. *)
+and fetch_constraint () : su_constraint option =
+  if (Q.length eq_worklist > 0)
+  then 
+    Some (Q.take eq_worklist)
+  else if (Q.length inst_worklist > 0)
+  then
+    Some (Q.take inst_worklist)
+  else
+    None 
+
+(** Returns the target of a cached instantiation, if it exists. *)
+and target (t,i,p : tau * int * polarity) : (polarity * tau) option =
+  let cache = get_cache t in
+    if (global_tau t) then Some (Non,t) 
+    else
+      try
+	Some (H.find cache i)
+      with 
+	| Not_found -> None
+	  
+(** Caches a new instantiation, or applies well-formedness. *)
+and store ( t,(i,p),t' : tau * (int * polarity) * tau) : bool =
+  let cache = get_cache t in
+    match target(t,i,p) with
+      | Some (p'',t'') ->
+	  if (U.equal (t',t'') && (lub(p,p'') = p''))
+	  then
+	      false
+	  else
+	    begin
+	      add_constraint_int (Unification (t',t''));
+	      H.replace cache i (lub(p,p''),t'');
+	      (* add a new forced instantiation as well *)
+	      if (lub(p,p'') = p'') 
+	      then ()
+	      else
+		begin
+		  unstore(t,i);
+		  add_constraint_int (Instantiation (t,(i,lub(p,p'')),t''))
+		end;
+	      false 
+	    end
+      | None ->
+	  begin
+	    H.add cache i (p,t');
+	    true
+	  end
+
+(** Remove a cached instantiation. Used when type structure changes *)
+and unstore (t,i : tau * int) =
+let cache = get_cache t in
+  H.remove cache i
+
+(** The main solver loop. *)
+and solve_constraints () : unit = 
+  match fetch_constraint () with
+    | Some c ->
+	begin
+	  (match c with
+	     | Instantiation (t,(i,p),t') -> instantiate_int (t,(i,p),t')
+	     | Unification (t,t') -> unify_int (t,t')
+	  );
+	  solve_constraints()
+	end
+    | None -> ()
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Interface Functions                                                 *)
+(*                                                                     *)
+(***********************************************************************)
+    
+(** Return the contents of the lvalue. *)
+let rvalue (lv : lvalue) : tau = 
+  lv.contents
+
+(** Dereference the rvalue. If it does not have enough structure to support
+  the operation, then the correct structure is added via new unification
+  constraints. *)
+let rec deref (t : tau) : lvalue =
+  match U.deref t with 
+    | Pair p ->
+	(
+	  match U.deref (p.ptr) with
+	    | Var _ ->
+		begin 
+		 (* let points_to = make_pair(fresh_var(),fresh_var()) in *)
+		  let points_to = fresh_var() in 
+		  let l = fresh_label() in
+		  let r = make_ref(l,points_to)
+		  in
+		    add_constraint (Unification (p.ptr,r));
+		    make_lval(l, points_to)
+		end
+	    | Ref r -> make_lval(r.rl, r.points_to)
+	    | _ -> raise (Inconsistent("deref"))
+	)
+    | Var v -> 
+	begin
+	  add_constraint (Unification (t,make_pair(fresh_var(),fresh_var())));
+	  deref t
+	end
+    | _ -> raise (Inconsistent("deref -- no top level pair"))
+
+(** Form the union of [t] and [t']. *)
+let join (t : tau) (t' : tau) : tau = 
+  let t''  = fresh_var() in
+    add_constraint (Unification (t,t''));
+    add_constraint (Unification (t',t''));
+    t''
+
+(** Form the union of a list [tl], expected to be the initializers of some
+  structure or array type. *)
+let join_inits (tl : tau list) : tau = 
+  let t' = fresh_var() in
+    begin
+      List.iter (function t'' -> add_constraint (Unification(t',t''))) tl;
+      t'
+    end
+
+(** Take the address of an lvalue. Does not add constraints. *)
+let address (lv  : lvalue) : tau = 
+  make_pair (make_ref (lv.l, lv.contents), fresh_var() )
+    
+(** Instantiate a type with index i. By default, uses positive polarity. 
+ Adds an instantiation constraint. *)
+let instantiate (lv : lvalue) (i : int) : lvalue = 
+  if (!analyze_mono) then lv
+  else
+    begin
+      let l' = fresh_label () in
+      let t' = fresh_var_i () in
+	instantiate_label(lv.l,(i,Pos),l');
+	add_constraint (Instantiation (lv.contents,(i,Pos),t'));
+	make_lval(l',t') (* check -- fresh label ?? *)
+    end 
+    
+(** Constraint generated from assigning [t] to [lv]. *)
+let assign (lv : lvalue) (t : tau) : unit = 
+  add_constraint (Unification (lv.contents,t))
+    
+
+(** Project out the first (ref) component or a pair. If the argument [t] has
+  no discovered structure, raise No_contents. *)
+let proj_ref (t : tau) : tau = 
+  match U.deref t with
+    | Pair p -> p.ptr
+    | Var v -> raise No_contents
+    | _ -> raise Bad_proj
+
+(* Project out the second (fun) component of a pair. If the argument [t] has
+ no discovered structure, create it on the fly by adding constraints. *)
+let proj_fun (t : tau) : tau = 
+  match U.deref t with
+    | Pair p -> p.lam
+    | Var v -> 
+	let p,f = fresh_var(), fresh_var() in
+	  add_constraint (Unification (t,make_pair(p,f)));
+	  f
+    | _ -> raise Bad_proj
+
+let get_args (t : tau) : tau list ref =
+  match U.deref t with 
+    | Fun f -> f.args
+    | _ -> raise (Inconsistent("get_args"))
+
+(** Function type [t] is applied to the arguments [actuals]. Unifies the 
+  actuals with the formals of [t]. If no functions have been discovered for 
+  [t] yet, create a fresh one and unify it with t. The result is the return
+  value of the function. *)
+let apply (t : tau) (al : tau list) : tau = 
+  let f = proj_fun(t) in
+  let actuals = ref al in 
+  let formals,ret =
+    match U.deref f with
+      | Fun fi -> (fi.args),fi.ret
+      | Var v ->
+	  let new_l,new_ret,new_args = 
+	    fresh_label(), fresh_var (), 
+	    List.map (function _ -> fresh_var()) (!actuals) 
+	  in
+	  let new_fun = make_fun(new_l,new_args,new_ret) in
+	    add_constraint (Unification(new_fun,f));
+	    (get_args new_fun,new_ret)
+      | Ref _ -> raise (Inconsistent ("apply_ref"))
+      | Pair _ -> raise (Inconsistent ("apply_pair"))
+      | Wild -> raise (Inconsistent("apply_wild"))
+  in
+    pad_args(formals,actuals);
+    List.iter2 (fun actual -> fun formal -> 
+		  add_constraint (Unification (actual,formal))
+	       ) !actuals !formals;
+    ret 
+    
+(** Create a new function type with name [name], list of formal arguments 
+  [formals], and return value [ret]. Adds no constraints. *)
+let make_function (name : string) (formals : lvalue list) (ret : tau) : tau = 
+  let 
+    f = make_fun(make_label(name),List.map (fun x -> rvalue x) formals, ret) 
+  in
+    make_pair(fresh_var(),f)
+
+(** Create an lvalue. If [is_global] is true, the lvalue will be treated 
+    monomorphically. *)
+let make_lvalue (is_global : bool) (name : string) : lvalue = 
+  if (!debug && is_global) 
+  then 
+    Printf.printf "Making global lvalue : %s\n" name
+  else ();
+  make_lval(make_label(name), make_var is_global name)
+ 
+
+(** Create a fresh non-global named variable. *)
+let make_fresh (name : string) : tau =
+  make_var false (name)
+
+(** The default type for constants. *)
+let bottom () : tau = 
+  make_var false ("bottom")
+
+(** Unify the result of a function with its return value. *)
+let return (t : tau) (t' : tau) =
+  add_constraint (Unification (t,t'))
+
+
+(***********************************************************************)
+(*                                                                     *)
+(* Query/Extract Solutions                                             *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Unify the data stored in two label bounds. *)
+let combine_lbounds (s,s' : label boundset * label boundset) =
+  B.union s s'
+
+(** Truncates a list of urefs [l] to those elements up to and including the 
+  first occurence of the specified element [elt].  *)
+let truncate l elt = 
+  let keep = ref true in
+    List.filter 
+      (fun x -> 
+	 if (not (!keep)) 
+	 then 
+	     false
+	 else
+	   begin
+	     if  (U.equal(x,elt)) 
+	     then 
+	       keep := false
+	     else ();
+	     true
+	   end
+      ) l
+
+let debug_cycle_bounds is_pos c =
+  let rec debug_cycle_bounds' = function
+    | h :: [] -> 
+	Printf.printf "%s --> %s\n" (string_of_bounds is_pos h) 
+	(string_of_label2 h)
+    | h :: t ->
+	begin
+	  Printf.printf "%s --> %s\n" (string_of_bounds is_pos h)
+	    (string_of_label2 h);
+	  debug_cycle_bounds' t
+	end
+    | [] -> ()
+  in
+    debug_cycle_bounds' c
+
+(** For debugging, print a cycle of instantiations *)
+let debug_cycle (is_pos,c,l,p) =
+  let kind = if is_pos then "P" else "N" in
+  let rec string_of_cycle = function 
+    | h :: [] -> string_of_label2 h
+    | [] -> ""
+    | h :: t -> Printf.sprintf "%s,%s" (string_of_label2 h) (string_of_cycle t)
+  in
+    Printf.printf "Collapsing %s cycle around %s:\n" kind (string_of_label2 l);
+    Printf.printf "Elements are: %s\n" (string_of_cycle c);
+    Printf.printf "Per-element bounds:\n";
+    debug_cycle_bounds is_pos c;
+    Printf.printf "Full path is: %s" (string_of_cycle p);
+    print_newline()
+
+(** Compute pos or neg flow, depending on [is_pos]. Searches for cycles in the
+  instantiations (can these even occur?) and unifies either the positive or
+  negative edge sets for the labels on the cycle. Note that this does not 
+  ever unify the labels themselves. The return is the new bounds of the 
+  argument label *)
+let rec flow (is_pos : bool) (path : label list) (l : label) : label boundset =
+  let collapse_cycle () = 
+    let cycle = truncate path l in
+      debug_cycle (is_pos,cycle,l,path);
+      List.iter (fun x -> U.unify combine_lbounds 
+		   ((get_bounds is_pos x),get_bounds is_pos l)
+		) cycle
+  in
+    if (on_path l) 
+    then
+      begin
+	collapse_cycle (); 
+	(* set_on_path l false; *)
+	B.empty
+      end
+    else
+      if ( (is_pos && (U.deref l).p_cached) || 
+	   ( (not is_pos) && (U.deref l).n_cached) ) then
+	begin
+	  U.deref (get_bounds is_pos l)
+	end
+      else
+	begin
+	  let newbounds = ref B.empty in
+	  let base = get_bounds is_pos l in
+	    set_on_path l true;
+	    if (is_pos) then 
+	      (U.deref l).p_cached <- true 
+	    else 
+	      (U.deref l).n_cached <- true;
+	    B.iter 
+	      (fun x -> 
+		 if (U.equal(x.info,l)) then () 
+		 else
+		   (newbounds := 
+		    (B.union (!newbounds) (flow is_pos (l :: path) x.info)))
+	      ) (U.deref base); 
+	    set_on_path l false;
+	    U.update (base,(B.union (U.deref base) !newbounds));
+	    U.deref base
+	end
+	
+(** Compute and cache any positive flow. *)
+let pos_flow l : constantset  = 
+  let result = ref C.empty in 
+    begin
+      ignore (flow true [] l);
+      B.iter (fun x -> result := C.union (!result) (U.deref(x.info)).aliases )
+	(U.deref (get_bounds true l)); 
+      !result
+    end
+    
+(** Compute and cache any negative flow. *)
+let neg_flow l : constantset =
+  let result = ref C.empty in
+    begin
+      ignore (flow false [] l); 
+      B.iter (fun x -> result := C.union (!result) (U.deref(x.info)).aliases )
+	(U.deref (get_bounds false l));
+      !result
+    end
+    
+(** Compute and cache any pos-neg flow. Assumes that both pos_flow and
+  neg_flow have been computed for the label [l]. *)
+let pos_neg_flow(l : label) : constantset  =
+  let result = ref C.empty in
+    begin
+      B.iter (fun x -> result := C.union (!result) (pos_flow x.info))
+	(U.deref (get_bounds false l));
+      !result
+    end
+
+(** Compute a points-to set by computing positive, then negative, then
+  positive-negative flow for a label. *)
+let points_to_int (lv : lvalue) : constantset =
+  let visited_caches : cache list ref  = ref [] in
+  let rec points_to_tau (t : tau) : constantset =
+    try 
+      begin
+	match U.deref (proj_ref t) with
+	  | Var v -> C.empty
+	  | Ref r ->
+	      begin
+		let pos = pos_flow r.rl in
+		let neg = neg_flow r.rl in
+		let interproc = C.union (pos_neg_flow r.rl) (C.union pos neg)
+		in
+		  C.union ((U.deref(r.rl)).aliases) interproc
+	      end
+	  | _ -> raise (Inconsistent ("points_to"))
+      end
+    with
+      | No_contents ->
+	  begin
+	    match (U.deref t) with
+	      | Var v -> rebuild_flow v.v_cache
+	      | _ -> raise (Inconsistent ("points_to"))
+	  end
+  and rebuild_flow (c : cache) : constantset = 
+    if (List.mem c (!visited_caches) ) (* cyclic instantiations *)
+    then
+      begin
+	(* visited_caches := List.tl (!visited_caches); *) (* check *)
+	C.empty
+      end
+    else
+      begin
+	visited_caches :=  c :: (!visited_caches);
+	let result = ref (C.empty) in
+	  H.iter (fun _ -> fun(p,t) -> 
+		    match p with 
+		      | Pos -> () 
+		      | _ -> result := C.union (!result) (points_to_tau t)
+		 ) c;
+	  visited_caches := List.tl (!visited_caches);
+	  !result
+      end
+  in
+    if (!no_flow) then 
+      (U.deref lv.l).aliases
+    else 
+      points_to_tau (lv.contents)
+
+let points_to (lv : lvalue) : string list =
+  List.map snd (C.elements (points_to_int lv))
+
+let alias_query (a_progress : bool) (lv : lvalue list) : int * int = 
+  (0,0) (* todo *)
+(*
+  let a_count = ref 0 in
+  let ptsets = List.map points_to_int lv in
+  let total_sets = List.length ptsets in
+  let counted_sets = ref 0 in 
+  let record_alias s s' = 
+    if (C.is_empty (C.inter s s')) 
+    then ()
+    else (incr a_count)
+  in
+  let rec check_alias = function
+    | h :: t ->
+	begin
+	  List.iter (record_alias h) ptsets; 
+	  check_alias t 
+	end
+    | [] -> ()
+  in
+    check_alias ptsets;
+    !a_count
+*)
diff --git a/cil/src/ext/pta/steensgaard.mli b/cil/src/ext/pta/steensgaard.mli
new file mode 100644
index 00000000..f009e7e0
--- /dev/null
+++ b/cil/src/ext/pta/steensgaard.mli
@@ -0,0 +1,71 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(*                                                                     *)
+(* This file is currently unused by CIL.  It is included in the        *)
+(*   distribution for reference only.                                  *)
+(*                                                                     *)
+(*                                                                     *)
+(***********************************************************************)
+
+type lvalue
+type tau
+val debug : bool ref
+val debug_constraints : bool ref
+val print_constraints : bool ref
+val no_flow : bool ref
+val no_sub : bool ref
+val analyze_mono : bool ref
+val solve_online : bool ref
+val solve_constraints : unit -> unit
+val rvalue : lvalue -> tau
+val deref : tau -> lvalue
+val join : tau -> tau -> tau
+val join_inits : tau list -> tau
+val address : lvalue -> tau
+val instantiate : lvalue -> int -> lvalue
+val assign : lvalue -> tau -> unit
+val apply : tau -> tau list -> tau
+val make_function :  string -> lvalue list -> tau -> tau
+val make_lvalue : bool -> string -> lvalue
+val bottom : unit -> tau
+val return : tau -> tau -> unit
+val make_fresh : string -> tau
+val points_to : lvalue -> string list    
+val string_of_lvalue : lvalue -> string
+val global_lvalue : lvalue -> bool
+val alias_query : bool -> lvalue list -> int * int
diff --git a/cil/src/ext/pta/uref.ml b/cil/src/ext/pta/uref.ml
new file mode 100644
index 00000000..53f36400
--- /dev/null
+++ b/cil/src/ext/pta/uref.ml
@@ -0,0 +1,94 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+exception Bad_find
+
+type 'a urefC =
+    Ecr of 'a * int
+  | Link of 'a uref
+and 'a uref = 'a urefC ref
+
+let rec find p = 
+  match !p with
+    | Ecr _ -> p
+    | Link p' ->
+	let p'' = find p' 
+	in p := Link p''; p''
+
+let uref x = ref (Ecr(x,0))
+
+let equal (p,p') = (find p == find p')
+
+let deref p = 
+  match ! (find p) with 
+    | Ecr (x,_) -> x
+    | _ -> raise Bad_find
+
+let update (p,x) = 
+  let p' = find p 
+  in
+    match !p' with
+      | Ecr (_,rank) -> p' := Ecr(x,rank)
+      | _ -> raise Bad_find
+	  
+let unify f (p,q) = 
+  let p',q' = find p, find q in
+    match (!p',!q') with 
+      | (Ecr(px,pr),Ecr(qx,qr)) ->
+	let x = f(px,qx) in
+	  if (p' == q') then
+	    p' := Ecr(x,pr)
+	  else if pr == qr then
+	    (q' := Ecr(x,qr+1); p' := Link q')
+	  else if pr < qr then
+	    (q' := Ecr(x,qr); p' := Link q')
+	  else (* pr > qr *)
+	    (p' := Ecr(x,pr); q' := Link p')
+      | _ -> raise Bad_find
+	  
+let union (p,q) = 
+  let p',q' = find p, find q in
+    match (!p',!q') with 
+      | (Ecr(px,pr),Ecr(qx,qr)) ->
+	  if (p' == q') then 
+	    ()
+	  else if pr == qr then
+	    (q' := Ecr(qx, qr+1); p' := Link q')
+	  else if pr < qr then
+	    p' := Link q'
+	  else (* pr > qr *)
+	    q' := Link p'
+      | _ -> raise Bad_find
+	  
+
diff --git a/cil/src/ext/pta/uref.mli b/cil/src/ext/pta/uref.mli
new file mode 100644
index 00000000..1dee5036
--- /dev/null
+++ b/cil/src/ext/pta/uref.mli
@@ -0,0 +1,65 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  John Kodumal        <jkodumal@eecs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+type 'a uref
+  
+(** Union-find with union by rank and path compression 
+  
+  This is an implementation of Tarjan's union-find data structure using 
+  generics. The interface is analagous to standard references, with the
+  addition of a union operation which makes two references indistinguishable.
+  
+*)
+  
+val uref: 'a -> 'a uref 
+  (** Create a new uref *)
+  
+val equal: 'a uref * 'a uref -> bool
+  (** Test whether two urefs share the same equivalence class *)
+  
+val deref: 'a uref -> 'a
+  (** Extract the contents of this reference *)
+  
+val update: 'a uref * 'a -> unit
+  (** Update the value stored in this reference *)
+  
+val unify: ('a * 'a -> 'a) -> 'a uref * 'a uref -> unit
+  (** [unify f (p,q)] unifies references [p] and [q], making them 
+    indistinguishable. The contents of the reference are the result of
+    [f] *)
+    
+val union: 'a uref * 'a uref -> unit
+  (** [unify (p,q)] unifies references [p] and [q], making them
+    indistinguishable. The contents of the reference are the contents of
+    one of the first or second arguments (unspecified) *)