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

23 files changed, 5205 insertions, 0 deletions

diff --git a/cil/ocamlutil/Makefile.ocaml b/cil/ocamlutil/Makefile.ocaml
new file mode 100644
index 00000000..1d0673fa
--- /dev/null
+++ b/cil/ocamlutil/Makefile.ocaml
@@ -0,0 +1,395 @@
+# -*- Mode: makefile -*-
+# Copyright (c) 2001-2002, 
+#  George C. Necula    <necula@cs.berkeley.edu>
+#  Scott McPeak        <smcpeak@cs.berkeley.edu>
+#  Wes Weimer          <weimer@cs.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.
+
+  # Generic Makefile for Ocaml projects
+  # Written by necula@cs.berkeley.edu
+  # 
+  # Features: 
+  #   - keeps byproducts of building in a separate directory
+  #   - handles dependencies automatically
+  #   - user specifies just what modules go into a project and 
+  #     everything else is done automatically
+  #   - you can use one Makefile for several Ocaml projects
+  #   
+  # You must include this file in your Makefile. Before the include point 
+  # you must defined the following variables (which are glob al for all Ocaml 
+  # projects specified in one Makefile):
+  # 
+  # CAMLDIR    - the directory where to get the ocaml executables from. 
+  #              Must be empty (defaul) or end with a /
+  # OBJDIR     - the directory where to put all object files. This directory 
+  #              must exist (default obj)
+  # DEPENDDIR  - the directory where to put dependency files. This directory 
+  #              must exist.  (default obj/.depend)
+  # NATIVECAML - if set then will use the native compiler
+  # UNSAFE     - if set then will turn off safety checks (only with NATIVECAML)
+  # PROFILE    - if set then it will compile and link with "gprof" profiling
+  #              support (NATIVECAML mode only)
+  # ASSEMBLY   - if set then it will keep assembly files
+  # STATIC     - if set then it will compile and link statically
+  #              (NATIVECAML mode only)
+  # PREPROC    - the preprocessor command
+
+  # MODULES    - a list of all modules for all projects defined in the 
+  #              Makefile. Give only the basenames (no directory, 
+  #              no extension).  This is used to create the dependencies.
+  # SOURCEDIRS - a list of all directories containing sources for all 
+  #              projects defined in a Makefile. This is used to set vpath.
+  # MLLS       - a list of all .mll (ocamllex input) files for all 
+  #              projects defined in the Makefile. 
+  # MLYS       - a list of all .mly (ocamlyacc input) files for all 
+  #              projects defined in the Makefile. 
+  # ECHO       - if specifically set to nothing then it will print 
+  #              all of the commands issued. Set this in the command line
+  #              if you want to see what is going on.
+  #
+  # COMPILEFLAGS      - if defined, then it is passed as argument to ocamlc
+  #                     and ocamlopt
+  # LINKFLAGS         - if defined, then it is passed as argument to 
+  #                     ocamlc and ocamlopt, when linking (at start of 
+  #                     command line)
+  #
+  # CAML_CFLAGS   - flags used only for the compilation of C files.
+  #                 e.g. '-ccopt <gcc flag>'
+  #
+  #
+  # After you set all of the above you must do the following for EACH separate 
+  # executable that you want to build.
+  #
+  # Define the following:
+  # PROJECT_EXECUTABLE - the name of the executable you want to build. To take 
+  #                      advantage of the naming scheme that separates the 
+  #                      bytecode version and the native version, use the 
+  #                      $(EXE) variable which is defined to either .byte.exe 
+  #                      or .asm.exe. I typically put the executable in 
+  #                      $(OBJDIR) as well.
+  # PROJECT_MODULES    - the base names of the modules that make this 
+  #                      executable in the order in which they must be
+  #                      passed to the linker. Make sure that all of
+  #                      the names mentioned here are also mentioned in 
+  #                      MODULES.
+  # PROJECT_CMODULES   - same as modules but for the C modules. These
+  #                      do not need to be mentioned in MODULES. There must be
+  #                      no name clashes with MODULES
+  # PROJECT_LIBS       - the base names of the libraries that you 
+  #                      want to link in the executable.
+  #
+  #
+  # Then include Makefile.ocaml.build to generate a customized
+  # rule for making your executable.
+  #
+  # Example:
+  # 
+  # OBJDIR     = obj
+  # DEPENDDIR  = obj/.depend
+  # SOURCEDIRS = src src/special
+  # MLLS       = mylex 
+  # MLYS       = myparse
+  #
+  # MODULES    = mod11 mod12 mod21 modcommon
+  #
+  #  # Rules for project 1
+  # PROJECT_EXECUTABLE = $(OBJDIR)/proj1$(EXE)
+  # PROJECT_MODULES    = mod11 mod12 modcommon
+  # PROJECT_CMODULES   =  
+  # PROJEC_LIBS        = unix
+  # include Makefile.ocaml.build
+  #
+  #
+  #  # Rules for project 2 
+  # PROJECT_EXECUTABLE = $(OBJDIR)/proj2$(EXE)
+  # PROJECT_MODULES    = mod21 modcommon
+  # PROJECT_CMODULES   =  
+  # PROJEC_LIBS        = unix str
+  # include Makefile.ocaml.build
+
+
+CAMLLEX = ocamllex
+CAMLYACC= ocamlyacc -v
+CAMLDEP = ocamldep
+
+COMPILEFLAGS += -I $(OBJDIR)
+
+# sm: two styles for echoing compilation progress:
+#   style 1, by George:
+#     - print English descriptions of what's happening
+#     - set ECHO to "" to see *everything*
+#   style 2, by Scott:
+#     - do not print English descriptions
+#     - print every shell command that is executed which has a side effect,
+#       so that they could be pasted into a shell to reproduce manually
+#     - omit some of the details of dependency generation
+#
+# to be able to choose which style, several variables are used:
+#   @$(NARRATIVE)  - put this before English descriptions for style 1
+#   @$(COMMAND)    - put this before shell commands which are to be
+#                    printed for style 2; the command is *not* executed
+#   $(AT)          - put this before shell commands which are to be executed,
+#                    and also printed in style 2
+#   $(ECHO)        - use in place of '@' for things not printed in either style
+ifdef ECHOSTYLE_SCOTT
+  # 'true' silently consumes its arguments, whereas 'echo' prints them
+  NARRATIVE   := true           
+  COMMAND     := echo
+  AT          := 
+  ECHO        := @
+else
+  NARRATIVE   := echo
+  COMMAND     := true
+  # change these next two definitions to <empty> to echo everything,
+  # or leave as @ to suppress echoing
+  AT          := @
+  ECHO        := @
+endif
+
+ifdef PREPROC
+  COMPILEFLAGS += -pp "$(PREPROC)$"
+  DEPFLAGS += -pp "$(PREPROC)"
+endif
+
+COMPILEMSG=
+LINKMSG=
+
+ifdef WIN32
+OBJ             = obj
+else
+OBJ             = o
+endif
+EXE		= $(EXEEXT).exe
+
+
+export EXE
+
+ifdef NATIVECAML
+ ifdef PROFILE
+   COMPILEFLAGS   += -p
+   LINKFLAGS      += -p
+   COMPILEMSG     += (profile)
+   LINKMSG        += (profile)
+ endif
+ ifdef ASSEMBLY
+   COMPILEFLAGS   += -S
+ endif
+ ifdef STATIC
+   COMPILEFLAGS   += -ccopt -static
+   LINKFLAGS      += -ccopt -static
+ endif
+ #foo := $(shell echo "I am in NATIVECAML mode" >&2; echo whatever)
+ ifdef WIN32
+   COMPILEFLAGS    += -ccopt /Ox
+ else
+   COMPILEFLAGS    += -ccopt -O3
+ endif
+ CAMLC          = $(CAMLDIR)ocamlopt  $(COMPILEFLAGS)
+ CAMLLINK       = $(CAMLDIR)ocamlopt  $(LINKFLAGS)
+ CMO            = cmx
+ CMC            = opt.$(OBJ)  # compiled (and optimized) C
+ CMXA           = cmxa
+ EXEEXT         = .asm
+ MOVEAFTERCAMLC = cmi cmx $(OBJ)
+ COMPILETOWHAT  = native code
+ # sm: by adding -native in native mode, we prevent spurious
+ # dependencies on .cmo files which were causing lots of
+ # extra recompilation
+ CAMLDEP        = $(CAMLDIR)ocamldep -native
+else 
+ CMO            = cmo
+ CMXA           = cma
+ CMC            = $(OBJ)
+ EXEEXT         = .byte
+ MOVEAFTERCAMLC = cmi cmo
+ COMPILETOWHAT  = bytecode
+ ifdef WIN32
+   COMPILEFLAGS += -ccopt /Zi -ccopt /Od
+   LINKFLAGS    += -ccopt /Zi -ccopt /Od
+ else
+   COMPILEFLAGS += -g -ccopt -g
+   LINKFLAGS    += -g -ccopt -g
+ endif
+ CAMLC          = $(CAMLDIR)ocamlc -g $(COMPILEFLAGS)
+ CAMLLINK       = $(CAMLDIR)ocamlc -custom  $(LINKFLAGS)
+endif
+
+
+ifdef UNSAFE 
+ CAMLC          := $(CAMLC) -unsafe -noassert
+endif
+
+
+
+
+    # Allow searching for .ml and .mli
+vpath %.mll $(SOURCEDIRS)
+vpath %.mly $(SOURCEDIRS)
+vpath %.ml  $(SOURCEDIRS) $(OBJDIR)
+vpath %.mli $(SOURCEDIRS) $(OBJDIR)
+vpath %.c   $(SOURCEDIRS)
+
+
+#  Secondaries are intermediates that we don't want make to delete
+#  By giving the right names to secondary files we tell make where to make
+#  them if they are not already made. VERY USEFUL!!
+.SECONDARY : $(MLLS:%.mll=$(OBJDIR)/%.ml) $(MLYS:%.mly=$(OBJDIR)/%.ml) \
+             $(MLYS:%.mly=$(OBJDIR)/%.mli)
+
+             # Run the lexer generator
+             # Move the result to the OBJDIR directory
+             # If there is a .mli file in the same directory with .mll then
+             # copy it to OBJDIR (where the .ml) file will live.
+$(OBJDIR)/%.ml: %.mll
+	$(CAMLLEX) $<
+	$(AT)mv -f $(basename $<).ml $(OBJDIR)/
+	$(ECHO)if test -f $(basename $<).mli ;then \
+	  $(COMMAND) cp -f $(basename $<).mli $(OBJDIR)/; \
+	  cp -f $(basename $<).mli $(OBJDIR)/ \
+        ;fi
+
+             # Run the parser generator
+             # Move the result to the $(OBJDIR) directory.
+$(OBJDIR)/%.ml $(OBJDIR)/%.mli: %.mly
+	$(CAMLYACC) $(CAMLYACCFLAGS) $<
+	$(AT)mv -f $(basename $<).ml $(basename $<).mli $(OBJDIR)/
+
+         # Compile an MLI file. After compilation move the result to OBJDIR
+$(OBJDIR)/%.cmi: %.mli
+	@$(NARRATIVE) Compiling interface $<
+	$(AT)$(CAMLC) $(COMPILEFLAGS) -c $<
+	$(ECHO)if test $(OBJDIR) != $(<D) ;then \
+                   $(COMMAND) mv -f $(basename $<).cmi $(OBJDIR)/; \
+                   mv -f $(basename $<).cmi $(OBJDIR)/ \
+        ;fi
+
+         # Compile an ML file. After compilation we 
+         # copy to $(OBJDIR) the .cmi and the result of compilation.
+$(OBJDIR)/%.$(CMO): %.ml
+	@$(NARRATIVE) "Compiling           $< to $(COMPILETOWHAT) $(COMPILEMSG)"
+#	$(ECHO)#if test $(OBJDIR) != $(<D) -a -f $(OBJDIR)/$(basename $(<F)).cmi ;then \
+#           $(COMMAND) mv -f $(OBJDIR)/$(basename $(<F)).cmi $(<D); \
+#           mv -f $(OBJDIR)/$(basename $(<F)).cmi $(<D); \
+#        fi
+	@$(COMMAND) $(CAMLC) $(COMPILEFLAGS) -c $<
+	$(ECHO)$(CAMLC) $(COMPILEFLAGS) -c $< ; res=$$?; \
+	   if test $(OBJDIR) != $(<D) ;then \
+              for ext in $(MOVEAFTERCAMLC); do \
+                if test -f $(basename $<).$$ext ;then \
+                  $(COMMAND) mv -f $(basename $<).$$ext $(OBJDIR)/; \
+                  mv -f $(basename $<).$$ext $(OBJDIR)/; \
+                fi; \
+              done; \
+           fi; exit $$res
+
+             # Compile C files
+             # They appear to be left in the current directory as .o files
+$(OBJDIR)/%.$(CMC): %.c
+	@$(NARRATIVE) "Compiling C file $< $(COMPILEMSG)"
+	$(AT)$(CAMLC) $(COMPILEFLAGS) $(CAML_CFLAGS) -c $< -o $@
+	$(AT)mv -f $(basename $(notdir $<)).$(OBJ) $@
+
+              # Special rule for profile.c
+CAMLC_NOPROF=$(subst -p,,$(CAMLC))
+$(OBJDIR)/profile.$(CMC): profile.c
+	@$(NARRATIVE) "Compiling C file $<"
+	$(AT)$(CAMLC_NOPROF) $(COMPILEFLAGS) $(CAML_CFLAGS) -c $< -o $@
+	$(AT)mv -f $(basename $(notdir $<)).$(OBJ) $@
+
+
+#	Phonies should be "remade" even if someone mistakenly creates them
+.PHONY: cleancaml
+cleancaml:
+	-rm -f $(OBJDIR)/*.cmi
+	-rm -f $(OBJDIR)/*.cmo
+	-rm -f $(OBJDIR)/*.cmx
+	-rm -f $(OBJDIR)/*.cma
+	-rm -f $(OBJDIR)/*.cmxa
+	-rm -f $(OBJDIR)/*.exe
+	-rm -f $(OBJDIR)/*.obj
+	-rm -f $(OBJDIR)/*.o
+	-rm -f $(OBJDIR)/*.obj
+	-rm -f $(OBJDIR)/*.o
+	-rm -f $(OBJDIR)/*.lib
+	-rm -f $(OBJDIR)/*.a
+	-rm -f $(OBJDIR)/*.mli
+	-rm -f $(OBJDIR)/*.ml
+	-rm -f $(DEPENDDIR)/*.d $(DEPENDDIR)/*.di
+	-rm -f $(MLLS:%.mll=$(OBJDIR)/%.ml) \
+               $(MLLS:%.mll=$(OBJDIR)/%.mli) \
+               $(MLYS:%.mly=$(OBJDIR)/%.ml) \
+               $(MLYS:%.mly=$(OBJDIR)/%.mli)
+
+
+# Automatic dependency generation (see GNU info for details)
+#
+# Each .ml file has a .d (dependency file) which is automatically
+# generated and included by the rules below.  The perl script replaces
+# directory paths with $(OBJDIR)/
+#
+# Dependencies for .mli files reside in corresponding .di files.
+#
+
+# Replace the directories in the dependency rules with $(OBJDIR)/, since 
+# we'll move .cmo/.cmx files there.
+# 1. Strip any text followed by / or \.  The / case even strips slashes that
+#    are preceded by whitespace, to account for unix absolute paths.
+#    The \ case does not strip slashes that come immediately after whitespace,
+#    to preserve the trailing \ at the end of Makefile rules.
+# 2. Replace these directory names by '$(OBJDIR)/'
+FIXDEPEND:=perl -e 'while(<>) { s%[^/\\ :]*/% %g; s%[^/\\ :]+\\% %g; s%([-a-zA-Z0-9+-.:/\/_]+)%\$$(OBJDIR)/$$1%g; print $$_;}'
+# FIXDEPEND:=cat
+
+DEPINCLUDES= -I $(OBJDIR) $(SOURCEDIRS:%=-I %)
+$(DEPENDDIR)/%.d: %.ml
+	@$(NARRATIVE) Generating dependency information for $<
+	@$(COMMAND) $(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $<
+	$(ECHO)$(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< | $(FIXDEPEND) > $@
+
+$(DEPENDDIR)/%.di: %.mli
+	@$(NARRATIVE) Generating dependency information for $<
+	@$(COMMAND) $(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $<
+	$(ECHO)$(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< | $(FIXDEPEND) > $@
+
+# sm: it turns out there's a variable which lists all the goals
+# specified on the command line; I'll use this to set CLEANING
+# (which is not set anywhere else, currently)
+ifeq ($(MAKECMDGOALS),clean)
+  #$(warning "Skipping dependency rules because we're cleaning")
+  CLEANING := 1
+endif
+
+ifndef CLEANING
+-include $(MODULES:%=$(DEPENDDIR)/%.d)
+-include $(MODULES:%=$(DEPENDDIR)/%.di)
+endif
+
+listmodules: 
+	@echo $(MODULES)
diff --git a/cil/ocamlutil/Makefile.ocaml.build b/cil/ocamlutil/Makefile.ocaml.build
new file mode 100644
index 00000000..5271e461
--- /dev/null
+++ b/cil/ocamlutil/Makefile.ocaml.build
@@ -0,0 +1,50 @@
+# -*- Mode: makefile -*-
+# Copyright (c) 2001-2002, 
+#  George C. Necula    <necula@cs.berkeley.edu>
+#  Scott McPeak        <smcpeak@cs.berkeley.edu>
+#  Wes Weimer          <weimer@cs.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.
+
+  # Auxiliary Makefile for building Ocaml project. See the documentation in
+  # the associated Makefile.ocaml for how to use this file.
+  # Written by necula@cs.berkeley.edu
+  # 
+$(PROJECT_EXECUTABLE) : $(PROJECT_MODULES:%=$(OBJDIR)/%.$(CMO)) \
+                        $(PROJECT_CMODULES:%=$(OBJDIR)/%.$(CMC))
+	@$(NARRATIVE) "Linking $(COMPILETOWHAT) $@ $(LINKMSG)"
+	$(AT)$(CAMLLINK) -verbose -o $@ \
+                    $(PROJECT_LIBS:%=%.$(CMXA)) \
+                    $(PROJECT_LIBS:%=-cclib -l%) \
+                    $^
+
+
+
+
+
diff --git a/cil/ocamlutil/alpha.ml b/cil/ocamlutil/alpha.ml
new file mode 100755
index 00000000..6a1ea017
--- /dev/null
+++ b/cil/ocamlutil/alpha.ml
@@ -0,0 +1,156 @@
+module H = Hashtbl
+module E = Errormsg
+open Pretty
+
+let debugAlpha (prefix: string) = false
+(*** Alpha conversion ***)
+let alphaSeparator = "___"
+let alphaSeparatorLen = String.length alphaSeparator
+
+(** For each prefix we remember the next integer suffix to use and the list 
+ * of suffixes, each with some data assciated with the newAlphaName that 
+ * created the suffix. *)
+type 'a alphaTableData = int * (string * 'a) list
+
+type 'a undoAlphaElement = 
+    AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The 
+                                             * reference that was changed and 
+                                             * the old suffix *)
+  | AlphaAddedSuffix of string          (* We added this new entry to the 
+                                         * table *)
+
+(* Create a new name based on a given name. The new name is formed from a 
+ * prefix (obtained from the given name by stripping a suffix consisting of 
+ * the alphaSeparator followed by only digits), followed by alphaSeparator 
+ * and then by a positive integer suffix. The first argument is a table 
+ * mapping name prefixes to the largest suffix used so far for that 
+ * prefix. The largest suffix is one when only the version without suffix has 
+ * been used. *)
+let rec newAlphaName ~(alphaTable: (string, 'a alphaTableData ref) H.t)
+                     ~(undolist: 'a undoAlphaElement list ref option)
+                     ~(lookupname: string) 
+                     ~(data: 'a) : string * 'a = 
+  alphaWorker ~alphaTable:alphaTable ~undolist:undolist 
+              ~lookupname:lookupname ~data:data true
+  
+
+(** Just register the name so that we will not use in the future *)
+and registerAlphaName ~(alphaTable: (string, 'a alphaTableData ref) H.t)
+                      ~(undolist: 'a undoAlphaElement list ref option)
+                      ~(lookupname: string) 
+                      ~(data: 'a) : unit = 
+  ignore (alphaWorker ~alphaTable:alphaTable ~undolist:undolist 
+                      ~lookupname:lookupname ~data:data false)
+
+
+and alphaWorker      ~(alphaTable: (string, 'a alphaTableData ref) H.t)
+                     ~(undolist: 'a undoAlphaElement list ref option)
+                     ~(lookupname: string) ~(data:'a)
+                     (make_new: bool) : string * 'a = 
+  let prefix, suffix, (numsuffix: int) = splitNameForAlpha ~lookupname in
+  if debugAlpha prefix then
+    ignore (E.log "Alpha worker: prefix=%s suffix=%s (%d) create=%b. " 
+              prefix suffix numsuffix make_new);
+  let newname, (olddata: 'a) = 
+    try
+      let rc = H.find alphaTable prefix in
+      let max, suffixes = !rc in 
+      (* We have seen this prefix *)
+      if debugAlpha prefix then
+        ignore (E.log " Old max %d. Old suffixes: @[%a@]" max
+                  (docList 
+                     (fun (s, l) -> dprintf "%s" (* d_loc l *) s)) suffixes);
+      (* Save the undo info *)
+      (match undolist with 
+        Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
+      | _ -> ());
+
+      let newmax, newsuffix, (olddata: 'a), newsuffixes = 
+        if numsuffix > max then begin 
+          (* Clearly we have not seen it *)
+          numsuffix, suffix, data,
+          (suffix, data) :: suffixes 
+        end else begin 
+          match List.filter (fun (n, _) -> n = suffix) suffixes with 
+            [] -> (* Not found *)
+              max, suffix, data, (suffix, data) :: suffixes
+          | [(_, l) ] -> 
+              (* We have seen this exact suffix before *)
+              if make_new then 
+                let newsuffix = alphaSeparator ^ (string_of_int (max + 1)) in
+                max + 1, newsuffix, l, (newsuffix, data) :: suffixes
+              else
+                max, suffix, data, suffixes
+          |  _ -> E.s (E.bug "Cil.alphaWorker")
+        end
+      in
+      rc := (newmax, newsuffixes);
+      prefix ^ newsuffix, olddata
+    with Not_found -> begin (* First variable with this prefix *)
+      (match undolist with 
+        Some l -> l := AlphaAddedSuffix prefix :: !l
+      | _ -> ());
+      H.add alphaTable prefix (ref (numsuffix, [ (suffix, data) ]));
+      if debugAlpha prefix then ignore (E.log " First seen. ");
+      lookupname, data  (* Return the original name *)
+    end
+  in
+  if debugAlpha prefix then
+    ignore (E.log " Res=: %s \n" newname (* d_loc oldloc *));
+  newname, olddata
+
+(* Strip the suffix. Return the prefix, the suffix (including the separator 
+ * and the numeric value, possibly empty), and the 
+ * numeric value of the suffix (possibly -1 if missing) *) 
+and splitNameForAlpha ~(lookupname: string) : (string * string * int) = 
+  let len = String.length lookupname in
+  (* Search backward for the numeric suffix. Return the first digit of the 
+   * suffix. Returns len if no numeric suffix *)
+  let rec skipSuffix (i: int) = 
+    if i = -1 then -1 else 
+    let c = Char.code (String.get lookupname i) - Char.code '0' in
+    if c >= 0 && c <= 9 then 
+      skipSuffix (i - 1)
+    else (i + 1)
+  in
+  let startSuffix = skipSuffix (len - 1) in
+
+  if startSuffix >= len (* No digits at all at the end *) ||
+     startSuffix <= alphaSeparatorLen     (* Not enough room for a prefix and 
+                                           * the separator before suffix *) ||
+     (* Suffix starts with a 0 and has more characters after that *) 
+     (startSuffix < len - 1 && String.get lookupname startSuffix = '0')  ||
+     alphaSeparator <> String.sub lookupname 
+                                 (startSuffix - alphaSeparatorLen)  
+                                 alphaSeparatorLen 
+  then
+    (lookupname, "", -1)  (* No valid suffix in the name *)
+  else
+    (String.sub lookupname 0 (startSuffix - alphaSeparatorLen), 
+     String.sub lookupname (startSuffix - alphaSeparatorLen) 
+                           (len - startSuffix + alphaSeparatorLen),
+     int_of_string (String.sub lookupname startSuffix (len - startSuffix)))
+    
+
+let getAlphaPrefix ~(lookupname:string) : string = 
+  let p, _, _ = splitNameForAlpha ~lookupname:lookupname in
+  p
+      
+(* Undoes the changes as specified by the undolist *)
+let undoAlphaChanges ~(alphaTable: (string, 'a alphaTableData ref) H.t) 
+                     ~(undolist: 'a undoAlphaElement list) = 
+  List.iter
+    (function 
+        AlphaChangedSuffix (where, old) -> 
+          where := old
+      | AlphaAddedSuffix name -> 
+          if debugAlpha name then 
+            ignore (E.log "Removing %s from alpha table\n" name);
+          H.remove alphaTable name)
+    undolist
+
+let docAlphaTable () (alphaTable: (string, 'a alphaTableData ref) H.t) = 
+  let acc : (string * (int * (string * 'a) list)) list ref = ref [] in
+  H.iter (fun k d -> acc := (k, !d) :: !acc) alphaTable;
+  docList ~sep:line (fun (k, (d, _)) -> dprintf "  %s -> %d" k d) () !acc
+
diff --git a/cil/ocamlutil/alpha.mli b/cil/ocamlutil/alpha.mli
new file mode 100755
index 00000000..e1e430dc
--- /dev/null
+++ b/cil/ocamlutil/alpha.mli
@@ -0,0 +1,50 @@
+(** {b ALPHA conversion} *)
+
+(** This is the type of the elements that are recorded by the alpha 
+ * conversion functions in order to be able to undo changes to the tables 
+ * they modify. Useful for implementing 
+ * scoping *)
+type 'a undoAlphaElement
+
+(** This is the type of the elements of the alpha renaming table. These 
+ * elements can carry some data associated with each occurrence of the name. *)
+type 'a alphaTableData
+
+
+(** Create a new name based on a given name. The new name is formed from a 
+ * prefix (obtained from the given name by stripping a suffix consisting of _ 
+ * followed by only digits), followed by a special separator and then by a 
+ * positive integer suffix. The first argument is a table mapping name 
+ * prefixes to some data that specifies what suffixes have been used and how 
+ * to create the new one. This function updates the table with the new 
+ * largest suffix generated. The "undolist" argument, when present, will be 
+ * used by the function to record information that can be used by 
+ * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo 
+ * information will be in reverse order in which the action occurred. Returns 
+ * the new name and, if different from the lookupname, the location of the 
+ * previous occurrence. This function knows about the location implicitly 
+ * from the {!Cil.currentLoc}. *)
+val newAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t ->
+                  undolist: 'a undoAlphaElement list ref option ->
+                  lookupname:string -> data:'a -> string * 'a
+
+
+(** Register a name with an alpha conversion table to ensure that when later 
+  * we call newAlphaName we do not end up generating this one *)
+val registerAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t -> 
+                       undolist: 'a undoAlphaElement list ref option ->
+                       lookupname:string -> data:'a -> unit
+
+(** Split the name in preparation for newAlphaName. The prefix returned is 
+    used to index into the hashtable. The next result value is a separator 
+    (either empty or the separator chosen to separate the original name from 
+     the index)  *)
+val docAlphaTable: unit -> 
+                  (string, 'a alphaTableData ref) Hashtbl.t -> Pretty.doc
+
+
+val getAlphaPrefix: lookupname:string -> string
+
+(** Undo the changes to a table *)
+val undoAlphaChanges: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t -> 
+                      undolist:'a undoAlphaElement list -> unit
diff --git a/cil/ocamlutil/clist.ml b/cil/ocamlutil/clist.ml
new file mode 100644
index 00000000..80f0fd64
--- /dev/null
+++ b/cil/ocamlutil/clist.ml
@@ -0,0 +1,183 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+open Pretty
+
+
+(* We often need to concatenate sequences and using lists for this purpose is 
+ * expensive. So we define a kind of "concatenable lists" that are easier to 
+ * concatenate *)
+type 'a clist = 
+  | CList of 'a list             (* This is the only representation for empty 
+                                  * *)
+  | CConsL of 'a * 'a clist
+  | CConsR of 'a clist * 'a 
+  | CSeq  of 'a clist * 'a clist (* We concatenate only two of them at this 
+                                  * time. Neither is CEmpty. To be sure 
+                                  * always use append to make these  *)
+
+let rec listifyOnto (tail: 'a list) = function
+    CList l -> l @ tail
+  | CConsL (x, l) -> x :: listifyOnto tail l
+  | CConsR (l, x) -> listifyOnto (x :: tail) l
+  | CSeq (l1, l2) -> listifyOnto (listifyOnto tail l2) l1
+        
+let toList l = listifyOnto [] l
+let fromList l = CList l
+    
+    
+let single x = CList [x]
+let empty = CList []
+    
+let checkBeforeAppend  (l1: 'a clist) (l2: 'a clist) : bool =
+  l1 != l2 || l1 = (CList [])
+
+let append l1 l2 =
+  if l1 = CList [] then l2 else
+  if l2 = CList [] then l1 else
+  begin
+    if l1 == l2 then 
+      raise (Failure "You should not use Clist.append to double a list");
+    CSeq (l1, l2)
+  end
+
+let rec length (acc: int) = function
+    CList l -> acc + (List.length l)
+  | CConsL (x, l) -> length (acc + 1) l
+  | CConsR (l, _) -> length (acc + 1) l
+  | CSeq (l1, l2) -> length (length acc l1) l2
+let length l = length 0 l  (* The external version *)
+    
+let map (f: 'a -> 'b) (l: 'a clist) : 'b clist = 
+  let rec loop = function
+      CList l -> CList (List.map f l)
+    | CConsL (x, l) -> let x' = f x in CConsL (x', loop l)
+    | CConsR (l, x) -> let l' = loop l in CConsR (l', f x)
+    | CSeq (l1, l2) -> let l1' = loop l1 in CSeq (l1', loop l2)
+  in
+  loop l
+    
+  
+let fold_left (f: 'acc -> 'a -> 'acc) (start: 'acc) (l: 'a clist) = 
+  let rec loop (start: 'acc) = function
+      CList l -> List.fold_left f start l
+    | CConsL (x, l) -> loop (f start x) l
+    | CConsR (l, x) -> let res = loop start l in f res x
+    | CSeq (l1, l2) -> 
+        let res1 = loop start l1 in
+        loop res1 l2
+  in
+  loop start l
+    
+let iter (f: 'a -> unit) (l: 'a clist) : unit = 
+  let rec loop = function
+      CList l -> List.iter f l
+    | CConsL (x, l) -> f x; loop l
+    | CConsR (l, x) -> loop l; f x
+    | CSeq (l1, l2) -> loop l1; loop l2
+  in
+  loop l
+    
+        
+let rec rev (revelem: 'a -> 'a) = function
+    CList l -> 
+      let rec revonto (tail: 'a list) = function
+          [] -> tail
+        | x :: rest -> revonto (revelem x :: tail) rest
+      in
+      CList (revonto [] l)
+
+  | CConsL (x, l) -> CConsR (rev revelem l, x)
+  | CConsR (l, x) -> CConsL (x, rev revelem l)
+  | CSeq (l1, l2) -> CSeq (rev revelem l2, rev revelem l1)
+
+
+let docCList (sep: doc) (doone: 'a -> doc) () (dl: 'a clist) = 
+  fold_left 
+    (fun (acc: doc) (elem: 'a) -> 
+      let elemd = doone elem in
+      if acc == nil then elemd else acc ++ sep ++ elemd)
+    nil
+    dl
+
+    
+(* let debugCheck (lst: 'a clist) : unit =*)
+(*   (* use a hashtable to store values encountered *)*)
+(*   let tbl : 'a bool H.t = (H.create 13) in*)
+
+(*   letrec recurse (node: 'a clist) =*)
+(*     (* have we seen*)*)
+
+(*     match node with*)
+(*     | CList*)
+
+
+(* --------------- testing ----------------- *)
+type boxedInt =
+  | BI of int
+  | SomethingElse
+
+let d_boxedInt () b =
+  match b with
+  | BI(i) -> (dprintf "%d" i)
+  | SomethingElse -> (text "somethingElse")
+
+
+(* sm: some simple tests of CLists 
+let testCList () : unit =
+begin
+  (trace "sm" (dprintf "in testCList\n"));
+
+  let clist1 = (fromList [BI(1); BI(2); BI(3)]) in
+  (trace "sm" (dprintf "length of clist1 is %d\n"
+                       (length clist1) ));
+
+  let flattened = (toList clist1) in
+  (trace "sm" (dprintf "flattened: %a\n"
+                       (docList ~sep:(chr ',' ++ break) (d_boxedInt ()))
+                       flattened));
+
+
+end
+1) in
+  (trace "sm" (dprintf "flattened: %a\n"
+                       (docList ~sep:(chr ',' ++ break) (d_boxedInt ()))
+                       flattened));
+
+
+end
+*)
diff --git a/cil/ocamlutil/clist.mli b/cil/ocamlutil/clist.mli
new file mode 100644
index 00000000..c0378a60
--- /dev/null
+++ b/cil/ocamlutil/clist.mli
@@ -0,0 +1,97 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+(** Utilities for managing "concatenable lists" (clists). We often need to
+    concatenate sequences, and using lists for this purpose is expensive. This
+    module provides routines to manage such lists more efficiently. In this
+    model, we never do cons or append explicitly. Instead we maintain
+    the elements of the list in a special data structure. Routines are provided
+    to convert to/from ordinary lists, and carry out common list operations.*)
+
+(** The clist datatype. A clist can be an ordinary list, or a clist preceded 
+    or followed by an element, or two clists implicitly appended together*)
+type 'a clist = 
+  | CList of 'a list             (** The only representation for the empty 
+                                     list. Try to use sparingly.  *)
+  | CConsL of 'a * 'a clist      (** Do not use this a lot because scanning 
+                                   * it is not tail recursive *)
+  | CConsR of 'a clist * 'a 
+  | CSeq of 'a clist * 'a clist (** We concatenate only two of them at this
+                                    time. Neither is the empty clist. To be
+                                    sure always use append to make these *)
+
+
+(** Convert a clist to an ordinary list *)
+val toList: 'a clist -> 'a list
+
+(** Convert an ordinary list to a clist *)  
+val fromList: 'a list -> 'a clist 
+
+(** Create a clist containing one element *)
+val single: 'a -> 'a clist        
+
+(** The empty clist *)
+val empty: 'a clist               
+
+
+(** Append two clists *)
+val append: 'a clist -> 'a clist -> 'a clist 
+                 
+(** A useful check to assert before an append. It checks that the two lists 
+ * are not identically the same (Except if they are both empty) *)
+val checkBeforeAppend: 'a clist -> 'a clist -> bool
+
+(** Find the length of a clist *)
+val length: 'a clist -> int   
+
+(** Map a function over a clist. Returns another clist *)
+val map: ('a -> 'b) -> 'a clist -> 'b clist 
+
+
+(** A version of fold_left that works on clists *)
+val fold_left: ('acc -> 'a -> 'acc) -> 'acc -> 'a clist -> 'acc
+
+(** A version of iter that works on clists *)
+val iter: ('a -> unit) -> 'a clist -> unit
+
+(** Reverse a clist. The first function reverses an element.  *)
+val rev: ('a -> 'a) -> 'a clist -> 'a clist
+
+(** A document for printing a clist (similar to [docList]) *)
+val docCList: 
+    Pretty.doc -> ('a -> Pretty.doc) -> unit -> 'a clist -> Pretty.doc
+ 
diff --git a/cil/ocamlutil/errormsg.ml b/cil/ocamlutil/errormsg.ml
new file mode 100644
index 00000000..07e935d4
--- /dev/null
+++ b/cil/ocamlutil/errormsg.ml
@@ -0,0 +1,337 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+open Pretty
+
+
+
+let debugFlag  = ref false              (* If set then print debugging info *)
+let verboseFlag = ref false
+
+(**** Error reporting ****)  
+exception Error
+let s (d : 'a) = raise Error
+
+let hadErrors = ref false
+
+let errorContext = ref []
+let pushContext f = errorContext := f :: (!errorContext)
+let popContext () = 
+  match !errorContext with 
+    _ :: t -> errorContext := t
+  | [] -> s (eprintf "Bug: cannot pop error context")
+
+
+let withContext ctx f x = 
+  pushContext ctx;
+  try
+    let res = f x in
+    popContext ();
+    res
+  with e -> begin
+    popContext ();
+    raise e
+  end
+  
+                                        (* Make sure that showContext calls 
+                                         * each f with its appropriate 
+                                         * errorContext as it was when it was 
+                                         * pushed *)
+let showContext () = 
+  let rec loop = function
+      [] -> ()
+    | f :: rest -> (errorContext := rest; (* Just in case f raises an error *)
+                    ignore (eprintf "  Context : %t@!" f);
+                    loop rest)
+  in
+  let old = !errorContext in
+  try 
+    loop old;
+    errorContext := old
+  with e -> begin
+    errorContext := old;
+    raise e
+  end
+
+let contextMessage (name: string) (d: doc) = 
+  ignore (eprintf "@!%s: %a@!" name insert d);
+  showContext ()
+
+let warnFlag = ref false
+
+let logChannel : out_channel ref = ref stderr
+
+
+let bug (fmt : ('a,unit,doc,unit) format4) : 'a = 
+  let f d =  
+    hadErrors := true; contextMessage "Bug" d; 
+    flush !logChannel
+  in
+  Pretty.gprintf f fmt
+
+let error (fmt : ('a,unit,doc,unit) format4) : 'a = 
+  let f d = hadErrors := true; contextMessage "Error" d; 
+    flush !logChannel
+  in
+  Pretty.gprintf f fmt
+
+let unimp (fmt : ('a,unit,doc,unit) format4) : 'a = 
+  let f d = hadErrors := true; contextMessage "Unimplemented" d; 
+    flush !logChannel
+  in
+  Pretty.gprintf f fmt
+
+let warn (fmt : ('a,unit,doc,unit) format4) : 'a = 
+  let f d = contextMessage "Warning" d; flush !logChannel in
+  Pretty.gprintf f fmt
+
+let warnOpt (fmt : ('a,unit,doc,unit) format4) : 'a = 
+    let f d = 
+      if !warnFlag then contextMessage "Warning" d; 
+      flush !logChannel in
+    Pretty.gprintf f fmt
+
+
+let log (fmt : ('a,unit,doc,unit) format4) : 'a = 
+  let f d = fprint !logChannel 80 d; flush !logChannel in
+  Pretty.gprintf f fmt
+
+let logg (fmt : ('a,unit,doc,unit) format4) : 'a =
+  let f d = fprint !logChannel 10000000 d; flush !logChannel in
+  Pretty.gprintf f fmt
+
+let null (fmt : ('a,unit,doc,unit) format4) : 'a =
+  let f d = () in
+  Pretty.gprintf f fmt
+
+
+let theLexbuf = ref (Lexing.from_string "")
+
+let fail format = Pretty.gprintf (fun x -> Pretty.fprint stderr 80 x; 
+                                           raise (Failure "")) format
+
+
+
+(***** Handling parsing errors ********)
+type parseinfo =
+    { mutable  linenum: int      ; (* Current line *)
+      mutable  linestart: int    ; (* The position in the buffer where the 
+                                    * current line starts *)
+      mutable fileName : string   ; (* Current file *)
+      mutable hfile   : string   ; (* High-level file *)
+      mutable hline   : int;       (* High-level line *)
+      lexbuf          : Lexing.lexbuf;
+      inchan          : in_channel option; (* None, if from a string *)
+      mutable   num_errors : int;  (* Errors so far *)
+    }
+      
+let dummyinfo = 
+    { linenum   = 1;
+      linestart = 0;
+      fileName  = "" ;
+      lexbuf    = Lexing.from_string "";
+      inchan    = None;
+      hfile     = "";
+      hline     = 0;
+      num_errors = 0;
+    }
+
+let current = ref dummyinfo
+
+let setHLine (l: int) : unit =
+    !current.hline <- l
+let setHFile (f: string) : unit =
+    !current.hfile <- f
+    
+let rem_quotes str = String.sub str 1 ((String.length str) - 2)
+
+(* Change \ into / in file names. To avoid complications with escapes *)
+let cleanFileName str = 
+  let str1 = 
+    if str <> "" && String.get str 0 = '"' (* '"' ( *) 
+    then rem_quotes str else str in
+  let l = String.length str1 in
+  let rec loop (copyto: int) (i: int) = 
+    if i >= l then 
+      String.sub str1 0 copyto
+     else 
+       let c = String.get str1 i in
+       if c <> '\\' then begin
+          String.set str1 copyto c; loop (copyto + 1) (i + 1)
+       end else begin
+          String.set str1 copyto '/';
+          if i < l - 2 && String.get str1 (i + 1) = '\\' then
+              loop (copyto + 1) (i + 2)
+          else 
+              loop (copyto + 1) (i + 1)
+       end
+  in
+  loop 0 0
+
+let readingFromStdin = ref false
+
+let startParsing ?(useBasename=true) (fname: string) = 
+  (* We only support one open file at a time *)
+  if !current != dummyinfo then begin
+     s (error "Errormsg.startParsing supports only one open file: You want to open %s and %s is still open\n" fname !current.fileName); 
+  end; 
+  let inchan = 
+    try if fname = "-" then begin 
+           readingFromStdin := true;
+           stdin 
+        end else begin
+           readingFromStdin := false;
+           open_in fname 
+        end
+    with e -> s (error "Cannot find input file %s (exception %s" 
+                    fname (Printexc.to_string e)) in
+  let lexbuf = Lexing.from_channel inchan in
+  let i = 
+    { linenum = 1; linestart = 0; 
+      fileName = 
+        cleanFileName (if useBasename then Filename.basename fname else fname);
+      lexbuf = lexbuf; inchan = Some inchan;
+      hfile = ""; hline = 0;
+      num_errors = 0 } in
+
+  current := i;
+  lexbuf
+
+let startParsingFromString ?(file="<string>") ?(line=1) (str: string) = 
+  let lexbuf = Lexing.from_string str in
+  let i = 
+    { linenum = line; linestart = line - 1;
+      fileName = file;
+      hfile = ""; hline = 0;
+      lexbuf = lexbuf; 
+      inchan = None;
+      num_errors = 0 }
+  in
+  current := i;
+  lexbuf
+
+let finishParsing () = 
+  let i = !current in
+  (match i.inchan with Some c -> close_in c | _ -> ());
+  current := dummyinfo
+
+
+(* Call this function to announce a new line *)
+let newline () = 
+  let i = !current in
+  i.linenum <- 1 + i.linenum;
+  i.linestart <- Lexing.lexeme_start i.lexbuf
+
+let newHline () = 
+  let i = !current in
+  i.hline <- 1 + i.hline
+
+let setCurrentLine (i: int) = 
+  !current.linenum <- i
+
+let setCurrentFile (n: string) = 
+  !current.fileName <- cleanFileName n
+
+
+let max_errors = 20  (* Stop after 20 errors *)
+
+let parse_error (msg: string) : 'a =
+  (* Sometimes the Ocaml parser raises errors in symbol_start and symbol_end *)
+  let token_start, token_end = 
+    try Parsing.symbol_start (), Parsing.symbol_end ()
+    with e -> begin 
+      ignore (warn "Parsing raised %s\n" (Printexc.to_string e));
+      0, 0
+    end
+  in
+  let i = !current in
+  let adjStart = 
+    if token_start < i.linestart then 0 else token_start - i.linestart in
+  let adjEnd = 
+    if token_end < i.linestart then 0 else token_end - i.linestart in
+  output_string 
+    stderr
+    (i.fileName ^ "[" ^ (string_of_int i.linenum) ^ ":" 
+                        ^ (string_of_int adjStart) ^ "-" 
+                        ^ (string_of_int adjEnd) 
+                  ^ "]"
+     ^ " : " ^ msg);
+  output_string stderr "\n";
+  flush stderr ;
+  i.num_errors <- i.num_errors + 1;
+  if i.num_errors > max_errors then begin
+    output_string stderr "Too many errors. Aborting.\n" ;
+    exit 1 
+  end;
+  hadErrors := true;
+  raise Parsing.Parse_error
+
+
+
+
+(* More parsing support functions: line, file, char count *)
+let getPosition () : int * string * int = 
+  let i = !current in 
+  i.linenum, i.fileName, Lexing.lexeme_start i.lexbuf
+
+
+let getHPosition () = 
+  !current.hline, !current.hfile
+
+(** Type for source-file locations *)
+type location = 
+    { file: string; (** The file name *)
+      line: int;    (** The line number *)
+      hfile: string; (** The high-level file name, or "" if not present *)
+      hline: int;    (** The high-level line number, or 0 if not present *)
+    } 
+
+let d_loc () l = 
+  text (l.file ^ ":" ^ string_of_int l.line)
+    
+let d_hloc () (l: location) = 
+  dprintf "%s:%d%a" l.file l.line
+    insert (if l.hline > 0 then dprintf " (%s:%d)" l.hfile l.hline else nil)
+
+let locUnknown = { file = ""; hfile = ""; line = -1; hline = -1 }
+
+let getLocation () = 
+  let hl, hf = getHPosition () in
+  let l, f, c = getPosition () in
+  { hfile = hf; hline = hl;
+    file = f; line = l } 
+
diff --git a/cil/ocamlutil/errormsg.mli b/cil/ocamlutil/errormsg.mli
new file mode 100644
index 00000000..8d9c6979
--- /dev/null
+++ b/cil/ocamlutil/errormsg.mli
@@ -0,0 +1,164 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+(** Utility functions for error-reporting *)
+
+(** A channel for printing log messages *)
+val logChannel : out_channel ref
+
+(** If set then print debugging info *)
+val debugFlag  : bool ref               
+
+val verboseFlag : bool ref
+
+
+(** Set to true if you want to see all warnings. *)
+val warnFlag: bool ref
+
+(** Error reporting functions raise this exception *)
+exception Error
+
+
+   (* Error reporting. All of these functions take same arguments as a 
+    * Pretty.eprintf. They set the hadErrors flag, but do not raise an 
+    * exception. Their return type is unit.
+    *)
+
+(** Prints an error message of the form [Error: ...]. 
+    Use in conjunction with s, for example: [E.s (E.error ... )]. *)
+val error:         ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Similar to [error] except that its output has the form [Bug: ...] *)
+val bug:           ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Similar to [error] except that its output has the form [Unimplemented: ...] *)
+val unimp:         ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Stop the execution by raising an Error. *)
+val s:             'a -> 'b
+
+(** This is set whenever one of the above error functions are called. It must
+    be cleared manually *)
+val hadErrors: bool ref  
+
+(** Like {!Errormsg.error} but does not raise the {!Errormsg.Error} 
+ * exception. Return type is unit. *)
+val warn:    ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Like {!Errormsg.warn} but optional. Printed only if the 
+ * {!Errormsg.warnFlag} is set *)
+val warnOpt: ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Print something to [logChannel] *)
+val log:           ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** same as {!Errormsg.log} but do not wrap lines *)
+val logg:          ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+   (* All of the error and warning reporting functions can also print a 
+    * context. To register a context printing function use "pushContext". To 
+    * remove the last registered one use "popContext". If one of the error 
+    * reporting functions is called it will invoke all currently registered 
+    * context reporting functions in the reverse order they were registered. *)
+
+(** Do not actually print (i.e. print to /dev/null) *)
+val null : ('a,unit,Pretty.doc,unit) format4 -> 'a
+
+(** Registers a context printing function *)
+val pushContext  : (unit -> Pretty.doc) -> unit
+
+(** Removes the last registered context printing function *)
+val popContext   : unit -> unit
+
+(** Show the context stack to stderr *)
+val showContext : unit -> unit
+
+(** To ensure that the context is registered and removed properly, use the 
+    function below *)
+val withContext  : (unit -> Pretty.doc) -> ('a -> 'b) -> 'a -> 'b
+
+
+
+val newline: unit -> unit  (* Call this function to announce a new line *)
+val newHline: unit -> unit 
+
+val getPosition: unit -> int * string * int (* Line number, file name, 
+                                               current byte count in file *)
+val getHPosition: unit -> int * string (** high-level position *)
+
+val setHLine: int -> unit
+val setHFile: string -> unit
+
+val setCurrentLine: int -> unit
+val setCurrentFile: string -> unit
+
+(** Type for source-file locations *)
+type location = 
+    { file: string; (** The file name *)
+      line: int;    (** The line number *)
+      hfile: string; (** The high-level file name, or "" if not present *)
+      hline: int;    (** The high-level line number, or 0 if not present *)
+    } 
+
+val d_loc: unit -> location -> Pretty.doc
+val d_hloc: unit -> location -> Pretty.doc
+    
+val getLocation: unit -> location
+
+val parse_error: string -> (* A message *) 
+                 'a
+
+(** An unknown location for use when you need one but you don't have one *)
+val locUnknown: location
+
+
+(** Records whether the stdin is open for reading the goal **)
+val readingFromStdin: bool ref
+
+
+(* Call this function to start parsing. useBasename is by default "true", 
+ * meaning that the error information maintains only the basename. If the 
+ * file name is - then it reads from stdin. *)
+val startParsing:  ?useBasename:bool -> string -> 
+  Lexing.lexbuf 
+
+val startParsingFromString: ?file:string -> ?line:int -> string
+                            -> Lexing.lexbuf
+
+val finishParsing: unit -> unit (* Call this function to finish parsing and 
+                                 * close the input channel *)
+
+
diff --git a/cil/ocamlutil/growArray.ml b/cil/ocamlutil/growArray.ml
new file mode 100644
index 00000000..ccadc762
--- /dev/null
+++ b/cil/ocamlutil/growArray.ml
@@ -0,0 +1,191 @@
+(** Growable Arrays *)
+
+type 'a fill =
+    Elem of 'a
+  | Susp of (int -> 'a)
+
+type 'a t = {
+            gaFill: 'a fill;
+            (** Stuff to use to fill in the array as it grows *)
+
+    mutable gaMaxInitIndex: int;
+            (** Maximum index that was written to. -1 if no writes have 
+             * been made.  *)
+
+    mutable gaData: 'a array;
+  } 
+
+let growTheArray (ga: 'a t) (len: int) 
+                 (toidx: int) (why: string) : unit = 
+  if toidx >= len then begin
+    (* Grow the array by 50% *)
+    let newlen = toidx + 1 + len  / 2 in
+(*
+    ignore (E.log "growing an array to idx=%d (%s)\n" toidx why);
+*)
+    let data' = begin match ga.gaFill with
+      Elem x ->
+	let data'' = Array.create newlen x in
+	Array.blit ga.gaData 0 data'' 0 len;
+	data''
+    | Susp f -> Array.init newlen
+	  (fun i -> if i < len then ga.gaData.(i) else f i)
+    end
+    in
+    ga.gaData <- data'
+  end
+
+let max_init_index (ga: 'a t) : int =
+  ga.gaMaxInitIndex
+
+let num_alloc_index (ga: 'a t) : int = 
+  Array.length ga.gaData
+
+let reset_max_init_index (ga: 'a t) : unit =
+  ga.gaMaxInitIndex <- -1
+
+let getg (ga: 'a t) (r: int) : 'a = 
+  let len = Array.length ga.gaData in
+  if r >= len then 
+    growTheArray ga len r "getg";
+
+  ga.gaData.(r)
+
+let setg (ga: 'a t) (r: int) (what: 'a) : unit = 
+  let len = Array.length ga.gaData in
+  if r >= len then 
+    growTheArray ga len r "setg";
+  if r > max_init_index ga then ga.gaMaxInitIndex <- r;
+  ga.gaData.(r) <- what
+
+let get (ga: 'a t) (r: int) : 'a = Array.get ga.gaData r
+
+let set (ga: 'a t) (r: int) (what: 'a) : unit = 
+  if r > max_init_index ga then ga.gaMaxInitIndex <- r;
+  Array.set ga.gaData r what
+
+let make (initsz: int) (fill: 'a fill) : 'a t = 
+  { gaFill = fill;
+    gaMaxInitIndex = -1;
+    gaData = begin match fill with
+      Elem x -> Array.create initsz x
+    | Susp f -> Array.init initsz f
+    end; }
+
+let clear (ga: 'a t) : unit =
+  (* This assumes the user hasn't used the raw "set" on any value past
+     max_init_index.  Maybe we shouldn't trust max_init_index here?? *) 
+  if ga.gaMaxInitIndex >= 0 then begin
+    begin match ga.gaFill with 
+        Elem x -> Array.fill ga.gaData 0 (ga.gaMaxInitIndex+1) x
+      | Susp f -> 
+          for i = 0 to ga.gaMaxInitIndex do 
+            Array.set ga.gaData i (f i)
+          done
+    end;
+    ga.gaMaxInitIndex <- -1
+  end
+
+let copy (ga: 'a t) : 'a t = 
+  { ga with gaData = Array.copy ga.gaData } 
+
+let deep_copy (ga: 'a t) (copy: 'a -> 'a): 'a t = 
+  { ga with gaData = Array.map copy ga.gaData } 
+
+(* An accumulating for loop. Used internally. *)
+let fold_for ~(init: 'a) ~(lo: int) ~(hi: int) (f: int -> 'a -> 'a) =
+  let rec forloop i acc =
+    if i > hi then acc
+    else forloop (i+1) (f i acc)
+  in
+  forloop lo init
+
+(** Iterate over the initialized elements of the array *)
+let iter (f: 'a -> unit) (ga: 'a t) = 
+  for i = 0 to max_init_index ga do 
+    f ga.gaData.(i)
+  done
+
+(** Iterate over the initialized elements of the array *)
+let iteri  (f: int -> 'a -> unit) (ga: 'a t) = 
+  for i = 0 to max_init_index ga do 
+    f i ga.gaData.(i)
+  done
+
+(** Iterate over the elements of 2 arrays *)
+let iter2  (f: int -> 'a -> 'b -> unit) (ga1: 'a t) (ga2: 'b t) = 
+  let len1 = max_init_index ga1 in
+  let len2 = max_init_index ga2 in
+  if len1 > -1 || len2 > -1 then begin
+    let max = if len1 > len2 then begin
+                  ignore(getg ga2 len1); (*grow ga2 to match ga1*)
+                  len1
+              end else begin
+                  ignore(getg ga1 len2); (*grow ga1 to match ga2*)
+                  len2
+              end in
+    for i = 0 to max do 
+      f i ga1.gaData.(i) ga2.gaData.(i)
+    done
+  end
+
+(** Fold left over the initialized elements of the array *)
+let fold_left (f: 'acc -> 'a -> 'acc) (acc: 'acc) (ga: 'a t) : 'acc = 
+  let rec loop (acc: 'acc) (idx: int) : 'acc = 
+    if idx > max_init_index ga then 
+      acc
+    else
+      loop (f acc ga.gaData.(idx)) (idx + 1)
+  in
+  loop acc 0
+
+
+(** Fold left over the initialized elements of the array *)
+let fold_lefti (f: 'acc -> int -> 'a -> 'acc) (acc: 'acc) (ga: 'a t) : 'acc = 
+  let rec loop (acc: 'acc) (idx: int) : 'acc = 
+    if idx > max_init_index ga then 
+      acc
+    else
+      loop (f acc idx ga.gaData.(idx)) (idx + 1)
+  in
+  loop acc 0
+
+(** Fold right over the initialized elements of the array *)
+let fold_right (f: 'a -> 'acc -> 'acc) (ga: 'a t) (acc: 'acc) : 'acc = 
+  let rec loop (acc: 'acc) (idx: int) : 'acc = 
+    if idx < 0 then 
+      acc
+    else
+      loop (f ga.gaData.(idx) acc) (idx - 1)
+  in
+  loop acc (max_init_index ga)
+
+(** Document generator *)
+let d_growarray (sep: Pretty.doc)
+                (doit:int -> 'a -> Pretty.doc)
+                ()
+                (elements: 'a t) =
+  Pretty.docArray ~sep:sep doit () elements.gaData
+
+let restoreGA ?deepCopy (ga: 'a t) : (unit -> unit) = 
+  let old = 
+    (match deepCopy with 
+         None -> copy ga
+       | Some f -> deep_copy ga f)
+  in
+  (fun () ->
+     if ga.gaFill != old.gaFill then
+       Errormsg.s 
+         (Errormsg.bug "restoreGA to an array with a different fill.");
+     ga.gaMaxInitIndex <- old.gaMaxInitIndex;
+     for i = 0 to max_init_index ga do 
+       set ga i (getg old i)
+     done)
+
+let find (ga: 'a t) (fn: 'a -> bool) : int option = 
+  let rec loop (i:int) : int option = 
+    if i > ga.gaMaxInitIndex then None
+    else if fn (get ga i) then Some i
+    else loop (i + 1)
+  in
+  loop 0
diff --git a/cil/ocamlutil/growArray.mli b/cil/ocamlutil/growArray.mli
new file mode 100644
index 00000000..4cb5f48f
--- /dev/null
+++ b/cil/ocamlutil/growArray.mli
@@ -0,0 +1,131 @@
+(***********************************************************************)
+(* Growable Arrays                                                     *)
+(*                                                                     *)
+(* This a wrapper around the standard OCaml array, but will grow       *)
+(* automatically on get or set outside the current size of the         *)
+(* array.                                                              *)
+(*                                                                     *)
+(* The interface is the same as the standard OCaml array where         *)
+(* applicable (and implemented).                                       *)
+(***********************************************************************)
+
+(* $Id: growArray.mli,v 1.8 2005-01-06 15:37:36 necula Exp $ *)
+
+(** Array operations. *)
+
+(** The type of growable arrays *)
+type 'a t
+
+(** The default value to a new element of the growable array *)
+type 'a fill =
+    Elem of 'a
+    (* A default value *)
+  | Susp of (int -> 'a)
+    (* A function given an index to generate a default value *)
+
+val make : int -> 'a fill -> 'a t
+(** [GrowArray.make n x] returns a fresh growable array of size
+   at least [n] with default value specified by [x].
+
+   Raise [Invalid_argument] if [n < 0] or [n > Sys.max_array_length]. *)
+
+val num_alloc_index: 'a t -> int
+(** [GrowArray.num_alloc_index a] returns the number of allocated entries in 
+ * the array **)
+
+val max_init_index : 'a t -> int
+(** [GrowArray.max_init_index a] returns the maximum index to
+    which has been written.
+
+    Returns -1 if no writes have been made. *)
+
+val reset_max_init_index : 'a t -> unit
+(** [GrowArray.reset_init a] resets the max_init_index. You should probably
+   use [GrowArray.clear a] instead if you also want to delete the contents. *)
+
+val getg : 'a t -> int -> 'a
+(** [GrowArray.getg a n] returns the element number [n] of array [a].
+   The first element has number 0.
+   The last element has number [GrowArray.length a - 1].
+
+   If [n] is outside the range 0 to [(GrowArray.max_init_index a)],
+   then the array grows to at least [n] and yields the default value. *)
+
+val setg : 'a t -> int -> 'a -> unit
+(** [GrowArray.setg a n x] modifies array [a] in place, replacing
+   element number [n] with [x].
+
+   If [n] is outside the range 0 to [(GrowArray.max_init_index a)],
+   then the array grows to at least [n] and yields the default value. *)
+
+val get : 'a t -> int -> 'a
+(** [GrowArray.get a n] returns the element number [n] of grow array [a].
+
+   Raise [Invalid_argument "Array.get"]  if [n] is outside the range
+   of the underlying array. *)
+
+val set : 'a t -> int -> 'a -> unit
+(** [GrowArray.set a n x] modifies grow array [a] in place, replacing
+   element number [n] with [x].
+
+   Raise [Invalid_argument "Array.set"] if [n] is outside the range
+   of the underlying array. *)
+        
+val clear: 'a t -> unit 
+(** [GrowArray.clear a] clears the contents of the array and sets 
+   max_init_index to -1.  Suspension thunks will be rerun to regenerate the 
+   initial values of the array. *)
+
+val copy : 'a t -> 'a t
+(** [GrowArray.copy a] returns a copy of [a], that is, a fresh array
+   containing the same elements as [a]. *)
+
+val deep_copy : 'a t -> ('a -> 'a) -> 'a t
+(** [GrowArray.copy a f] returns a deep copy of [a] using f to
+    copy elements of [a]. *)
+
+val iter : ('a -> unit) -> 'a t -> unit
+(** [GrowArray.iter f a] applies function [f] in turn to all
+   the elements of [a].  It is equivalent to
+   [f a.(0); f a.(1); ...; f a.(GrowArray.length a - 1); ()]. *)
+
+val iteri : (int -> 'a -> unit) -> 'a t -> unit
+(** Same as {!GrowArray.iter}, but the
+   function is applied to the index of the element as first argument,
+   and the element itself as second argument. *)
+
+val iter2 : (int -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
+(** Same as {!GrowArray.iteri}, but the function is applied to two arrays.
+  [iter2 f a b]  is equivalent to
+  [f 0 a.(0) b.(0); f 1 a.(1) b.(1); ...;  f n a.(n) b.(n); ()]
+  where n is the larger of (max_init_index a) or (max_init_index b).
+  The shorter array will grow to match the longer.*)
+
+val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+(** [GrowArray.fold_left f x a] computes
+   [f (... (f (f x a.(0)) a.(1)) ...) a.(n-1)],
+   where [n] is the length of the array [a]. *)
+
+val fold_lefti : ('a -> int -> 'b -> 'a) -> 'a -> 'b t -> 'a
+(** [GrowArray.fold_lefti f x a] computes
+   [f (... (f (f x 0 a.(0)) 1 a.(1)) ...) (n-1) a.(n-1)],
+   where [n] is the length of the array [a]. *)
+
+val fold_right : ('b -> 'a -> 'a) -> 'b t -> 'a -> 'a
+(** [GrowArray.fold_right f a x] computes
+   [f a.(0) (f a.(1) ( ... (f a.(n-1) x) ...))],
+   where [n] is the length of the array [a]. *)
+
+val d_growarray : Pretty.doc -> (int -> 'a -> Pretty.doc) -> unit -> 'a t
+                             -> Pretty.doc
+(** [GrowArray.d_growarray sep f () a] creates a {!Pretty.doc} for growable
+   array a using separator sep and element printer f. *)
+
+
+val restoreGA: ?deepCopy:('a -> 'a) -> 'a t -> unit -> unit
+(** Given a growable array, produce a thunk that later restores it to its
+    current value *)
+
+val find: 'a t -> ('a -> bool) -> int option
+(** Returns the index of the first element in the array that satisfies the
+    predicate, or None if there is no such element *)
diff --git a/cil/ocamlutil/inthash.ml b/cil/ocamlutil/inthash.ml
new file mode 100755
index 00000000..b1ad0c07
--- /dev/null
+++ b/cil/ocamlutil/inthash.ml
@@ -0,0 +1,188 @@
+(** A hash table specialized on integer keys *)
+type 'a t =
+  { mutable size: int;                        (* number of elements *)
+    mutable data: 'a bucketlist array } (* the buckets *)
+
+and 'a bucketlist =
+    Empty
+  | Cons of int * 'a * 'a bucketlist
+
+let hash key = key land 0x3fffffff
+
+let create initial_size =
+  let s = min (max 1 initial_size) Sys.max_array_length in
+  { size = 0; data = Array.make s Empty }
+
+let clear h =
+  for i = 0 to Array.length h.data - 1 do
+    h.data.(i) <- Empty
+  done;
+  h.size <- 0
+
+let copy h =
+  { size = h.size;
+    data = Array.copy h.data }
+
+let copy_into src dest = 
+  dest.size <- src.size;
+  dest.data <- Array.copy src.data
+
+let length h = h.size
+
+let resize tbl =
+  let odata = tbl.data in
+  let osize = Array.length odata in
+  let nsize = min (2 * osize + 1) Sys.max_array_length in
+  if nsize <> osize then begin
+    let ndata = Array.create nsize Empty in
+    let rec insert_bucket = function
+        Empty -> ()
+      | Cons(key, data, rest) ->
+          insert_bucket rest; (* preserve original order of elements *)
+          let nidx = (hash key) mod nsize in
+          ndata.(nidx) <- Cons(key, data, ndata.(nidx)) in
+    for i = 0 to osize - 1 do
+      insert_bucket odata.(i)
+    done;
+    tbl.data <- ndata;
+  end
+
+let add h key info =
+  let i = (hash key) mod (Array.length h.data) in
+  let bucket = Cons(key, info, h.data.(i)) in
+  h.data.(i) <- bucket;
+  h.size <- succ h.size;
+  if h.size > Array.length h.data lsl 1 then resize h
+
+let remove h key =
+  let rec remove_bucket = function
+      Empty ->
+        Empty
+    | Cons(k, i, next) ->
+        if k = key
+        then begin h.size <- pred h.size; next end
+        else Cons(k, i, remove_bucket next) in
+  let i = (hash key) mod (Array.length h.data) in
+  h.data.(i) <- remove_bucket h.data.(i)
+
+let remove_all h key =
+  let rec remove_bucket = function
+      Empty ->
+        Empty
+    | Cons(k, i, next) ->
+        if k = key
+        then begin h.size <- pred h.size; 
+	  remove_bucket next end
+        else Cons(k, i, remove_bucket next) in
+  let i = (hash key) mod (Array.length h.data) in
+  h.data.(i) <- remove_bucket h.data.(i)
+
+let rec find_rec key = function
+    Empty ->
+      raise Not_found
+  | Cons(k, d, rest) ->
+      if key = k then d else find_rec key rest
+
+let find h key =
+  match h.data.((hash key) mod (Array.length h.data)) with
+    Empty -> raise Not_found
+  | Cons(k1, d1, rest1) ->
+      if key = k1 then d1 else
+      match rest1 with
+        Empty -> raise Not_found
+      | Cons(k2, d2, rest2) ->
+          if key = k2 then d2 else
+          match rest2 with
+            Empty -> raise Not_found
+          | Cons(k3, d3, rest3) ->
+              if key = k3 then d3 else find_rec key rest3
+
+let find_all h key =
+  let rec find_in_bucket = function
+    Empty ->
+      []
+  | Cons(k, d, rest) ->
+      if k = key then d :: find_in_bucket rest else find_in_bucket rest in
+  find_in_bucket h.data.((hash key) mod (Array.length h.data))
+
+let replace h key info =
+  let rec replace_bucket = function
+      Empty ->
+        raise Not_found
+    | Cons(k, i, next) ->
+        if k = key
+        then Cons(k, info, next)
+        else Cons(k, i, replace_bucket next) in
+  let i = (hash key) mod (Array.length h.data) in
+  let l = h.data.(i) in
+  try
+    h.data.(i) <- replace_bucket l
+  with Not_found ->
+    h.data.(i) <- Cons(key, info, l);
+    h.size <- succ h.size;
+    if h.size > Array.length h.data lsl 1 then resize h
+
+let mem h key =
+  let rec mem_in_bucket = function
+  | Empty ->
+      false
+  | Cons(k, d, rest) ->
+      k = key || mem_in_bucket rest in
+  mem_in_bucket h.data.((hash key) mod (Array.length h.data))
+
+let iter (f: int -> 'a -> unit) (h: 'a t) : unit =
+  let rec do_bucket = function
+      Empty ->
+        ()
+    | Cons(k, d, rest) ->
+        f k d; do_bucket rest in
+  let d = h.data in
+  for i = 0 to Array.length d - 1 do
+    do_bucket d.(i)
+  done
+
+let fold (f: int -> 'a -> 'b -> 'b) (h: 'a t) (init: 'b) =
+  let rec do_bucket b accu =
+    match b with
+      Empty ->
+        accu
+    | Cons(k, d, rest) ->
+        do_bucket rest (f k d accu) in
+  let d = h.data in
+  let accu = ref init in
+  for i = 0 to Array.length d - 1 do
+    accu := do_bucket d.(i) !accu
+  done;
+  !accu
+
+
+let memoize (h: 'a t) (key: int) (f: int -> 'a) : 'a = 
+  let i = (hash key) mod (Array.length h.data) in
+  let rec find_rec key = function
+      Empty -> addit ()
+    | Cons(k, d, rest) ->
+        if key = k then d else find_rec key rest
+  and find_in_bucket key = function
+      Empty -> addit ()
+    | Cons(k1, d1, rest1) ->
+        if key = k1 then d1 else
+        match rest1 with
+          Empty -> addit ()
+        | Cons(k2, d2, rest2) ->
+            if key = k2 then d2 else
+            match rest2 with
+              Empty -> addit () 
+            | Cons(k3, d3, rest3) ->
+                if key = k3 then d3 else find_rec key rest3
+  and addit () = 
+    let it = f key in
+    h.data.(i) <- Cons(key, it, h.data.(i));
+    h.size <- succ h.size;
+    if h.size > Array.length h.data lsl 1 then resize h;
+    it
+  in
+  find_in_bucket key h.data.(i)
+                  
+  
+let tolist (h: 'a t) : (int * 'a) list = 
+  fold (fun k d acc -> (k, d) :: acc) h []
diff --git a/cil/ocamlutil/inthash.mli b/cil/ocamlutil/inthash.mli
new file mode 100755
index 00000000..f62fcd2b
--- /dev/null
+++ b/cil/ocamlutil/inthash.mli
@@ -0,0 +1,27 @@
+type 'a t
+
+(* These functions behave the same as Hashtbl, but the key type is
+   always int.  (Specializing on int improves the performance) *)
+
+val create: int -> 'a t
+val clear: 'a t -> unit
+val length : 'a t -> int
+
+val copy: 'a t -> 'a t
+val copy_into: 'a t -> 'a t -> unit
+
+val add: 'a t -> int -> 'a -> unit
+val replace: 'a t -> int -> 'a -> unit
+val remove: 'a t -> int -> unit
+val remove_all: 'a t -> int -> unit
+
+val mem: 'a t -> int -> bool
+val find: 'a t -> int -> 'a
+val find_all: 'a t -> int -> 'a list
+
+val iter: (int -> 'a -> unit) -> 'a t -> unit
+val fold: (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+
+val memoize: 'a t -> int -> (int -> 'a) -> 'a
+
+val tolist: 'a t -> (int * 'a) list
diff --git a/cil/ocamlutil/intmap.ml b/cil/ocamlutil/intmap.ml
new file mode 100755
index 00000000..00242bc1
--- /dev/null
+++ b/cil/ocamlutil/intmap.ml
@@ -0,0 +1,171 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           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: intmap.ml,v 1.2 2005-10-04 21:30:25 necula Exp $ *)
+
+(* specialized to integer keys by George Necula *)
+
+type 'a t =
+    Empty
+  | Node of 'a t * int * 'a * 'a t * int
+
+let height = function
+    Empty -> 0
+  | Node(_,_,_,_,h) -> h
+        
+let create l x d r =
+  let hl = height l and hr = height r in
+  Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+let bal l x d 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 "Map.bal"
+    | Node(ll, lv, ld, lr, _) ->
+        if height ll >= height lr then
+          create ll lv ld (create lr x d r)
+        else begin
+          match lr with
+            Empty -> invalid_arg "Map.bal"
+          | Node(lrl, lrv, lrd, lrr, _)->
+              create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+        end
+  end else if hr > hl + 2 then begin
+    match r with
+      Empty -> invalid_arg "Map.bal"
+    | Node(rl, rv, rd, rr, _) ->
+        if height rr >= height rl then
+          create (create l x d rl) rv rd rr
+        else begin
+          match rl with
+            Empty -> invalid_arg "Map.bal"
+          | Node(rll, rlv, rld, rlr, _) ->
+              create (create l x d rll) rlv rld (create rlr rv rd rr)
+        end
+  end else
+    Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+      
+let empty = Empty
+
+let is_empty = function Empty -> true | _ -> false
+    
+let rec add x data = function
+    Empty ->
+      Node(Empty, x, data, Empty, 1)
+  | Node(l, v, d, r, h) as t ->
+      if x = v then
+        Node(l, x, data, r, h)
+      else if x < v then
+        bal (add x data l) v d r
+      else
+        bal l v d (add x data r)
+          
+let rec find x = function
+    Empty ->
+      raise Not_found
+  | Node(l, v, d, r, _) ->
+      if x = v then d
+      else find x (if x < v then l else r)
+          
+let rec mem x = function
+    Empty ->
+      false
+  | Node(l, v, d, r, _) ->
+      x = v || mem x (if x < v then l else r)
+        
+let rec min_binding = function
+    Empty -> raise Not_found
+  | Node(Empty, x, d, r, _) -> (x, d)
+  | Node(l, x, d, r, _) -> min_binding l
+        
+let rec remove_min_binding = function
+    Empty -> invalid_arg "Map.remove_min_elt"
+  | Node(Empty, x, d, r, _) -> r
+  | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+let merge t1 t2 =
+  match (t1, t2) with
+    (Empty, t) -> t
+  | (t, Empty) -> t
+  | (_, _) ->
+      let (x, d) = min_binding t2 in
+      bal t1 x d (remove_min_binding t2)
+
+let rec remove x = function
+    Empty ->
+      Empty
+  | Node(l, v, d, r, h) as t ->
+      if x = v then
+        merge l r
+      else if x < v then
+        bal (remove x l) v d r
+      else
+        bal l v d (remove x r)
+
+let rec iter f = function
+    Empty -> ()
+  | Node(l, v, d, r, _) ->
+      iter f l; f v d; iter f r
+
+let rec map f = function
+    Empty               -> Empty
+  | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
+
+let rec mapi f = function
+    Empty               -> Empty
+  | Node(l, v, d, r, h) -> Node(mapi f l, v, f v d, mapi f r, h)
+
+let rec fold f m accu =
+  match m with
+    Empty -> accu
+  | Node(l, v, d, r, _) ->
+      fold f l (f v d (fold f r accu))
+
+type 'a enumeration = End | More of int * 'a * 'a t * 'a enumeration
+
+let rec cons_enum m e =
+  match m with
+    Empty -> e
+  | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e))
+
+let compare cmp m1 m2 =
+  let rec compare_aux e1 e2 =
+    match (e1, e2) with
+      (End, End) -> 0
+    | (End, _)  -> -1
+    | (_, End) -> 1
+    | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+        if v1 <> v2 then if v1 < v2 then -1 else 1 else
+        let c = cmp d1 d2 in
+        if c <> 0 then c else
+        compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+in compare_aux (cons_enum m1 End) (cons_enum m2 End)
+
+let equal cmp m1 m2 =
+  let rec equal_aux e1 e2 =
+    match (e1, e2) with
+      (End, End) -> true
+    | (End, _)  -> false
+    | (_, End) -> false
+    | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+        v1 = v2 && cmp d1 d2 &&
+        equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
+in equal_aux (cons_enum m1 End) (cons_enum m2 End)
+
+(** Some definitions for ML2Coq *)
+let _ = ignore "coq: 
+(* Some definitions for ML2Coq *)
+
+"
diff --git a/cil/ocamlutil/intmap.mli b/cil/ocamlutil/intmap.mli
new file mode 100755
index 00000000..eef89b55
--- /dev/null
+++ b/cil/ocamlutil/intmap.mli
@@ -0,0 +1,87 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           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: intmap.mli,v 1.1 2005-02-28 16:24:00 necula Exp $ *)
+
+(** Specialized to integer keys by George Necula *)
+
+(** Association tables over ordered types.
+
+   This module implements applicative association tables, also known as
+   finite maps or dictionaries, given a total ordering function
+   over the keys.
+   All operations over maps are purely applicative (no side-effects).
+   The implementation uses balanced binary trees, and therefore searching
+   and insertion take time logarithmic in the size of the map. 
+*)
+
+type (+'a) t
+      (** The type of maps from type [key] to type ['a]. *)
+
+val empty: 'a t
+    (** The empty map. *)
+
+val is_empty: 'a t -> bool
+    (** Test whether a map is empty or not. *)
+
+val add: int -> 'a -> 'a t -> 'a t
+    (** [add x y m] returns a map containing the same bindings as
+       [m], plus a binding of [x] to [y]. If [x] was already bound
+       in [m], its previous binding disappears. *)
+
+val find: int -> 'a t -> 'a
+    (** [find x m] returns the current binding of [x] in [m],
+       or raises [Not_found] if no such binding exists. *)
+
+val remove: int -> 'a t -> 'a t
+    (** [remove x m] returns a map containing the same bindings as
+       [m], except for [x] which is unbound in the returned map. *)
+
+val mem: int -> 'a t -> bool
+    (** [mem x m] returns [true] if [m] contains a binding for [x],
+       and [false] otherwise. *)
+
+val iter: (int -> 'a -> unit) -> 'a t -> unit
+    (** [iter f m] applies [f] to all bindings in map [m].
+       [f] receives the key as first argument, and the associated value
+       as second argument.  The bindings are passed to [f] in increasing
+       order with respect to the ordering over the type of the keys.
+       Only current bindings are presented to [f]:
+       bindings hidden by more recent bindings are not passed to [f]. *)
+
+val map: ('a -> 'b) -> 'a t -> 'b t
+    (** [map f m] returns a map with same domain as [m], where the
+       associated value [a] of all bindings of [m] has been
+       replaced by the result of the application of [f] to [a].
+       The bindings are passed to [f] in increasing order
+       with respect to the ordering over the type of the keys. *)
+
+val mapi: (int -> 'a -> 'b) -> 'a t -> 'b t
+    (** Same as {!Map.S.map}, but the function receives as arguments both the
+       key and the associated value for each binding of the map. *)
+
+val fold: (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+    (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
+       where [k1 ... kN] are the keys of all bindings in [m]
+       (in increasing order), and [d1 ... dN] are the associated data. *)
+
+val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+    (** Total ordering between maps.  The first argument is a total ordering
+        used to compare data associated with equal keys in the two maps. *)
+
+val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+    (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
+       equal, that is, contain equal keys and associate them with
+       equal data.  [cmp] is the equality predicate used to compare
+       the data associated with the keys. *)
+
diff --git a/cil/ocamlutil/perfcount.c.in b/cil/ocamlutil/perfcount.c.in
new file mode 100755
index 00000000..ae532f69
--- /dev/null
+++ b/cil/ocamlutil/perfcount.c.in
@@ -0,0 +1,184 @@
+// -*- Mode: c -*-
+//
+/*
+ * A module that allows the reading of performance counters on Pentium.
+ *
+ * This file contains both code that uses the performance counters to 
+ * compute the number of cycles per second (to be used during ./configure) 
+ * and also code to read the performance counters from Ocaml.
+ *
+ * Author: George Necula (necula@cs.berkeley.edu)
+ */
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#if defined(__GNUC__)
+  #define longlong long long
+  // RDTSC puts the result in EAX and EDX. We tell gcc to use those registers
+  // for "low" and "high"
+  #if defined(__i386__)
+    #define GETCOUNTER(low,high) \
+            __asm__ volatile ("rdtsc" : "=a" (low), "=d" (high));
+  #else
+    #define GETCOUNTER(low,high) \
+            printf ("Reading of performance counters is supported only on Intel x86\n"); \
+            exit(1);
+  #endif
+#else
+  // Microsoft Visual Studio
+  #define longlong __int64
+  #define inline   __inline
+  #define GETCOUNTER(low,high) __asm { \
+    __asm rdtsc \
+    __asm mov low, eax \
+    __asm mov high, edx };
+#endif
+
+/* Store here the first value read from the performance counter */
+unsigned static longlong first_value;
+
+
+/* This is the function that actually reads the performance counter. */
+inline unsigned longlong read_ppc(void) {
+  unsigned long pclow, pchigh;
+  unsigned longlong lowhigh;
+
+  GETCOUNTER(pclow, pchigh);
+  
+  // printf ("Read low=0x%08lx high=0x%08lx\n", low, high);
+
+  // Put the 64-bit value together
+  lowhigh = ((unsigned longlong)pclow) | ((unsigned longlong)pchigh << 32);
+
+  if(first_value == 0) {
+    first_value = lowhigh;
+  }
+  return lowhigh - first_value;
+}
+
+
+/* sm: I want a version that is as fast as possible, dropping
+ * bits that aren't very important to achieve it. *
+ *
+ * This version drops the low 20 bits and the high 14 bits so the
+ * result is 30 bits (always a positive Ocaml int); this yields
+ * megacycles, which for GHz machines will be something like
+ * milliseconds. */
+static unsigned long sample_ppc_20(void)
+{
+  unsigned long pclow, pchigh;
+
+  GETCOUNTER(pclow, pchigh);
+
+  return ((pclow >> 20) | (pchigh << 12)) & 0x3FFFFFFF;
+}
+
+/* This version drops the low 10 bits, yielding something like
+ * microseconds. */
+inline static unsigned long sample_ppc_10()
+{
+  unsigned long pclow, pchigh;
+
+  GETCOUNTER(pclow,pchigh);
+    
+  return ((pclow >> 10) | (pchigh << 22)) & 0x3FFFFFFF;
+}
+
+
+
+#ifndef CONFIGURATION_ONLY
+/*** This is the OCAML stub for the read_ppc ***/
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+
+#define CYCLES_PER_USEC @CYCLES_PER_USEC@
+value read_pentium_perfcount()
+{
+  double counter = (double)read_ppc() / (1000000.0 * CYCLES_PER_USEC);
+  return copy_double(counter);
+}
+
+/* The Ocaml system can use this function to figure out if there are
+ * performance counters available */
+value has_performance_counters() {
+  // HAS_PERFCOUNT is set by the configuration code at the end of
+  // this file, during ./configure
+#if @HAS_PERFCOUNT@ != 0
+  return Val_true;
+#else
+  return Val_false;
+#endif
+}
+
+/* sm: interface to above from Ocaml */
+value sample_pentium_perfcount_20()
+{
+  return Val_long(sample_ppc_20());
+}
+
+value sample_pentium_perfcount_10()
+{
+  return Val_long(sample_ppc_10());
+}
+
+#endif
+
+
+/* Now we have a function that tries to compute the number of cycles per 
+ * second (to be used during ./configure) */
+#ifdef CONFIGURATION_ONLY
+#include <sys/times.h>
+#include <unistd.h>
+#include <math.h>
+
+int main() {
+  struct tms t;
+  clock_t start, finish, diff;
+  unsigned longlong start_pc, finish_pc, diff_pc;
+  long clk_per_sec = sysconf(_SC_CLK_TCK);
+  double cycles_per_usec;
+  
+  if(clk_per_sec <= 0) {
+    printf("Cannot find clk_per_sec (got %ld)\n", clk_per_sec);
+    exit(1);
+  }
+  
+  times(&t); start = t.tms_utime;
+  start_pc = read_ppc();
+  // Do something for a while
+  {
+    int i;
+    double a = 5.678;
+    for(i=0;i<10000000;i++) {
+      a = (i & 1) ? (a * a) : (sqrt(a));
+    }
+  }
+  times(&t); finish = t.tms_utime;
+  finish_pc = read_ppc();
+  diff = finish - start;
+  diff_pc = finish_pc - start_pc;
+  if(diff == 0) {
+    printf("Cannot use Unix.times\n");
+    exit(1);
+  }
+  if(diff_pc == 0) {
+    printf("Invalid result from the peformance counters\n");
+    exit(1);
+  }
+  diff_pc /= 1000000; // We care about cycles per microsecond
+//  printf("diff = %ld, diff_pc = %ld, clk = %ld\n",
+//         (long)diff,
+//         (long)diff_pc, (long)clk_per_sec);
+
+  cycles_per_usec = (((double)diff_pc / (double)diff)
+                               * (double)clk_per_sec);
+
+  /* Whatever value we print here will be used as the CYCLES_PER_USEC
+   * below */
+  printf("%.3lf\n", cycles_per_usec);
+  exit(0);
+}
+#endif //defined CONFIGURATION_ONLY
+
diff --git a/cil/ocamlutil/pretty.ml b/cil/ocamlutil/pretty.ml
new file mode 100644
index 00000000..47d07ac4
--- /dev/null
+++ b/cil/ocamlutil/pretty.ml
@@ -0,0 +1,859 @@
+(* 
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+(******************************************************************************)
+(* Pretty printer 
+   This module contains several fast, but sub-optimal heuristics to pretty-print 
+   structured text. 
+*)
+
+let debug =  false
+
+(* Choose an algorithm *)
+type algo = George | Aman | Gap
+let  algo = George
+let fastMode       = ref false
+
+
+(** Whether to print identation or not (for faster printing and smaller 
+  * output) *)
+let printIndent = ref true
+
+(******************************************************************************)	
+(* The doc type and constructors *)
+
+type doc = 
+    Nil
+  | Text     of string
+  | Concat   of doc * doc
+  | CText    of doc * string
+  | Break
+  | Line 
+  | LeftFlush
+  | Align
+  | Unalign  
+  | Mark
+  | Unmark
+
+(* Break a string at \n *)
+let rec breakString (acc: doc) (str: string) : doc = 
+  try
+    (* Printf.printf "breaking string %s\n" str; *)
+    let r = String.index str '\n' in
+    (* Printf.printf "r=%d\n" r; *)
+    let len = String.length str in
+    if r > 0 then begin
+      (* Printf.printf "Taking %s\n" (String.sub str 0 r); *)
+      let acc' = Concat(CText (acc, String.sub str 0 r), Line) in
+      if r = len - 1 then (* The last one *)
+        acc'
+      else begin
+        (* Printf.printf "Continuing with %s\n" (String.sub str (r + 1) (len - r - 1)); *)
+        breakString acc'
+          (String.sub str (r + 1) (len - r - 1))
+      end
+    end else (* The first is a newline *)
+      breakString (Concat(acc, Line))
+        (String.sub str (r + 1) (len - r - 1))
+  with Not_found -> 
+    if acc = Nil then Text str else CText (acc, str)
+
+let nil           = Nil
+let text s        = breakString nil s
+let num  i        = text (string_of_int i)
+let real f        = text (string_of_float f)
+let chr  c        = text (String.make 1 c) 
+let align         = Align
+let unalign       = Unalign
+let line          = Line
+let leftflush     = LeftFlush
+let break         = Break  
+let mark          = Mark
+let unmark        = Unmark
+
+let d_int32 (i: int32) = text (Int32.to_string i)
+let f_int32 () i = d_int32 i
+
+let d_int64 (i: int64) = text (Int64.to_string i)
+let f_int64 () i = d_int64 i
+
+
+(* Note that the ++ operator in Ocaml are left-associative. This means 
+ * that if you have a long list of ++ then the whole thing is very unbalanced 
+ * towards the left side. This is the worst possible case since scanning the 
+ * left side of a Concat is the non-tail recursive case. *)
+
+let (++) d1 d2 = Concat (d1, d2)
+let concat d1 d2 = Concat (d1, d2)
+
+(* Ben Liblit fix *)
+let indent n d = text (String.make n ' ') ++ (align ++ (d ++ unalign))
+
+let markup d = mark ++ d ++ unmark
+
+(* Format a sequence. The first argument is a separator *)
+let seq ~(sep:doc)  ~(doit:'a -> doc) ~(elements: 'a list) = 
+  let rec loop (acc: doc) = function
+      []     -> acc
+    | h :: t -> 
+        let fh = doit h in  (* Make sure this is done first *)
+        loop (acc ++ sep ++ fh) t
+  in
+  (match elements with
+    [] -> nil
+  | h :: t -> 
+      let fh = doit h in loop fh t)
+
+
+let docArray ?(sep=chr ',') (doit:int -> 'a -> doc) () (elements:'a array) = 
+  let len = Array.length elements in
+  if len = 0 then 
+    nil
+  else
+    let rec loop (acc: doc) i =
+      if i >= len then acc else
+      let fi = doit i elements.(i) in (* Make sure this is done first *)
+      loop (acc ++ sep ++ fi) (i + 1)
+    in
+    let f0 = doit 0 elements.(0) in
+    loop f0 1
+
+let docOpt delem () = function
+    None -> text "None"
+  | Some e -> text "Some(" ++ (delem e) ++ chr ')'
+
+
+
+let docList ?(sep=chr ',') (doit:'a -> doc) () (elements:'a list) = 
+  seq sep doit elements
+
+let insert () d = d
+
+
+let d_list (sep:string) (doit:unit -> 'a -> doc) () (elts:'a list) : doc =
+  (* thunk 'doit' to match docList's interface *)
+  let internalDoit (elt:'a) =
+    (doit () elt) in
+  (docList ~sep:(text sep) internalDoit () elts)
+
+(** Format maps *)
+module MakeMapPrinter =
+  functor (Map: sig 
+                  type key
+                  type 'a t
+                  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+                end) ->
+struct
+  let docMap ?(sep=chr ',')
+              (doit: Map.key -> 'a -> doc) () (maplets: 'a Map.t) : doc =
+    Map.fold
+      (fun k d acc ->
+	(if acc==nil then acc else acc ++ sep)
+	  ++ (doit k d))
+      maplets
+      nil
+
+  let dmaplet d0 d1 = d0 ++ (text " |-> ") ++ d1
+
+  let d_map ?(dmaplet=dmaplet) (sep:string) dkey dval =
+    let doit = fun k d -> dmaplet (dkey () k) (dval () d) in
+    docMap ~sep:(text sep) doit
+end
+
+(** Format sets *)
+module MakeSetPrinter =
+  functor (Set: sig 
+                  type elt
+                  type t
+                  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+                end) ->
+struct
+  let docSet ?(sep=chr ',') (doit: Set.elt -> doc) () (set: Set.t) : doc =
+    Set.fold
+      (fun elt acc ->
+	(if acc==nil then acc else acc ++ sep)
+	  ++ (doit elt))
+      set
+      nil
+
+  let d_set (sep:string) delt =
+    docSet ~sep:(text sep) (delt ())
+end
+
+
+(******************************************************************************)	
+(* Some debugging stuff *)
+
+let dbgprintf x = Printf.fprintf stderr x
+
+let rec dbgPrintDoc = function
+    Nil -> dbgprintf "(Nil)"
+  | Text s -> dbgprintf "(Text %s)" s
+  | Concat (d1,d2) -> dbgprintf ""; dbgPrintDoc  d1; dbgprintf " ++\n "; 
+      dbgPrintDoc  d2; dbgprintf ""
+  | CText (d,s) -> dbgPrintDoc  d; dbgprintf " ++ \"%s\"" s; 
+  | Break -> dbgprintf "(Break)" 
+  | Line -> dbgprintf "(Line)"
+  | LeftFlush -> dbgprintf "(LeftFlush)"
+  | Align -> dbgprintf "(Align)"
+  | Unalign -> dbgprintf "(Unalign)"
+  | Mark -> dbgprintf "(Mark)"
+  | Unmark -> dbgprintf "(Unmark)"
+
+(******************************************************************************)	
+(* The "george" algorithm *)
+
+(* When we construct documents, most of the time they are heavily unbalanced 
+ * towards the left. This is due to the left-associativity of ++ and also to 
+ * the fact that constructors such as docList construct from the let of a 
+ * sequence. We would prefer to shift the imbalance to the right to avoid 
+ * consuming a lot of stack when we traverse the document *)
+let rec flatten (acc: doc) = function
+  | Concat (d1, d2) -> flatten (flatten acc d2) d1
+  | CText (d, s) -> flatten (Concat(Text s, acc)) d
+  | Nil -> acc (* Get rid of Nil *)
+  | d -> Concat(d, acc)
+
+(* We keep a stack of active aligns. *)
+type align = 
+    { mutable gainBreak: int;  (* This is the gain that is associated with 
+                                 * taking the break associated with this 
+                                 * alignment mark. If this is 0, then there 
+                                 * is no break associated with the mark *)
+      mutable isTaken: bool ref; (* If breakGain is > 0 then this is a ref 
+                                  * cell that must be set to true when the 
+                                  * break is taken. These ref cells are also 
+                                  * int the "breaks" list  *)
+            deltaFromPrev: int ref; (* The column of this alignment mark - 
+                                     * the column of the previous mark. 
+                                     * Shared with the deltaToNext of the 
+                                     * previous active align  *)
+             deltaToNext: int ref  (* The column of the next alignment mark - 
+                                    * the columns of this one. Shared with 
+                                    * deltaFromPrev of the next active align *)
+    } 
+      
+(* We use references to avoid the need to pass data around all the time *)
+let aligns: align list ref =  (* The current stack of active alignment marks, 
+                               * with the top at the head. Never empty.  *)
+  ref [{ gainBreak = 0; isTaken = ref false; 
+         deltaFromPrev = ref 0; deltaToNext = ref 0; }]
+
+let topAlignAbsCol = ref 0 (* The absolute column of the top alignment *)
+
+let pushAlign (abscol: int) = 
+  let topalign = List.hd !aligns in
+  let res = 
+    { gainBreak = 0; isTaken = ref false; 
+      deltaFromPrev = topalign.deltaToNext; (* Share with the previous *)
+      deltaToNext = ref 0; (* Allocate a new ref *)} in
+  aligns := res :: !aligns;
+  res.deltaFromPrev := abscol - !topAlignAbsCol;
+  topAlignAbsCol := abscol
+
+let popAlign () = 
+  match !aligns with
+    top :: t when t != [] -> 
+      aligns := t; 
+      topAlignAbsCol := !topAlignAbsCol - !(top.deltaFromPrev)
+  | _ -> failwith "Unmatched unalign\n"
+
+(** We keep a list of active markup sections. For each one we keep the column 
+ * we are in *)
+let activeMarkups: int list ref = ref []
+
+
+(* Keep a list of ref cells for the breaks, in the same order that we see 
+ * them in the document *)
+let breaks: bool ref list ref = ref []
+
+(* The maximum column that we should use *)
+let maxCol = ref 0
+
+(* Sometimes we take all the optional breaks *)
+let breakAllMode = ref false
+
+(* We are taking a newline and moving left *)
+let newline () =
+  let topalign = List.hd !aligns in (* aligns is never empty *)
+  if debug then
+    dbgprintf "Taking a newline: reseting gain of %d\n" topalign.gainBreak;
+  topalign.gainBreak <- 0;        (* Erase the current break info *)
+  if !breakAllMode && !topAlignAbsCol < !maxCol then 
+    breakAllMode := false;
+  !topAlignAbsCol                          (* This is the new column *)
+
+
+
+(* Choose the align with the best gain. We outght to find a better way to 
+ * keep the aligns sorted, especially since they gain never changes (when the 
+ * align is the top align) *)
+let chooseBestGain () : align option =        
+  let bestGain = ref 0 in
+  let rec loop (breakingAlign: align option) = function
+      [] -> breakingAlign
+    | a :: resta -> 
+        if debug then dbgprintf "Looking at align with gain %d\n" a.gainBreak;
+        if a.gainBreak > !bestGain then begin
+          bestGain := a.gainBreak;
+          loop (Some a) resta
+        end else
+          loop breakingAlign resta
+  in
+  loop None !aligns
+
+
+(* Another one that chooses the break associated with the current align only *)
+let chooseLastGain () : align option = 
+  let topalign = List.hd !aligns in
+  if topalign.gainBreak > 0 then Some topalign else None
+
+(* We have just advanced to a new column. See if we must take a line break *)
+let movingRight (abscol: int) : int = 
+  (* Keep taking the best break until we get back to the left of maxCol or no 
+   * more are left *)
+  let rec tryAgain abscol = 
+    if abscol <= !maxCol then abscol else 
+    begin
+      if debug then
+        dbgprintf "Looking for a break to take in column %d\n" abscol;
+      (* Find the best gain there is out there *)
+      match if !fastMode then None else chooseBestGain () with 
+        None -> begin
+          (* No breaks are available. Take all breaks from now on *)
+          breakAllMode := true;
+          if debug then
+            dbgprintf "Can't find any breaks\n";
+          abscol
+        end 
+      | Some breakingAlign -> begin
+          let topalign = List.hd !aligns in
+          let theGain = breakingAlign.gainBreak in
+          assert (theGain > 0);
+          if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain;
+          breakingAlign.isTaken := true;
+          breakingAlign.gainBreak <- 0;
+          if breakingAlign != topalign then begin
+            breakingAlign.deltaToNext := 
+               !(breakingAlign.deltaToNext) - theGain;
+            topAlignAbsCol := !topAlignAbsCol - theGain
+          end;
+          tryAgain (abscol - theGain)
+      end
+    end
+  in
+  tryAgain abscol
+
+
+(* Keep track of nested align in gprintf. Each gprintf format string must 
+ * have properly nested align/unalign pairs. When the nesting depth surpasses 
+ * !printDepth then we print ... and we skip until the matching unalign *)
+let printDepth = ref 10000000 (* WRW: must see whole thing *)
+let alignDepth = ref 0
+
+let useAlignDepth = true
+
+(** Start an align. Return true if we ahve just passed the threshhold *)
+let enterAlign () = 
+  incr alignDepth;
+  useAlignDepth && !alignDepth = !printDepth + 1
+
+(** Exit an align *)
+let exitAlign () = 
+  decr alignDepth
+
+(** See if we are at a low-enough align level (and we should be printing 
+ * normally) *)
+let shallowAlign () = 
+  not useAlignDepth || !alignDepth <= !printDepth
+
+
+(* Pass the current absolute column and compute the new column *)
+let rec scan (abscol: int) (d: doc) : int = 
+  match d with 
+    Nil -> abscol
+  | Concat (d1, d2) -> scan (scan abscol d1) d2
+  | Text s when shallowAlign () -> 
+      let sl = String.length s in 
+      if debug then 
+        dbgprintf "Done string: %s from %d to %d\n" s abscol (abscol + sl);
+      movingRight (abscol + sl)
+  | CText (d, s) -> 
+      let abscol' = scan abscol d in
+      if shallowAlign () then begin
+        let sl = String.length s in 
+        if debug then 
+          dbgprintf "Done string: %s from %d to %d\n" s abscol' (abscol' + sl);
+        movingRight (abscol' + sl)
+      end else
+        abscol'
+
+  | Align -> 
+      pushAlign abscol; 
+      if enterAlign () then 
+        movingRight (abscol + 3) (* "..." *)
+      else
+        abscol
+
+  | Unalign -> exitAlign (); popAlign (); abscol 
+
+  | Line when shallowAlign () -> (* A forced line break *) 
+      if !activeMarkups != [] then 
+        failwith "Line breaks inside markup sections";
+      newline ()
+
+  | LeftFlush when shallowAlign ()  -> (* Keep cursor left-flushed *) 0
+
+  | Break when shallowAlign () -> (* An optional line break. Always a space 
+                                   * followed by an optional line break *)
+      if !activeMarkups != [] then 
+        failwith "Line breaks inside markup sections";
+      let takenref = ref false in
+      breaks := takenref :: !breaks;
+      let topalign = List.hd !aligns in (* aligns is never empty *)
+      if !breakAllMode then begin
+        takenref := true;
+        newline ()
+      end else begin
+        (* If there was a previous break there it stays not taken, forever. 
+         * So we overwrite it. *)
+        topalign.isTaken <- takenref;
+        topalign.gainBreak <- 1 + abscol - !topAlignAbsCol;
+        if debug then
+          dbgprintf "Registering a break at %d with gain %d\n" 
+            (1 + abscol) topalign.gainBreak;
+        movingRight (1 + abscol)
+      end
+
+  | Mark -> activeMarkups := abscol :: !activeMarkups;
+            abscol
+
+  | Unmark -> begin
+      match !activeMarkups with 
+        old :: rest -> activeMarkups := rest; 
+                       old
+      | [] -> failwith "Too many unmark"
+  end
+
+  | _ -> (* Align level is too deep *) abscol
+    
+
+(** Keep a running counter of the newlines we are taking. You can read and 
+  * reset this from user code, if you want *)
+let countNewLines = ref 0
+
+(* The actual function that takes a document and prints it *)
+let emitDoc 
+    (emitString: string -> int -> unit) (* emit a number of copies of a 
+                                         * string *)
+    (d: doc) = 
+  let aligns: int list ref = ref [0] in (* A stack of alignment columns *)
+
+  let wantIndent = ref false in
+  (* Use this function to take a newline *)
+  (* AB: modified it to flag wantIndent. The actual indentation is done only 
+     if leftflush is not encountered *)
+  let newline () =
+    match !aligns with
+      [] -> failwith "Ran out of aligns"
+    | x :: _ ->
+	emitString "\n" 1;
+        incr countNewLines;
+	wantIndent := true;
+	x
+  in
+  (* Print indentation if wantIndent was previously flagged ; reset this flag *)
+  let indentIfNeeded () =
+    if !printIndent && !wantIndent then ignore (
+      match !aligns with
+	[] -> failwith "Ran out of aligns"
+      | x :: _ -> 
+          if x > 0 then emitString " "  x;
+          x);
+    wantIndent := false	  
+  in
+  (* A continuation passing style loop *)
+  let rec loopCont (abscol: int) (d: doc) (cont: int -> unit) : unit 
+      (* the new column *) =
+    match d with
+      Nil -> cont abscol
+    | Concat (d1, d2) -> 
+        loopCont abscol d1 (fun abscol' -> loopCont abscol' d2 cont)
+
+    | Text s when shallowAlign () -> 
+        let sl = String.length s in
+	indentIfNeeded ();
+        emitString s 1;
+        cont (abscol + sl)
+
+    | CText (d, s) -> 
+        loopCont abscol d 
+          (fun abscol' -> 
+            if shallowAlign () then 
+              let sl = String.length s in
+	      indentIfNeeded ();
+              emitString s 1; 
+              cont (abscol' + sl)
+            else
+              cont abscol')
+
+    | Align -> 
+        aligns := abscol :: !aligns;
+        if enterAlign () then begin
+          indentIfNeeded ();
+          emitString "..." 1;
+          cont (abscol + 3)
+        end else
+          cont abscol
+
+    | Unalign -> begin
+        match !aligns with
+          [] -> failwith "Unmatched unalign"
+        | _ :: rest -> 
+            exitAlign ();
+            aligns := rest; cont abscol
+    end
+    | Line when shallowAlign ()  -> cont (newline ())
+    | LeftFlush when shallowAlign () -> wantIndent := false;  cont (0)
+    | Break when shallowAlign () -> begin
+        match !breaks with
+          [] -> failwith "Break without a takenref"
+        | istaken :: rest -> 
+            breaks := rest; (* Consume the break *)
+            if !istaken then cont (newline ())
+            else begin
+	      indentIfNeeded ();
+              emitString " " 1; 
+              cont (abscol + 1)
+            end
+    end
+
+    | Mark -> 
+        activeMarkups := abscol :: !activeMarkups;
+        cont abscol
+
+    | Unmark -> begin
+        match !activeMarkups with 
+          old :: rest -> activeMarkups := rest; 
+                         cont old
+        | [] -> failwith "Unmark without a mark"
+    end
+
+    | _ -> (* Align is too deep *)
+        cont abscol
+  in
+
+  loopCont 0 d (fun x -> ()) 
+
+
+(* Print a document on a channel *)
+let fprint (chn: out_channel) ~(width: int) doc =
+  (* Save some parameters, to allow for nested calls of these routines. *)
+  maxCol := width;
+  let old_breaks = !breaks in 
+  breaks := [];
+  let old_alignDepth = !alignDepth in 
+  alignDepth := 0;
+  let old_activeMarkups = !activeMarkups in 
+  activeMarkups := [];
+  ignore (scan 0 doc);
+  breaks := List.rev !breaks;
+  ignore (emitDoc 
+            (fun s nrcopies -> 
+              for i = 1 to nrcopies do
+                output_string chn s
+              done) doc);
+  activeMarkups := old_activeMarkups;
+  alignDepth := old_alignDepth;
+  breaks := old_breaks (* We must do this especially if we don't do emit 
+                        * (which consumes breaks) because otherwise we waste 
+                        * memory *)
+
+(* Print the document to a string *)
+let sprint ~(width : int)  doc : string = 
+  maxCol := width;
+  let old_breaks = !breaks in 
+  breaks := [];
+  let old_activeMarkups = !activeMarkups in 
+  activeMarkups := [];
+  let old_alignDepth = !alignDepth in 
+  alignDepth := 0;
+  ignore (scan 0 doc);
+  breaks := List.rev !breaks;
+  let buf = Buffer.create 1024 in
+  let rec add_n_strings str num =
+    if num <= 0 then ()
+    else begin Buffer.add_string buf str; add_n_strings str (num - 1) end
+  in
+  emitDoc add_n_strings doc;
+  breaks  := old_breaks;
+  activeMarkups := old_activeMarkups;
+  alignDepth := old_alignDepth;
+  Buffer.contents buf
+
+
+                                        (* The rest is based on printf.ml *)
+external format_int: string -> int -> string = "caml_format_int"
+external format_float: string -> float -> string = "caml_format_float"
+
+
+    
+let gprintf (finish : doc -> 'b)  
+            (format : ('a, unit, doc, 'b) format4) : 'a =
+  let format = (Obj.magic format : string) in
+
+  (* Record the starting align depth *)
+  let startAlignDepth = !alignDepth in
+  (* Special concatenation functions *)
+  let dconcat (acc: doc) (another: doc) = 
+    if !alignDepth > !printDepth then acc else acc ++ another in
+  let dctext1 (acc: doc) (str: string) = 
+    if !alignDepth > !printDepth then acc else 
+    CText(acc, str)
+  in
+  (* Special finish function *)
+  let dfinish (dc: doc) : 'b = 
+    if !alignDepth <> startAlignDepth then
+      prerr_string ("Unmatched align/unalign in " ^ format ^ "\n");
+    finish dc
+  in
+  let flen    = String.length format in
+                                        (* Reading a format character *)
+  let fget    = String.unsafe_get format in
+                                        (* Output a literal sequence of 
+                                         * characters, starting at i. The 
+                                         * character at i does not need to be 
+                                         * checked.  *) 
+  let rec literal acc i = 
+    let rec skipChars j = 
+      if j >= flen || 
+      (match fget j with 
+        '%' -> true 
+      | '@' -> true 
+      | '\n' -> true
+      | _ -> false) then
+        collect (dctext1 acc (String.sub format i (j-i))) j
+      else
+        skipChars (succ j)
+    in
+    skipChars (succ i)
+                                        (* the main collection function *)
+  and collect (acc: doc) (i: int) = 
+    if i >= flen then begin
+      Obj.magic (dfinish acc) 
+    end else begin
+      let c = fget i in
+      if c = '%' then begin
+        let j = skip_args (succ i) in
+        match fget j with
+          '%' -> literal acc j 
+        | 's' ->
+            Obj.magic(fun s ->
+              let str = 
+                if j <= i+1 then
+                  s
+                else
+                  let sl = String.length s in
+                  let p =
+                    try
+                      int_of_string (String.sub format (i+1) (j-i-1))
+                    with _ ->
+                      invalid_arg "fprintf: bad %s format" in
+                  if p > 0 && sl < p then
+                    (String.make (p - sl) ' ') ^ s
+                  else if p < 0 && sl < -p then
+                    s ^ (String.make (-p - sl) ' ')
+                  else
+                    s
+              in
+              collect (breakString acc str) (succ j))
+        | 'c' ->
+            Obj.magic(fun c ->
+              collect (dctext1 acc (String.make 1 c)) (succ j))
+        | 'd' | 'i' | 'o' | 'x' | 'X' | 'u' ->
+            Obj.magic(fun n ->
+              collect (dctext1 acc
+                         (format_int (String.sub format i 
+                                                  (j-i+1)) n))
+                (succ j))
+    (* L, l, and n are the Int64, Int32, and Nativeint modifiers to the integer
+       formats d,i,o,x,X,u.  For example, %Lo means print an Int64 in octal.*)
+	| 'L' ->
+	    if j != i + 1 then  (*Int64.format handles simple formats like %d.
+                     * Any special flags eaten by skip_args will confuse it. *)
+              invalid_arg ("dprintf: unimplemented format " 
+			   ^ (String.sub format i (j-i+1)));
+	    let j' = succ j in (* eat the d,i,x etc. *)
+	    let format_spec = "% " in
+	    String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *)
+            Obj.magic(fun n ->
+              collect (dctext1 acc
+                         (Int64.format format_spec n))
+                (succ j'))
+	| 'l' ->
+	    if j != i + 1 then invalid_arg ("dprintf: unimplemented format " 
+					    ^ (String.sub format i (j-i+1)));
+	    let j' = succ j in (* eat the d,i,x etc. *)
+	    let format_spec = "% " in
+	    String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *)
+            Obj.magic(fun n ->
+              collect (dctext1 acc
+                         (Int32.format format_spec n))
+                (succ j'))
+	| 'n' ->
+	    if j != i + 1 then invalid_arg ("dprintf: unimplemented format " 
+					    ^ (String.sub format i (j-i+1)));
+	    let j' = succ j in (* eat the d,i,x etc. *)
+	    let format_spec = "% " in
+	    String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *)
+            Obj.magic(fun n ->
+              collect (dctext1 acc
+                         (Nativeint.format format_spec n))
+                (succ j'))
+        | 'f' | 'e' | 'E' | 'g' | 'G' ->
+            Obj.magic(fun f ->
+              collect (dctext1 acc
+                         (format_float (String.sub format i (j-i+1)) f))
+                (succ j))
+        | 'b' | 'B' ->
+            Obj.magic(fun b ->
+              collect (dctext1 acc (string_of_bool b)) (succ j))
+        | 'a' ->
+            Obj.magic(fun pprinter arg ->
+              collect (dconcat acc (pprinter () arg)) (succ j))
+        | 't' ->
+            Obj.magic(fun pprinter ->
+              collect (dconcat acc (pprinter ())) (succ j))
+        | c ->
+            invalid_arg ("dprintf: unknown format %s" ^ String.make 1 c)
+
+      end else if c = '@' then begin
+        if i + 1 < flen then begin
+          match fget (succ i) with
+
+                                        (* Now the special format characters *)
+            '[' ->                      (* align *)
+              let newacc = 
+                if !alignDepth > !printDepth then
+                  acc
+                else if !alignDepth = !printDepth then
+                  CText(acc, "...")
+                else
+                  acc ++ align
+              in
+              incr alignDepth;
+              collect newacc (i + 2)
+                
+          | ']' ->                        (* unalign *)
+              decr alignDepth;
+              let newacc = 
+                if !alignDepth >= !printDepth then
+                  acc
+                else
+                  acc ++ unalign
+              in
+              collect newacc (i + 2)
+          | '!' ->                        (* hard-line break *)
+              collect (dconcat acc line) (i + 2)
+          | '?' ->                        (* soft line break *)
+              collect (dconcat acc (break)) (i + 2)
+          | '<' -> 
+              collect (dconcat acc mark) (i +1)
+          | '>' -> 
+              collect (dconcat acc unmark) (i +1)
+	  | '^' ->                        (* left-flushed *)
+	      collect (dconcat acc (leftflush)) (i + 2)
+          | '@' -> 
+              collect (dctext1 acc "@") (i + 2)
+          | c ->
+              invalid_arg ("dprintf: unknown format @" ^ String.make 1 c)
+        end else
+          invalid_arg "dprintf: incomplete format @"
+      end else if c = '\n' then begin
+        collect (dconcat acc line) (i + 1)
+      end else
+        literal acc i
+    end
+
+  and skip_args j =
+    match String.unsafe_get format j with
+      '0' .. '9' | ' ' | '.' | '-' -> skip_args (succ j)
+    | c -> j
+
+  in
+  collect Nil 0
+
+let withPrintDepth dp thunk = 
+  let opd = !printDepth in
+  printDepth := dp;
+  thunk ();
+  printDepth := opd
+
+
+
+let flushOften = ref false
+
+let dprintf format     = gprintf (fun x -> x) format
+let fprintf chn format = 
+  let f d = fprint chn 80 d; d in
+	(* weimeric hack begins -- flush output to streams *)
+  let res = gprintf f format in
+	(* save the value we would have returned, flush the channel and then 
+         * return it -- this allows us to see debug input near infinite loops 
+         * *)
+  if !flushOften then flush chn;
+  res
+	(* weimeric hack ends *)
+
+let printf format = fprintf stdout format
+let eprintf format = fprintf stderr format
+
+
+
+(******************************************************************************)
+let getAlgoName = function
+    George -> "George"
+  | Aman   -> "Aman"
+  | Gap    -> "Gap"
+
+let getAboutString () : string =
+  "(Pretty: ALGO=" ^ (getAlgoName algo) ^ ")"
+
+
+(************************************************)
+let auto_printer (typ: string) = 
+  failwith ("Pretty.auto_printer \"" ^ typ ^ "\" only works with you use -pp \"camlp4o pa_prtype.cmo\" when you compile")
diff --git a/cil/ocamlutil/pretty.mli b/cil/ocamlutil/pretty.mli
new file mode 100644
index 00000000..5422432d
--- /dev/null
+++ b/cil/ocamlutil/pretty.mli
@@ -0,0 +1,316 @@
+(*
+ *
+ * Copyright (c) 2001 by
+ *  George C. Necula	necula@cs.berkeley.edu
+ *  Scott McPeak        smcpeak@cs.berkeley.edu
+ *  Wes Weimer          weimer@cs.berkeley.edu
+ *   
+ * All rights reserved.  Permission to use, copy, modify and distribute
+ * this software for research purposes only is hereby granted, 
+ * 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 name of the authors may not be used to endorse or promote products 
+ * derived from  this software without specific prior written permission. 
+ *
+ * DISCLAIMER:
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.
+ *
+ *)
+
+(** Utility functions for pretty-printing. The major features provided by 
+    this module are 
+- An [fprintf]-style interface with support for user-defined printers
+- The printout is fit to a width by selecting some of the optional newlines
+- Constructs for alignment and indentation
+- Print ellipsis starting at a certain nesting depth
+- Constructs for printing lists and arrays
+
+ Pretty-printing occurs in two stages:
+- Construct a {!Pretty.doc} object that encodes all of the elements to be 
+  printed 
+  along with alignment specifiers and optional and mandatory newlines
+- Format the {!Pretty.doc} to a certain width and emit it as a string, to an 
+  output stream or pass it to a user-defined function
+
+ The formatting algorithm is not optimal but it does a pretty good job while 
+ still operating in linear time. The original version was based on a pretty 
+ printer by Philip Wadler which turned out to not scale to large jobs. 
+*)
+
+(** API *)
+
+(** The type of unformated documents. Elements of this type can be 
+ * constructed in two ways. Either with a number of constructor shown below, 
+ * or using the {!Pretty.dprintf} function with a [printf]-like interface. 
+ * The {!Pretty.dprintf} method is slightly slower so we do not use it for 
+ * large jobs such as the output routines for a compiler. But we use it for 
+ * small jobs such as logging and error messages. *)
+type doc
+
+
+
+(** Constructors for the doc type. *)
+
+
+
+
+(** Constructs an empty document *)
+val nil          : doc
+
+
+(** Concatenates two documents. This is an infix operator that associates to 
+    the left. *)
+val (++)         : doc -> doc -> doc 
+val concat       : doc -> doc -> doc
+
+(** A document that prints the given string *)
+val text         : string -> doc
+
+
+(** A document that prints an integer in decimal form *)
+val num          : int    -> doc
+
+
+(** A document that prints a real number *)
+val real         : float  -> doc
+
+(** A document that prints a character. This is just like {!Pretty.text}
+    with a one-character string. *)
+val chr          : char   -> doc
+
+
+(** A document that consists of a mandatory newline. This is just like [(text
+    "\n")]. The new line will be indented to the current indentation level,
+    unless you use {!Pretty.leftflush} right after this. *)
+val line         : doc
+
+(** Use after a {!Pretty.line} to prevent the indentation. Whatever follows 
+ * next will be flushed left. Indentation resumes on the next line. *)
+val leftflush    : doc
+
+
+(** A document that consists of either a space or a line break. Also called
+    an optional line break. Such a break will be
+    taken only if necessary to fit the document in a given width. If the break
+    is not taken a space is printed instead. *)
+val break: doc
+
+(** Mark the current column as the current indentation level. Does not print
+    anything. All taken line breaks will align to this column. The previous
+    alignment level is saved on a stack. *)
+val align: doc
+
+(** Reverts to the last saved indentation level. *)
+val unalign: doc
+
+
+(** Mark the beginning of a markup section. The width of a markup section is 
+ * considered 0 for the purpose of computing identation *)
+val mark: doc
+
+(** The end of a markup section *)
+val unmark: doc
+
+(************* Now some syntactic sugar *****************)
+(** Syntactic sugar *)
+
+(** Indents the document. Same as [((text "  ") ++ align ++ doc ++ unalign)],
+    with the specified number of spaces. *)
+val indent: int -> doc -> doc
+
+(** Prints a document as markup. The marked document cannot contain line 
+ * breaks or alignment constructs. *)
+val markup: doc -> doc
+
+(** Formats a sequence. [sep] is a separator, [doit] is a function that 
+ * converts an element to a document. *)
+val seq: sep:doc -> doit:('a ->doc) -> elements:'a list -> doc
+
+
+(** An alternative function for printing a list. The [unit] argument is there 
+ * to make this function more easily usable with the {!Pretty.dprintf} 
+ * interface. The first argument is a separator, by default a comma. *)
+val docList: ?sep:doc -> ('a -> doc) -> unit -> 'a list -> doc
+
+(** sm: Yet another list printer.  This one accepts the same kind of
+  * printing function that {!Pretty.dprintf} does, and itself works 
+  * in the dprintf context.  Also accepts
+  * a string as the separator since that's by far the most common.  *)
+val d_list: string -> (unit -> 'a -> doc) -> unit -> 'a list -> doc
+
+(** Formats an array. A separator and a function that prints an array
+    element. The default separator is a comma. *)
+val docArray: ?sep:doc -> (int -> 'a -> doc) -> unit -> 'a array -> doc
+
+(** Prints an ['a option] with [None] or [Some] *)
+val docOpt: ('a -> doc) -> unit -> 'a option -> doc
+
+
+(** Print an int32 *)
+val d_int32: int32 -> doc
+val f_int32: unit -> int32 -> doc
+
+val d_int64: int64 -> doc
+val f_int64: unit -> int64 -> doc
+
+(** Format maps. *)
+module MakeMapPrinter :
+  functor (Map: sig
+                  type key
+                  type 'a t
+                  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+                end) ->
+sig
+    (** Format a map, analogous to docList. *)
+    val docMap: ?sep:doc -> (Map.key -> 'a -> doc) -> unit -> 'a Map.t -> doc
+
+    (** Format a map, analogous to d_list. *)
+    val d_map: ?dmaplet:(doc -> doc -> doc)
+               -> string
+               -> (unit -> Map.key -> doc)
+               -> (unit -> 'a -> doc)
+               -> unit
+               -> 'a Map.t
+               -> doc
+  end
+
+(** Format sets. *)
+module MakeSetPrinter :
+  functor (Set: sig 
+                  type elt
+                  type t
+                  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+                end) ->
+sig
+    (** Format a set, analogous to docList. *)
+    val docSet: ?sep:doc -> (Set.elt -> doc) -> unit -> Set.t -> doc
+
+    (** Format a set, analogous to d_list. *)
+    val d_set: string
+               -> (unit -> Set.elt -> doc)
+               -> unit
+               -> Set.t
+               -> doc
+end
+
+(** A function that is useful with the [printf]-like interface *)
+val insert: unit -> doc -> doc
+
+val dprintf: ('a, unit, doc, doc) format4 -> 'a  
+(** This function provides an alternative method for constructing 
+    [doc] objects. The first argument for this function is a format string 
+    argument (of type [('a, unit, doc) format]; if you insist on 
+    understanding what that means see the module [Printf]). The format string 
+    is like that for the [printf] function in C, except that it understands a 
+    few more formatting controls, all starting with the @ character. 
+
+    See the gprintf function if you want to pipe the result of dprintf into 
+    some other functions.
+
+ The following special formatting characters are understood (these do not 
+ correspond to arguments of the function):
+-  @\[ Inserts an {!Pretty.align}. Every format string must have matching 
+        {!Pretty.align} and {!Pretty.unalign}. 
+-  @\] Inserts an {!Pretty.unalign}.
+-  @!  Inserts a {!Pretty.line}. Just like "\n"
+-  @?  Inserts a {!Pretty.break}.
+-  @<  Inserts a {!Pretty.mark}. 
+-  @>  Inserts a {!Pretty.unmark}.
+-  @^  Inserts a {!Pretty.leftflush}
+       Should be used immediately after @! or "\n".
+-  @@ : inserts a @ character
+
+ In addition to the usual [printf] % formatting characters the following two 
+ new characters are supported:
+- %t Corresponds to an argument of type [unit -> doc]. This argument is 
+     invoked to produce a document
+- %a Corresponds to {b two} arguments. The first of type [unit -> 'a -> doc] 
+     and the second of type ['a]. (The extra [unit] is do to the 
+     peculiarities of the built-in support for format strings in Ocaml. It 
+     turns out that it is not a major problem.) Here is an example of how 
+     you use this:
+
+{v dprintf "Name=%s, SSN=%7d, Children=\@\[%a\@\]\n"
+             pers.name pers.ssn (docList (chr ',' ++ break) text)
+             pers.children v}
+
+ The result of [dprintf] is a {!Pretty.doc}. You can format the document and 
+ emit it using the functions {!Pretty.fprint} and {!Pretty.sprint}.
+
+*)
+
+(** Like {!Pretty.dprintf} but more general. It also takes a function that is 
+ * invoked on the constructed document but before any formatting is done. The 
+ * type of the format argument means that 'a is the type of the parameters of 
+ * this function, unit is the type of the first argument to %a and %t 
+ * formats, doc is the type of the intermediate result, and 'b is the type of 
+ * the result of gprintf. *)
+val gprintf: (doc -> 'b) -> ('a, unit, doc, 'b) format4 -> 'a
+
+(** Format the document to the given width and emit it to the given channel *)
+val fprint: out_channel -> width:int -> doc -> unit
+
+(** Format the document to the given width and emit it as a string *)
+val sprint: width:int -> doc -> string
+
+(** Like {!Pretty.dprintf} followed by {!Pretty.fprint} *)
+val fprintf: out_channel -> ('a, unit, doc) format -> 'a  
+
+(** Like {!Pretty.fprintf} applied to [stdout] *)
+val printf: ('a, unit, doc) format -> 'a 
+
+(** Like {!Pretty.fprintf} applied to [stderr] *)
+val eprintf: ('a, unit, doc) format -> 'a 
+
+                                                                     
+(* sm: arg!  why can't I write this function?! *)
+(* * Like {!Pretty.dprintf} but yielding a string with no newlines *)
+(*val sprintf: (doc, unit, doc) format -> string*)
+
+(* sm: different tack.. *)
+(* doesn't work either.  well f it anyway *)
+(*val failwithf: ('a, unit, doc) format -> 'a*)
+
+
+(** Invokes a thunk, with printDepth temporarily set to the specified value *)
+val withPrintDepth : int -> (unit -> unit) -> unit
+
+(** The following variables can be used to control the operation of the printer *)
+
+(** Specifies the nesting depth of the [align]/[unalign] pairs at which 
+    everything is replaced with ellipsis *)
+val printDepth   : int ref
+
+val printIndent  : bool ref  (** If false then does not indent *)
+
+
+(** If set to [true] then optional breaks are taken only when the document 
+    has exceeded the given width. This means that the printout will looked 
+    more ragged but it will be faster *)
+val fastMode  : bool ref 
+
+val flushOften   : bool ref  (** If true the it flushes after every print *)
+
+
+(** Keep a running count of the taken newlines. You can read and write this 
+  * from the client code if you want *)
+val countNewLines : int ref
+
+
+(** A function that when used at top-level in a module will direct 
+ * the pa_prtype module generate automatically the printing functions for a 
+ * type *)
+val auto_printer: string -> 'b
diff --git a/cil/ocamlutil/stats.ml b/cil/ocamlutil/stats.ml
new file mode 100644
index 00000000..8bbb7d05
--- /dev/null
+++ b/cil/ocamlutil/stats.ml
@@ -0,0 +1,146 @@
+(* The following functions are implemented in perfcount.c *) 
+
+(* Returns true is we have the performance counters *)
+external has_performance_counters: unit -> bool = "has_performance_counters"
+
+(* Returns number of seconds since the first read *)
+external read_pentium_perfcount : unit -> float = "read_pentium_perfcount"
+
+(* Returns current cycle counter, divided by 1^20, and truncated to 30 bits *)
+external sample_pentium_perfcount_20 : unit -> int = "sample_pentium_perfcount_20"
+
+(* Returns current cycle counter, divided by 1^10, and truncated to 30 bits *)
+external sample_pentium_perfcount_10 : unit -> int = "sample_pentium_perfcount_10"
+
+
+(* Whether to use the performance counters (on Pentium only) *)
+
+(* The performance counters are disabled by default. *)
+let do_use_performance_counters = ref false
+
+                                        (* A hierarchy of timings *)
+
+type t = { name : string;
+           mutable time : float; (* In seconds *)
+           mutable sub  : t list}
+
+                                        (* Create the top level *)
+let top = { name = "TOTAL";
+            time = 0.0;
+            sub  = []; }
+
+                                        (* The stack of current path through 
+                                         * the hierarchy. The first is the 
+                                         * leaf. *)
+let current : t list ref = ref [top]
+
+exception NoPerfCount
+let reset (perfcount: bool) = 
+  top.sub <- [];
+  if perfcount then begin
+    if not (has_performance_counters ()) then begin
+      raise NoPerfCount
+    end
+  end;
+  do_use_performance_counters := perfcount
+
+
+
+let print chn msg = 
+  (* Total up *)
+  top.time <- List.fold_left (fun sum f -> sum +. f.time) 0.0 top.sub;
+  let rec prTree ind node = 
+    if !do_use_performance_counters then 
+      (Printf.fprintf chn "%s%-20s          %8.5f s\n" 
+         (String.make ind ' ') node.name node.time)
+    else
+      (Printf.fprintf chn "%s%-20s          %6.3f s\n" 
+         (String.make ind ' ') node.name node.time);
+
+   List.iter (prTree (ind + 2)) (List.rev node.sub)
+  in
+  Printf.fprintf chn "%s" msg; 
+  List.iter (prTree 0) [ top ];
+  Printf.fprintf chn "Timing used %s\n"
+    (if !do_use_performance_counters then "Pentium performance counters"
+     else "Unix.time");
+  let gc = Gc.quick_stat () in 
+  let printM (w: float) : string = 
+    Printf.sprintf "%.2fMb" (w *. 4.0 /. 1000000.0)
+  in
+  Printf.fprintf chn 
+    "Memory statistics: total=%s, max=%s, minor=%s, major=%s, promoted=%s\n    minor collections=%d  major collections=%d compactions=%d\n"
+    (printM (gc.Gc.minor_words +. gc.Gc.major_words 
+               -. gc.Gc.promoted_words))
+    (printM (float_of_int gc.Gc.top_heap_words))
+    (printM gc.Gc.minor_words)
+    (printM gc.Gc.major_words)
+    (printM gc.Gc.promoted_words)
+    gc.Gc.minor_collections
+    gc.Gc.major_collections
+    gc.Gc.compactions;
+    
+  ()
+        
+  
+
+(* Get the current time, in seconds *)
+let get_current_time () : float = 
+  if !do_use_performance_counters then 
+    read_pentium_perfcount ()
+  else
+    (Unix.times ()).Unix.tms_utime
+
+let repeattime limit str f arg = 
+                                        (* Find the right stat *)
+  let stat : t = 
+    let curr = match !current with h :: _ -> h | _ -> assert false in
+    let rec loop = function
+        h :: _ when h.name = str -> h
+      | _ :: rest -> loop rest
+      | [] -> 
+          let nw = {name = str; time = 0.0; sub = []} in
+          curr.sub <- nw :: curr.sub;
+          nw
+    in
+    loop curr.sub
+  in
+  let oldcurrent = !current in
+  current := stat :: oldcurrent;
+  let start = get_current_time () in
+  let rec repeatf count = 
+    let res   = f arg in
+    let diff = get_current_time () -. start in
+    if diff < limit then
+      repeatf (count + 1)
+    else begin
+      stat.time <- stat.time +. (diff /. float(count));
+      current := oldcurrent;                (* Pop the current stat *)
+      res                                   (* Return the function result *)
+    end
+  in
+  repeatf 1
+
+
+let time str f arg = repeattime 0.0 str f arg
+    
+
+let lastTime = ref 0.0
+let timethis (f: 'a -> 'b) (arg: 'a) : 'b = 
+  let start = get_current_time () in
+  let res = f arg in 
+  lastTime := get_current_time () -. start; 
+  res
+  
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/cil/ocamlutil/stats.mli b/cil/ocamlutil/stats.mli
new file mode 100644
index 00000000..9ed98e56
--- /dev/null
+++ b/cil/ocamlutil/stats.mli
@@ -0,0 +1,72 @@
+(*
+ *
+ * Copyright (c) 2001 by
+ *  George C. Necula	necula@cs.berkeley.edu
+ *  Scott McPeak        smcpeak@cs.berkeley.edu
+ *  Wes Weimer          weimer@cs.berkeley.edu
+ *   
+ * All rights reserved.  Permission to use, copy, modify and distribute
+ * this software for research purposes only is hereby granted, 
+ * 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 name of the authors may not be used to endorse or promote products 
+ * derived from  this software without specific prior written permission. 
+ *
+ * DISCLAIMER:
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.
+ *
+ *)
+
+(** Utilities for maintaining timing statistics *)
+
+(** Resets all the timings. Invoke with "true" if you want to switch to using 
+ * the hardware performance counters from now on. You get an exception if 
+ * there are not performance counters available *)
+val reset: bool -> unit
+exception NoPerfCount
+
+(** Check if we have performance counters *)
+val has_performance_counters: unit -> bool
+                           
+(** Sample the current cycle count, in megacycles. *)
+val sample_pentium_perfcount_20: unit -> int
+
+(** Sample the current cycle count, in kilocycles. *)
+val sample_pentium_perfcount_10: unit -> int
+
+(** Time a function and associate the time with the given string. If some
+    timing information is already associated with that string, then accumulate
+    the times. If this function is invoked within another timed function then
+    you can have a hierarchy of timings *)
+val time : string -> ('a -> 'b) -> 'a -> 'b 
+
+(** repeattime is like time but runs the function several times until the total
+    running time is greater or equal to the first argument. The total time is
+    then divided by the number of times the function was run. *)
+val repeattime : float -> string -> ('a -> 'b) -> 'a -> 'b
+
+(** Print the current stats preceeded by a message *)
+val print : out_channel -> string -> unit
+
+
+
+(** Time a function and set lastTime to the time it took *)
+val lastTime: float ref
+val timethis: ('a -> 'b) -> 'a -> 'b
+
+
+
+
diff --git a/cil/ocamlutil/trace.ml b/cil/ocamlutil/trace.ml
new file mode 100644
index 00000000..b4292865
--- /dev/null
+++ b/cil/ocamlutil/trace.ml
@@ -0,0 +1,169 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+(* Trace module implementation
+ * see trace.mli
+ *)
+
+open Pretty;;
+
+
+(* --------- traceSubsystems --------- *)
+(* this is the list of tags (usually subsystem names) for which
+ * trace output will appear *)
+let traceSubsystems : string list ref = ref [];;
+
+
+let traceAddSys (subsys : string) : unit =
+  (* (ignore (printf "traceAddSys %s\n" subsys)); *)
+  traceSubsystems := subsys :: !traceSubsystems
+;;
+
+
+let traceActive (subsys : string) : bool =
+  (* (List.mem elt list) returns true if something in list equals ('=') elt *)
+  (List.mem subsys !traceSubsystems)
+;;
+
+
+let rec parseString (str : string) (delim : char) : string list =
+begin
+  if (not (String.contains str delim)) then 
+    if ((String.length str) = 0) then
+      [] 
+    else
+      [str]
+
+  else
+    let d = ((String.index str delim) + 1) in
+    if (d = 1) then
+      (* leading delims are eaten *)
+      (parseString (String.sub str d ((String.length str) - d)) delim)
+    else
+      (String.sub str 0 (d-1)) ::
+        (parseString (String.sub str d ((String.length str) - d)) delim)
+end;;
+
+let traceAddMulti (systems : string) : unit =
+begin
+  let syslist = (parseString systems ',') in
+  (List.iter traceAddSys syslist)
+end;;
+
+
+
+(* --------- traceIndent --------- *)
+let traceIndentLevel : int ref = ref 0;;
+
+
+let traceIndent (sys : string) : unit =
+  if (traceActive sys) then
+    traceIndentLevel := !traceIndentLevel + 2
+;;
+
+let traceOutdent (sys : string) : unit =
+  if ((traceActive sys) &&
+      (!traceIndentLevel >= 2)) then
+    traceIndentLevel := !traceIndentLevel - 2
+;;
+
+
+(* --------- trace --------- *)
+(* return a tag to prepend to a trace output
+ * e.g. "  %%% mysys: "
+ *)
+let traceTag (sys : string) : Pretty.doc =
+  (* return string of 'i' spaces *)
+  let rec ind (i : int) : string =
+    if (i <= 0) then
+      ""
+    else
+      " " ^ (ind (i-1))
+
+  in
+  (text ((ind !traceIndentLevel) ^ "%%% " ^ sys ^ ": "))
+;;
+
+
+(* this is the trace function; its first argument is a string
+ * tag, and subsequent arguments are like printf formatting
+ * strings ("%a" and whatnot) *)
+let trace
+    (subsys : string)                   (* subsystem identifier for enabling tracing *)
+    (d : Pretty.doc)                    (* something made by 'dprintf' *)
+    : unit =                            (* no return value *)
+  (* (ignore (printf "trace %s\n" subsys)); *)
+
+  (* see if the subsystem's tracing is turned on *)
+  if (traceActive subsys) then
+    begin
+      (fprint stderr 80			(* print it *)
+         ((traceTag subsys) ++ d));	(* with prepended subsys tag *)
+      (* mb: flush after every message; useful if the program hangs in an
+	 infinite loop... *)
+      (flush stderr)
+    end
+  else
+    ()			                         (* eat it *)
+;;
+
+
+let tracei (sys : string) (d : Pretty.doc) : unit =
+  (* trace before indent *)
+  (trace sys d);
+  (traceIndent sys)
+;;
+
+let traceu (sys : string) (d : Pretty.doc) : unit =
+  (* trace after outdent *)
+  (* no -- I changed my mind -- I want trace *then* outdent *)
+  (trace sys d);
+  (traceOutdent sys)
+;;
+
+
+
+
+(* -------------------------- trash --------------------- *)
+(* TRASH START
+
+(* sm: more experimenting *)
+(trace "no" (dprintf "no %d\n" 5));
+(trace "yes" (dprintf "yes %d\n" 6));
+(trace "maybe" (dprintf "maybe %d\n" 7));
+
+TRASH END *)
diff --git a/cil/ocamlutil/trace.mli b/cil/ocamlutil/trace.mli
new file mode 100644
index 00000000..46ca6523
--- /dev/null
+++ b/cil/ocamlutil/trace.mli
@@ -0,0 +1,106 @@
+(*
+ *
+ * Copyright (c) 2001-2002, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ *  Scott McPeak        <smcpeak@cs.berkeley.edu>
+ *  Wes Weimer          <weimer@cs.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.
+ *
+ *)
+
+(* Trace module
+ * Scott McPeak, 5/4/00
+ *
+ * The idea is to pepper the source with debugging printfs,
+ * and be able to select which ones to actually display at
+ * runtime.
+ *
+ * It is built on top of the Pretty module for printing data
+ * structures.
+ *
+ * To a first approximation, this is needed to compensate for
+ * the lack of a debugger that does what I want...
+ *)
+
+
+(* this is the list of tags (usually subsystem names) for which
+ * trace output will appear *)
+val traceSubsystems : string list ref
+
+(* interface to add a new subsystem to trace (slightly more
+ * convenient than direclty changing 'tracingSubsystems') *)
+val traceAddSys : string -> unit
+
+(* query whether a particular subsystem is being traced *)
+val traceActive : string -> bool
+   
+(* add several systems, separated by commas *)
+val traceAddMulti : string -> unit
+
+
+(* current indentation level for tracing *)
+val traceIndentLevel : int ref
+
+(* bump up or down the indentation level, if the given subsys
+ * is being traced *)
+val traceIndent : string -> unit
+val traceOutdent : string -> unit
+
+
+(* this is the trace function; its first argument is a string
+ * tag, and second argument is a 'doc' (which is what 'dprintf'
+ * returns).
+ *
+ * so a sample usage might be
+ *   (trace "mysubsys" (dprintf "something neat happened %d times\n" counter))
+ *)
+val trace : string -> Pretty.doc -> unit
+
+
+(* special flavors that indent/outdent as well.  the indent version
+ * indents *after* printing, while the outdent version outdents
+ * *before* printing.  thus, a sequence like
+ *
+ *   (tracei "foo" (dprintf "beginning razzle-dazzle\n"))
+ *     ..razzle..
+ *     ..dazzle..
+ *   (traceu "foo" (dprintf "done with razzle-dazzle\n"))
+ *
+ * will do the right thing
+ *
+ * update -- I changed my mind!  I decided I prefer it like this
+ *   %%% sys: (myfunc args)
+ *     %%% ...inner stuff...
+ *     %%% sys: myfunc returning 56
+ *
+ * so now they both print before in/outdenting
+ *)
+val tracei : string -> Pretty.doc -> unit
+val traceu : string -> Pretty.doc -> unit
diff --git a/cil/ocamlutil/util.ml b/cil/ocamlutil/util.ml
new file mode 100755
index 00000000..e6c2c679
--- /dev/null
+++ b/cil/ocamlutil/util.ml
@@ -0,0 +1,815 @@
+(** Utility functions for Coolaid *)
+module E = Errormsg
+module H = Hashtbl
+module IH = Inthash
+
+open Pretty
+
+exception GotSignal of int
+
+let withTimeout (secs: float) (* Seconds for timeout *)
+                (handler: int -> 'b) (* What to do if we have a timeout. The 
+                                        * argument passed is the signal number 
+                                        * received. *)
+                (f: 'a -> 'b) (* The function to run *)
+                (arg: 'a) (* And its argument *)
+   : 'b = 
+  let oldHandler = 
+    Sys.signal Sys.sigalrm 
+      (Sys.Signal_handle 
+         (fun i -> 
+           ignore (E.log "Got signal %d\n" i);
+           raise (GotSignal i)))
+  in
+  let reset_sigalrm () = 
+    ignore (Unix.setitimer Unix.ITIMER_REAL { Unix.it_value = 0.0;
+                                              Unix.it_interval = 0.0;});
+    Sys.set_signal Sys.sigalrm oldHandler;
+  in
+  ignore (Unix.setitimer Unix.ITIMER_REAL 
+            { Unix.it_value    = secs;
+              Unix.it_interval = 0.0;});
+  (* ignore (Unix.alarm 2); *)
+  try
+    let res = f arg in 
+    reset_sigalrm ();
+    res
+  with exc -> begin
+    reset_sigalrm ();
+    ignore (E.log "Got an exception\n");
+    match exc with 
+      GotSignal i -> 
+        handler i
+    | _ -> raise exc
+  end
+
+(** Print a hash table *)
+let docHash ?(sep=chr ',') (one: 'a -> 'b -> doc) () (h: ('a, 'b) H.t) = 
+  (H.fold 
+     (fun key data acc -> 
+       if acc == align then acc ++ one key data
+       else acc ++ sep ++ one key data)
+     h
+     align) ++ unalign
+    
+
+
+let hash_to_list (h: ('a, 'b) H.t) : ('a * 'b) list =
+  H.fold
+    (fun key data acc -> (key, data) :: acc)
+    h
+    []
+
+let keys (h: ('a, 'b) H.t) : 'a list =
+  H.fold
+    (fun key data acc -> key :: acc)
+    h
+    []
+
+let hash_copy_into (hfrom: ('a, 'b) H.t) (hto: ('a, 'b) H.t) : unit = 
+  H.clear hto;
+  H.iter (H.add hto) hfrom
+
+let anticompare a b = compare b a
+;;
+
+
+let rec list_drop (n : int) (xs : 'a list) : 'a list =
+  if n < 0 then invalid_arg "Util.list_drop";
+  if n = 0 then 
+    xs
+  else begin 
+    match xs with
+    | [] -> invalid_arg "Util.list_drop"
+    | y::ys -> list_drop (n-1) ys
+  end
+
+let list_droptail (n : int) (xs : 'a list) : 'a list =
+  if n < 0 then invalid_arg "Util.list_droptail";
+  let (ndrop,r) =
+    List.fold_right
+      (fun x (ndrop,acc) ->
+	if ndrop = 0 then (ndrop, x :: acc)
+	else (ndrop-1, acc))
+      xs
+      (n,[])
+  in
+  if ndrop > 0 then invalid_arg "Util.listdroptail"
+  else r
+
+let rec list_span (p : 'a -> bool) (xs : 'a list) : 'a list * 'a list = 
+  begin match xs with
+  | [] -> ([],[])
+  | x::xs' -> 
+      if p x then
+        let (ys,zs) = list_span p xs' in (x::ys,zs)
+      else ([],xs)
+  end
+;;
+
+let rec list_rev_append revxs ys =
+  begin match revxs with
+  | [] -> ys
+  | x::xs -> list_rev_append xs (x::ys)
+  end
+;;
+let list_insert_by (cmp : 'a -> 'a -> int) 
+    (x : 'a) (xs : 'a list) : 'a list =
+  let rec helper revhs ts =
+    begin match ts with
+    | [] -> List.rev (x::revhs)
+    | t::ts' -> 
+        if cmp x t >= 0 then helper (t::revhs) ts'
+        else list_rev_append (x::revhs) ts
+    end
+  in
+  helper [] xs
+;;
+
+let list_head_default (d : 'a) (xs : 'a list) : 'a =
+  begin match xs with
+  | [] -> d
+  | x::_ -> x
+  end
+;;
+
+let rec list_iter3 f xs ys zs =
+  begin match xs, ys, zs with
+  | [], [], [] -> ()
+  | x::xs, y::ys, z::zs -> f x y z; list_iter3 f xs ys zs
+  | _ -> invalid_arg "Util.list_iter3"
+  end
+;;
+  
+let rec get_some_option_list (xs : 'a option list) : 'a list =
+  begin match xs with
+  | [] -> []
+  | None::xs  -> get_some_option_list xs
+  | Some x::xs -> x :: get_some_option_list xs
+  end
+;;
+
+(* tail-recursive append: reverses xs twice *)
+let list_append (xs: 'a list) (ys: 'a list): 'a list =
+  match xs with (* optimize some common cases *)
+      [] -> ys
+    | [x] -> x::ys
+    | _ -> list_rev_append (List.rev xs) ys
+
+let list_iteri (f: int -> 'a -> unit) (l: 'a list) : unit = 
+  let rec loop (i: int) (l: 'a list) : unit = 
+    match l with 
+      [] -> ()
+    | h :: t -> f i h; loop (i + 1) t
+  in
+  loop 0 l
+
+let list_mapi (f: int -> 'a -> 'b) (l: 'a list) : 'b list = 
+  let rec loop (i: int) (l: 'a list) : 'b list = 
+    match l with 
+      [] -> []
+    | h :: t -> 
+	let headres = f i h in
+	headres :: loop (i + 1) t
+  in
+  loop 0 l
+
+let list_fold_lefti (f: 'acc -> int -> 'a -> 'acc) (start: 'acc) 
+                   (l: 'a list) : 'acc = 
+  let rec loop (i, acc) l = 
+    match l with
+      [] -> acc
+    | h :: t -> loop (i + 1, f acc i h) t
+  in
+  loop (0, start) l
+
+
+let list_init (len : int) (init_fun : int -> 'a) : 'a list =
+  let rec loop n acc =
+    if n < 0 then acc
+    else loop (n-1) ((init_fun n)::acc)
+  in
+  loop (len - 1) []
+;;
+
+
+let rec list_find_first (l: 'a list) (f: 'a -> 'b option) : 'b option = 
+  match l with 
+    [] -> None
+  | h :: t -> begin
+      match f h with 
+        None -> list_find_first t f
+      | r -> r
+  end
+  
+(** Generates the range of integers starting with a and ending with b *)
+let int_range_list (a: int) (b: int) = 
+  list_init (b - a + 1) (fun i -> a + i)
+
+
+(** Some handling of registers *)
+type 'a growArrayFill =
+    Elem of 'a
+  | Susp of (int -> 'a)
+
+type 'a growArray = {
+            gaFill: 'a growArrayFill;
+            (** Stuff to use to fill in the array as it grows *)
+
+    mutable gaMaxInitIndex: int;
+            (** Maximum index that was written to. -1 if no writes have 
+             * been made.  *)
+
+    mutable gaData: 'a array;
+  } 
+
+let growTheArray (ga: 'a growArray) (len: int) 
+                 (toidx: int) (why: string) : unit = 
+  if toidx >= len then begin
+    (* Grow the array by 50% *)
+    let newlen = toidx + 1 + len  / 2 in
+(*
+    ignore (E.log "growing an array to idx=%d (%s)\n" toidx why);
+*)
+    let data' = begin match ga.gaFill with
+      Elem x ->
+
+	let data'' = Array.create newlen x in
+	Array.blit ga.gaData 0 data'' 0 len;
+	data''
+    | Susp f -> Array.init newlen
+	  (fun i -> if i < len then ga.gaData.(i) else f i)
+    end
+    in
+    ga.gaData <- data'
+  end
+
+let getReg (ga: 'a growArray) (r: int) : 'a = 
+  let len = Array.length ga.gaData in
+  if r >= len then 
+    growTheArray ga len r "get";
+
+  ga.gaData.(r)
+
+let setReg (ga: 'a growArray) (r: int) (what: 'a) : unit = 
+  let len = Array.length ga.gaData in
+  if r >= len then 
+    growTheArray ga len r "set";
+  if r > ga.gaMaxInitIndex then ga.gaMaxInitIndex <- r;
+  ga.gaData.(r) <- what
+
+let newGrowArray (initsz: int) (fill: 'a growArrayFill) : 'a growArray = 
+  { gaFill = fill;
+    gaMaxInitIndex = -1;
+    gaData = begin match fill with
+      Elem x -> Array.create initsz x
+    | Susp f -> Array.init initsz f
+    end; }
+
+let copyGrowArray (ga: 'a growArray) : 'a growArray = 
+  { ga with gaData = Array.copy ga.gaData } 
+
+let deepCopyGrowArray (ga: 'a growArray) (copy: 'a -> 'a): 'a growArray = 
+  { ga with gaData = Array.map copy ga.gaData } 
+
+
+
+(** Iterate over the initialized elements of the array *)
+let growArray_iteri  (f: int -> 'a -> unit) (ga: 'a growArray) = 
+  for i = 0 to ga.gaMaxInitIndex do 
+    f i ga.gaData.(i)
+  done
+
+
+(** Fold left over the initialized elements of the array *)
+let growArray_foldl (f: 'acc -> 'a -> 'acc) 
+                    (acc: 'acc) (ga: 'a growArray) : 'acc = 
+  let rec loop (acc: 'acc) (idx: int) : 'acc = 
+    if idx > ga.gaMaxInitIndex then 
+      acc
+    else
+      loop (f acc ga.gaData.(idx)) (idx + 1)
+  in
+  loop acc 0
+
+
+
+
+let hasPrefix (prefix: string) (what: string) : bool = 
+  let pl = String.length prefix in
+  try String.sub what 0 pl = prefix 
+  with Invalid_argument _ -> false
+
+
+
+let restoreRef ?(deepCopy=(fun x -> x)) (r: 'a ref) : (unit -> unit) = 
+  let old = deepCopy !r in
+  (fun () -> r := old)
+
+let restoreHash ?deepCopy (h: ('a, 'b) H.t) : (unit -> unit) = 
+  let old = 
+    match deepCopy with 
+      None -> H.copy h 
+    | Some f -> 
+        let old = H.create (H.length h) in 
+        H.iter (fun k d -> H.add old k (f d)) h;
+        old
+  in
+  (fun () -> hash_copy_into old h)
+
+let restoreIntHash ?deepCopy (h: 'a IH.t) : (unit -> unit) = 
+  let old = 
+    match deepCopy with 
+      None -> IH.copy h 
+    | Some f -> 
+        let old = IH.create 13 in 
+        IH.iter (fun k d -> IH.add old k (f d)) h;
+        old
+  in
+  (fun () -> 
+    IH.clear old;
+    IH.iter (fun i k -> IH.add old i k) h)
+
+let restoreArray ?deepCopy (a: 'a array) : (unit -> unit) = 
+  let old = Array.copy a in
+  (match deepCopy with 
+    None -> ()
+  | Some f -> Array.iteri (fun i v -> old.(i) <- f v) old);
+  (fun () -> Array.blit old 0 a 0 (Array.length a))
+
+let runThunks (l: (unit -> unit) list) : (unit -> unit) = 
+  fun () -> List.iter (fun f -> f ()) l
+
+
+
+(* Memoize *)
+let memoize (h: ('a, 'b) Hashtbl.t) 
+            (arg: 'a) 
+            (f: 'a -> 'b) : 'b = 
+  try
+    Hashtbl.find h arg
+  with Not_found -> begin
+    let res = f arg in
+    Hashtbl.add h arg res;
+    res
+  end
+
+(* Just another name for memoize *)
+let findOrAdd h arg f = memoize h arg f
+
+(* A tryFinally function *)
+let tryFinally 
+    (main: 'a -> 'b) (* The function to run *)
+    (final: 'b option -> unit)  (* Something to run at the end *)
+    (arg: 'a) : 'b = 
+  try
+    let res: 'b = main arg in
+    final (Some res);
+    res
+  with e -> begin
+    final None;
+    raise e
+  end
+
+
+
+
+let valOf : 'a option -> 'a = function
+    None -> raise (Failure "Util.valOf")
+  | Some x -> x
+
+(**
+ * An accumulating for loop.
+ *
+ * Initialize the accumulator with init.  The current index and accumulator
+ * from the previous iteration is passed to f.
+ *)
+let fold_for ~(init: 'a) ~(lo: int) ~(hi: int) (f: int -> 'a -> 'a) =
+  let rec forloop i acc =
+    if i > hi then acc
+    else forloop (i+1) (f i acc)
+  in
+  forloop lo init
+
+(************************************************************************)
+
+module type STACK = sig
+  type 'a t
+  (** The type of stacks containing elements of type ['a]. *)
+
+  exception Empty
+  (** Raised when {!Stack.pop} or {!Stack.top} is applied to an empty stack. *)
+
+  val create : unit -> 'a t
+  (** Return a new stack, initially empty. *)
+
+  val push : 'a -> 'a t -> unit
+  (** [push x s] adds the element [x] at the top of stack [s]. *)
+
+  val pop : 'a t -> 'a
+  (** [pop s] removes and returns the topmost element in stack [s],
+     or raises [Empty] if the stack is empty. *)
+
+  val top : 'a t -> 'a
+  (** [top s] returns the topmost element in stack [s],
+     or raises [Empty] if the stack is empty. *)
+  
+  val clear : 'a t -> unit
+  (** Discard all elements from a stack. *)
+  
+  val copy : 'a t -> 'a t
+  (** Return a copy of the given stack. *)
+  
+  val is_empty : 'a t -> bool
+  (** Return [true] if the given stack is empty, [false] otherwise. *)
+  
+  val length : 'a t -> int
+  (** Return the number of elements in a stack. *)
+  
+  val iter : ('a -> unit) -> 'a t -> unit
+  (** [iter f s] applies [f] in turn to all elements of [s],
+     from the element at the top of the stack to the element at the
+     bottom of the stack. The stack itself is unchanged. *)
+end
+
+module Stack = struct
+
+  type 'a t = { mutable length : int;
+                stack : 'a Stack.t; }
+
+  exception Empty
+
+  let create () = { length = 0;
+                    stack = Stack.create(); }
+
+  let push x s =
+    s.length <- s.length + 1;
+    Stack.push x s.stack
+
+  let pop s =
+    s.length <- s.length - 1;
+    Stack.pop s.stack
+
+  let top s =
+    Stack.top s.stack
+
+  let clear s =
+    s.length <- 0;
+    Stack.clear s.stack
+
+  let copy s = { length = s.length;
+		 stack = Stack.copy s.stack; }
+    
+  let is_empty s =
+    Stack.is_empty s.stack
+
+  let length s = s.length
+
+  let iter f s =
+    Stack.iter f s.stack
+
+end
+
+(************************************************************************)
+
+let absoluteFilename (fname: string) = 
+  if Filename.is_relative fname then 
+    Filename.concat (Sys.getcwd ()) fname
+  else
+    fname
+
+
+(* mapNoCopy is like map but avoid copying the list if the function does not 
+ * change the elements. *)
+let rec mapNoCopy (f: 'a -> 'a) = function
+    [] -> []
+  | (i :: resti) as li -> 
+      let i' = f i in
+      let resti' = mapNoCopy f resti in
+      if i' != i || resti' != resti then i' :: resti' else li 
+
+let rec mapNoCopyList (f: 'a -> 'a list) = function
+    [] -> []
+  | (i :: resti) as li -> 
+      let il' = f i in
+      let resti' = mapNoCopyList f resti in
+      match il' with
+        [i'] when i' == i && resti' == resti -> li
+      | _ -> il' @ resti'
+
+
+(* Use a filter function that does not rewrite the list unless necessary *)
+let rec filterNoCopy (f: 'a -> bool) (l: 'a list) : 'a list = 
+  match l with 
+    [] -> []
+  | h :: rest when not (f h) -> filterNoCopy f rest 
+  | h :: rest -> 
+      let rest' = filterNoCopy f rest in
+      if rest == rest' then l else h :: rest'
+
+(** Join a list of strings *)
+let rec joinStrings (sep: string) (sl: string list) = 
+  match sl with 
+    [] -> ""
+  | [s1] -> s1
+  | s1 :: ((_ :: _) as rest) -> s1 ^ sep ^ joinStrings sep rest
+
+
+(************************************************************************
+
+ Configuration 
+
+ ************************************************************************)
+(** The configuration data can be of several types **)
+type configData = 
+    ConfInt of int
+  | ConfBool of bool
+  | ConfFloat of float
+  | ConfString of string
+  | ConfList of configData list
+
+
+(* Store here window configuration file *)
+let configurationData: (string, configData) H.t = H.create 13
+
+let clearConfiguration () = H.clear configurationData
+
+let setConfiguration (key: string) (c: configData) = 
+  H.replace configurationData key c
+
+let findConfiguration (key: string) : configData = 
+  H.find configurationData key 
+
+let findConfigurationInt (key: string) : int = 
+  match findConfiguration key with 
+    ConfInt i -> i
+  | _ -> 
+      ignore (E.warn "Configuration %s is not an integer" key);
+      raise Not_found
+
+let useConfigurationInt (key: string) (f: int -> unit) = 
+  try f (findConfigurationInt key)
+  with Not_found -> ()
+
+let findConfigurationString (key: string) : string = 
+  match findConfiguration key with 
+    ConfString s -> s
+  | _ -> 
+      ignore (E.warn "Configuration %s is not a string" key);
+      raise Not_found
+
+let useConfigurationString (key: string) (f: string -> unit) = 
+  try f (findConfigurationString key)
+  with Not_found -> ()
+
+
+let findConfigurationBool (key: string) : bool = 
+  match findConfiguration key with 
+    ConfBool b -> b
+  | _ -> 
+      ignore (E.warn "Configuration %s is not a boolean" key);
+      raise Not_found
+
+let useConfigurationBool (key: string) (f: bool -> unit) = 
+  try f (findConfigurationBool key)
+  with Not_found -> ()
+
+let findConfigurationList (key: string) : configData list  = 
+  match findConfiguration key with 
+    ConfList l -> l
+  | _ -> 
+      ignore (E.warn "Configuration %s is not a list" key);
+      raise Not_found
+
+let useConfigurationList (key: string) (f: configData list -> unit) = 
+  try f (findConfigurationList key)
+  with Not_found -> ()
+
+
+let saveConfiguration (fname: string) = 
+  (** Convert configuration data to a string, for saving externally *)
+  let configToString (c: configData) : string = 
+    let buff = Buffer.create 80 in
+    let rec loop (c: configData) : unit = 
+      match c with 
+        ConfInt i -> 
+          Buffer.add_char buff 'i';
+          Buffer.add_string buff (string_of_int i);
+          Buffer.add_char buff ';'
+            
+      | ConfBool b -> 
+          Buffer.add_char buff 'b';
+          Buffer.add_string buff (string_of_bool b);
+          Buffer.add_char buff ';'
+            
+      | ConfFloat f -> 
+          Buffer.add_char buff 'f';
+          Buffer.add_string buff (string_of_float f);
+          Buffer.add_char buff ';'
+            
+      | ConfString s -> 
+          if String.contains s '"' then 
+            E.s (E.unimp "Guilib: configuration string contains quotes");
+          Buffer.add_char buff '"';
+          Buffer.add_string buff s;
+          Buffer.add_char buff '"'; (* '"' *)
+          
+      | ConfList l -> 
+          Buffer.add_char buff '[';
+          List.iter loop l;
+          Buffer.add_char buff ']'
+    in
+    loop c;
+    Buffer.contents buff
+  in
+  try 
+    let oc = open_out fname in
+    ignore (E.log "Saving configuration to %s\n" (absoluteFilename fname));
+    H.iter (fun k c -> 
+      output_string oc (k ^ "\n");
+      output_string oc ((configToString c) ^ "\n"))
+      configurationData;
+    close_out oc
+  with _ -> 
+    ignore (E.warn "Cannot open configuration file %s\n" fname)
+
+
+(** Make some regular expressions early *)
+let intRegexp = Str.regexp "i\\([0-9]+\\);"
+let floatRegexp = Str.regexp "f\\([0-9]+\\.[0-9]+\\);"
+let boolRegexp = Str.regexp "b\\(\\(true\\)\\|\\(false\\)\\);"
+let stringRegexp = Str.regexp "\"\\([^\"]*\\)\""
+
+let loadConfiguration (fname: string) : unit = 
+  H.clear configurationData;
+
+  let stringToConfig (s: string) : configData = 
+    let idx = ref 0 in (** the current index *)
+    let l = String.length s in 
+    
+    let rec getOne () : configData = 
+      if !idx >= l then raise Not_found;
+      
+      if Str.string_match intRegexp s !idx then begin
+        idx := Str.match_end ();
+        ConfInt (int_of_string (Str.matched_group 1 s))
+      end else if Str.string_match floatRegexp s !idx then begin
+        idx := Str.match_end ();
+        ConfFloat (float_of_string (Str.matched_group 1 s))
+      end else if Str.string_match boolRegexp s !idx then begin
+        idx := Str.match_end ();
+        ConfBool (bool_of_string (Str.matched_group 1 s))
+      end else if  Str.string_match stringRegexp s !idx then begin
+        idx := Str.match_end ();
+        ConfString (Str.matched_group 1 s)
+      end else if String.get s !idx = '[' then begin
+        (* We are starting a list *)
+        incr idx;
+        let rec loop (acc: configData list) : configData list = 
+          if !idx >= l then begin
+            ignore (E.warn "Non-terminated list in configuration %s" s);
+            raise Not_found
+          end;
+          if String.get s !idx = ']' then begin
+            incr idx;
+            List.rev acc
+          end else
+            loop (getOne () :: acc)
+        in
+        ConfList (loop [])
+      end else begin
+        ignore (E.warn "Bad configuration element in a list: %s\n"
+                  (String.sub s !idx (l - !idx)));
+        raise Not_found
+      end
+    in
+    getOne ()
+  in
+  (try 
+    let ic = open_in fname in
+    ignore (E.log "Loading configuration from %s\n" (absoluteFilename fname));
+    (try 
+      while true do
+        let k = input_line ic in
+        let s = input_line ic in
+        try 
+          let c = stringToConfig s in 
+          setConfiguration k c
+        with Not_found -> ()
+      done
+    with End_of_file -> ());
+    close_in ic;
+  with _ -> () (* no file, ignore *));
+  
+  ()
+
+   
+ 
+(*********************************************************************)
+type symbol = int
+
+(**{ Registering symbol names} *)
+let registeredSymbolNames: (string, symbol) H.t = H.create 113
+let symbolNames: string IH.t = IH.create 113 
+let nextSymbolId = ref 0 
+
+(* When we register symbol ranges, we store a naming function for use later 
+ * when we print the symbol *)
+let symbolRangeNaming: (int * int * (int -> string)) list ref = ref []
+
+(* Reset the symbols. We want to allow the registration of symbols at the 
+ * top-level. This means that we cannot simply clear the hash tables. The 
+ * first time we call "reset" we actually remember the state. *)
+let resetThunk: (unit -> unit) option ref = ref None
+
+let snapshotSymbols () : unit -> unit = 
+  runThunks [ restoreIntHash symbolNames;
+              restoreRef nextSymbolId;
+              restoreHash registeredSymbolNames;
+              restoreRef symbolRangeNaming ]
+
+let resetSymbols () = 
+  match !resetThunk with 
+    None -> resetThunk := Some (snapshotSymbols ())
+  | Some t -> t ()
+  
+
+let dumpSymbols () = 
+  ignore (E.log "Current symbols\n");
+  IH.iter (fun i k -> ignore (E.log " %s -> %d\n" k i)) symbolNames;
+  ()
+
+let newSymbol (n: string) : symbol = 
+  assert(not (H.mem registeredSymbolNames n));
+  let id = !nextSymbolId in
+  incr nextSymbolId;
+  H.add registeredSymbolNames n id;
+  IH.add symbolNames id n;
+  id
+
+let registerSymbolName (n: string) : symbol = 
+  try H.find registeredSymbolNames n
+  with Not_found -> begin
+    newSymbol n
+  end
+
+(** Register a range of symbols. The mkname function will be invoked for 
+ * indices starting at 0 *)
+let registerSymbolRange (count: int) (mkname: int -> string) : symbol = 
+  if count < 0 then E.s (E.bug "registerSymbolRange: invalid counter");
+  let first = !nextSymbolId in
+  nextSymbolId := !nextSymbolId + count;
+  symbolRangeNaming := 
+    (first, !nextSymbolId - 1, mkname) :: !symbolRangeNaming;
+  first
+    
+let symbolName (id: symbol) : string = 
+  try IH.find symbolNames id
+  with Not_found -> 
+    (* Perhaps it is one of the lazily named symbols *)
+    try 
+      let (fst, _, mkname) = 
+        List.find 
+          (fun (fst,lst,_) -> fst <= id && id <= lst) 
+          !symbolRangeNaming in
+      let n = mkname (id - fst) in
+      IH.add symbolNames id n;
+      n
+    with Not_found ->
+      ignore (E.warn "Cannot find the name of symbol %d" id);
+      "symbol" ^ string_of_int id
+
+(************************************************************************)
+
+(** {1 Int32 Operators} *)
+
+module Int32Op = struct
+   exception IntegerTooLarge
+   let to_int (i: int32) = 
+     let i' = Int32.to_int i in (* Silently drop the 32nd bit *)
+     if i = Int32.of_int i' then i'
+     else raise IntegerTooLarge
+
+   let (<%) = (fun x y -> (Int32.compare x y) < 0)
+   let (<=%) = (fun x y -> (Int32.compare x y) <= 0)
+   let (>%) = (fun x y -> (Int32.compare x y) > 0)
+   let (>=%) = (fun x y -> (Int32.compare x y) >= 0)
+   let (<>%) = (fun x y -> (Int32.compare x y) <> 0)
+   
+   let (+%) = Int32.add
+   let (-%) = Int32.sub
+   let ( *% ) = Int32.mul
+   let (/%) = Int32.div
+   let (~-%) = Int32.neg
+
+   (* We cannot use the <<% because it trips camlp4 *)
+   let sll = fun i j -> Int32.shift_left i (to_int j)
+   let (>>%) = fun i j -> Int32.shift_right i (to_int j)
+   let (>>>%) = fun i j -> Int32.shift_right_logical i (to_int j)
+end
+
+
+(*********************************************************************)
+
+let equals x1 x2 : bool =
+  (compare x1 x2) = 0
diff --git a/cil/ocamlutil/util.mli b/cil/ocamlutil/util.mli
new file mode 100644
index 00000000..d701c65f
--- /dev/null
+++ b/cil/ocamlutil/util.mli
@@ -0,0 +1,311 @@
+(** A bunch of generally useful functions *)
+
+exception GotSignal of int
+
+val withTimeout : float -> (* Seconds for timeout *)
+                (int -> 'b) -> (* What to do if we have a timeout. The 
+                                        * argument passed is the signal number 
+                                        * received. *)
+                ('a -> 'b) -> (* The function to run *)
+                'a -> (* And its argument *)
+   'b
+
+val docHash : ?sep:Pretty.doc -> ('a -> 'b -> Pretty.doc) -> unit -> 
+  (('a, 'b) Hashtbl.t) -> Pretty.doc 
+
+
+val hash_to_list: ('a, 'b) Hashtbl.t -> ('a * 'b) list
+
+val keys: ('a, 'b) Hashtbl.t -> 'a list
+
+
+(** Copy a hash table into another *)
+val hash_copy_into: ('a, 'b) Hashtbl.t -> ('a, 'b) Hashtbl.t -> unit
+
+(** First, a few utility functions I wish were in the standard prelude *)
+
+val anticompare: 'a -> 'a -> int
+
+val list_drop : int -> 'a list -> 'a list
+val list_droptail : int -> 'a list -> 'a list
+val list_span: ('a -> bool) -> ('a list) -> 'a list * 'a list
+val list_insert_by: ('a -> 'a -> int) -> 'a -> 'a list -> 'a list
+val list_head_default: 'a -> 'a list -> 'a
+val list_iter3 : ('a -> 'b -> 'c -> unit) ->
+  'a list -> 'b list -> 'c list -> unit
+val get_some_option_list : 'a option list -> 'a list
+val list_append: ('a list) -> ('a list) -> ('a list) (* tail-recursive append*)
+
+(** Iterate over a list passing the index as you go *)
+val list_iteri: (int -> 'a -> unit) -> 'a list -> unit
+val list_mapi: (int -> 'a -> 'b) -> 'a list -> 'b list
+
+(** Like fold_left but pass the index into the list as well *)
+val list_fold_lefti: ('acc -> int -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc
+
+(** Generates the range of integers starting with a and ending with b *)
+val int_range_list : int -> int -> int list
+
+(* Create a list of length l *)
+val list_init : int -> (int -> 'a) -> 'a list
+
+(** Find the first element in a list that returns Some *)
+val list_find_first: 'a list -> ('a -> 'b option) -> 'b option 
+
+(** mapNoCopy is like map but avoid copying the list if the function does not 
+ * change the elements *)
+
+val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
+
+val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list
+
+val filterNoCopy: ('a -> bool) -> 'a list -> 'a list
+
+
+(** Join a list of strings *)
+val joinStrings: string -> string list -> string
+
+
+(**** Now in growArray.mli
+
+(** Growable arrays *)
+type 'a growArrayFill =
+    Elem of 'a
+  | Susp of (int -> 'a)
+
+type 'a growArray = {
+            gaFill: 'a growArrayFill;
+            (** Stuff to use to fill in the array as it grows *)
+
+    mutable gaMaxInitIndex: int;
+            (** Maximum index that was written to. -1 if no writes have 
+             * been made.  *)
+
+    mutable gaData: 'a array;
+  } 
+
+val newGrowArray: int -> 'a growArrayFill -> 'a growArray
+(** [newGrowArray initsz fillhow] *)
+
+val getReg: 'a growArray -> int -> 'a
+val setReg: 'a growArray -> int -> 'a -> unit
+val copyGrowArray: 'a growArray -> 'a growArray
+val deepCopyGrowArray: 'a growArray -> ('a -> 'a) -> 'a growArray
+
+
+val growArray_iteri:  (int -> 'a -> unit) -> 'a growArray -> unit
+(** Iterate over the initialized elements of the array *)
+
+val growArray_foldl: ('acc -> 'a -> 'acc) -> 'acc ->'a growArray -> 'acc
+(** Fold left over the initialized elements of the array *)
+
+****)
+
+(** hasPrefix prefix str returns true with str starts with prefix *)
+val hasPrefix: string -> string -> bool
+
+
+(** Given a ref cell, produce a thunk that later restores it to its current value *)
+val restoreRef: ?deepCopy:('a -> 'a) -> 'a ref -> unit -> unit
+
+(** Given a hash table, produce a thunk that later restores it to its current value *)
+val restoreHash: ?deepCopy:('b -> 'b) -> ('a, 'b) Hashtbl.t -> unit -> unit
+
+(** Given an integer hash table, produce a thunk that later restores it to 
+ * its current value *)
+val restoreIntHash: ?deepCopy:('b -> 'b) -> 'b Inthash.t -> unit -> unit
+
+(** Given an array, produce a thunk that later restores it to its current value *)
+val restoreArray: ?deepCopy:('a -> 'a) -> 'a array -> unit -> unit
+
+
+(** Given a list of thunks, produce a thunk that runs them all *)
+val runThunks: (unit -> unit) list -> unit -> unit
+
+
+val memoize: ('a, 'b) Hashtbl.t ->
+            'a ->
+            ('a -> 'b) -> 'b
+
+(** Just another name for memoize *)
+val findOrAdd: ('a, 'b) Hashtbl.t ->
+            'a ->
+            ('a -> 'b) -> 'b
+
+val tryFinally: 
+    ('a -> 'b) -> (* The function to run *)
+    ('b option -> unit) -> (* Something to run at the end. The None case is 
+                          * used when an exception is thrown *)
+    'a -> 'b
+
+
+
+
+(** Get the value of an option.  Raises Failure if None *)
+val valOf : 'a option -> 'a
+
+(**
+ * An accumulating for loop.
+ *
+ * Initialize the accumulator with init.  The current index and accumulator
+ * from the previous iteration is passed to f.
+ *)
+val fold_for : init:'a -> lo:int -> hi:int -> (int -> 'a -> 'a) -> 'a
+
+(************************************************************************)
+
+module type STACK = sig
+  type 'a t
+  (** The type of stacks containing elements of type ['a]. *)
+
+  exception Empty
+  (** Raised when {!Util.Stack.pop} or {!Util.Stack.top} is applied to an 
+   * empty stack. *)
+
+  val create : unit -> 'a t
+
+
+  val push : 'a -> 'a t -> unit
+  (** [push x s] adds the element [x] at the top of stack [s]. *)
+
+  val pop : 'a t -> 'a
+  (** [pop s] removes and returns the topmost element in stack [s],
+     or raises [Empty] if the stack is empty. *)
+
+  val top : 'a t -> 'a
+  (** [top s] returns the topmost element in stack [s],
+     or raises [Empty] if the stack is empty. *)
+  
+  val clear : 'a t -> unit
+  (** Discard all elements from a stack. *)
+  
+  val copy : 'a t -> 'a t
+  (** Return a copy of the given stack. *)
+  
+  val is_empty : 'a t -> bool
+  (** Return [true] if the given stack is empty, [false] otherwise. *)
+  
+  val length : 'a t -> int
+  (** Return the number of elements in a stack. *)
+  
+  val iter : ('a -> unit) -> 'a t -> unit
+  (** [iter f s] applies [f] in turn to all elements of [s],
+     from the element at the top of the stack to the element at the
+     bottom of the stack. The stack itself is unchanged. *)
+end
+
+module Stack : STACK
+
+(************************************************************************
+   Configuration 
+************************************************************************)
+(** The configuration data can be of several types **)
+type configData = 
+    ConfInt of int
+  | ConfBool of bool
+  | ConfFloat of float
+  | ConfString of string
+  | ConfList of configData list
+
+
+(** Load the configuration from a file *)
+val loadConfiguration: string -> unit
+
+(** Save the configuration in a file. Overwrites the previous values *)
+val saveConfiguration: string -> unit
+
+
+(** Clear all configuration data *)
+val clearConfiguration: unit -> unit
+
+(** Set a configuration element, with a key. Overwrites the previous values *)
+val setConfiguration: string -> configData -> unit
+
+(** Find a configuration elements, given a key. Raises Not_found if it canont 
+ * find it *)
+val findConfiguration: string -> configData
+
+(** Like findConfiguration but extracts the integer *)
+val findConfigurationInt: string -> int
+
+(** Looks for an integer configuration element, and if it is found, it uses 
+ * the given function. Otherwise, does nothing *)
+val useConfigurationInt: string -> (int -> unit) -> unit
+
+
+val findConfigurationBool: string -> bool
+val useConfigurationBool: string -> (bool -> unit) -> unit
+
+val findConfigurationString: string -> string
+val useConfigurationString: string -> (string -> unit) -> unit
+
+val findConfigurationList: string -> configData list
+val useConfigurationList: string -> (configData list -> unit) -> unit
+
+
+(************************************************************************)
+
+(** Symbols are integers that are uniquely associated with names *)
+type symbol = int
+
+(** Get the name of a symbol *)
+val symbolName: symbol -> string
+
+(** Register a symbol name and get the symbol for it *)
+val registerSymbolName: string -> symbol
+
+(** Register a number of consecutive symbol ids. The naming function will be 
+ * invoked with indices from 0 to the counter - 1. Returns the id of the 
+ * first symbol created. The naming function is invoked lazily, only when the 
+ * name of the symbol is required. *)
+val registerSymbolRange: int -> (int -> string) -> symbol
+
+
+(** Make a fresh symbol. Give the name also, which ought to be distinct from 
+ * existing symbols. This is different from registerSymbolName in that it 
+ * always creates a new symbol. *)
+val newSymbol: string -> symbol
+
+(** Reset the state of the symbols to the program startup state *)
+val resetSymbols: unit -> unit
+
+(** Take a snapshot of the symbol state. Returns a thunk that restores the 
+ * state. *)
+val snapshotSymbols: unit -> unit -> unit
+
+
+(** Dump the list of registered symbols *)
+val dumpSymbols: unit -> unit
+
+(************************************************************************)
+
+(** {1 Int32 Operators} *)
+
+module Int32Op : sig
+   val (<%) : int32 -> int32 -> bool
+   val (<=%) : int32 -> int32 -> bool
+   val (>%) : int32 -> int32 -> bool
+   val (>=%) : int32 -> int32 -> bool
+   val (<>%) : int32 -> int32 -> bool
+   
+   val (+%) : int32 -> int32 -> int32
+   val (-%) : int32 -> int32 -> int32
+   val ( *% ) : int32 -> int32 -> int32
+   val (/%) : int32 -> int32 -> int32
+   val (~-%) : int32 -> int32
+
+   val sll : int32 -> int32 -> int32
+   val (>>%) : int32 -> int32 -> int32
+   val (>>>%) : int32 -> int32 -> int32
+
+   exception IntegerTooLarge
+   val to_int : int32 -> int
+end
+
+(************************************************************************)
+
+(** This has the semantics of (=) on OCaml 3.07 and earlier.  It can
+   handle cyclic values as long as a structure in the cycle has a unique
+   name or id in some field that occurs before any fields that have cyclic
+   pointers. *)
+val equals: 'a -> 'a -> bool