Getting rid of CIL

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

23 files changed, 0 insertions, 5205 deletions

diff --git a/cil/ocamlutil/Makefile.ocaml b/cil/ocamlutil/Makefile.ocaml
deleted file mode 100644
index 36ac21a5..00000000
--- a/cil/ocamlutil/Makefile.ocaml
+++ /dev/null
@@ -1,395 +0,0 @@
-# -*- 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
-   LINKFLAGS    += -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
deleted file mode 100644
index 5271e461..00000000
--- a/cil/ocamlutil/Makefile.ocaml.build
+++ /dev/null
@@ -1,50 +0,0 @@
-# -*- 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
deleted file mode 100755
index 6a1ea017..00000000
--- a/cil/ocamlutil/alpha.ml
+++ /dev/null
@@ -1,156 +0,0 @@
-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
deleted file mode 100755
index e1e430dc..00000000
--- a/cil/ocamlutil/alpha.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(** {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
deleted file mode 100644
index 80f0fd64..00000000
--- a/cil/ocamlutil/clist.ml
+++ /dev/null
@@ -1,183 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index c0378a60..00000000
--- a/cil/ocamlutil/clist.mli
+++ /dev/null
@@ -1,97 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index 07e935d4..00000000
--- a/cil/ocamlutil/errormsg.ml
+++ /dev/null
@@ -1,337 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index 8d9c6979..00000000
--- a/cil/ocamlutil/errormsg.mli
+++ /dev/null
@@ -1,164 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index ccadc762..00000000
--- a/cil/ocamlutil/growArray.ml
+++ /dev/null
@@ -1,191 +0,0 @@
-(** 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
deleted file mode 100644
index 4cb5f48f..00000000
--- a/cil/ocamlutil/growArray.mli
+++ /dev/null
@@ -1,131 +0,0 @@
-(***********************************************************************)
-(* 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
deleted file mode 100755
index b1ad0c07..00000000
--- a/cil/ocamlutil/inthash.ml
+++ /dev/null
@@ -1,188 +0,0 @@
-(** 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
deleted file mode 100755
index f62fcd2b..00000000
--- a/cil/ocamlutil/inthash.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-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
deleted file mode 100755
index 00242bc1..00000000
--- a/cil/ocamlutil/intmap.ml
+++ /dev/null
@@ -1,171 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                           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
deleted file mode 100755
index eef89b55..00000000
--- a/cil/ocamlutil/intmap.mli
+++ /dev/null
@@ -1,87 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                           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
deleted file mode 100755
index ae532f69..00000000
--- a/cil/ocamlutil/perfcount.c.in
+++ /dev/null
@@ -1,184 +0,0 @@
-// -*- 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
deleted file mode 100644
index 47d07ac4..00000000
--- a/cil/ocamlutil/pretty.ml
+++ /dev/null
@@ -1,859 +0,0 @@
-(* 
- *
- * 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
deleted file mode 100644
index 5422432d..00000000
--- a/cil/ocamlutil/pretty.mli
+++ /dev/null
@@ -1,316 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index 8bbb7d05..00000000
--- a/cil/ocamlutil/stats.ml
+++ /dev/null
@@ -1,146 +0,0 @@
-(* 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
deleted file mode 100644
index 9ed98e56..00000000
--- a/cil/ocamlutil/stats.mli
+++ /dev/null
@@ -1,72 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index b4292865..00000000
--- a/cil/ocamlutil/trace.ml
+++ /dev/null
@@ -1,169 +0,0 @@
-(*
- *
- * 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
deleted file mode 100644
index 46ca6523..00000000
--- a/cil/ocamlutil/trace.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(*
- *
- * 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
deleted file mode 100755
index e6c2c679..00000000
--- a/cil/ocamlutil/util.ml
+++ /dev/null
@@ -1,815 +0,0 @@
-(** 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
deleted file mode 100644
index d701c65f..00000000
--- a/cil/ocamlutil/util.mli
+++ /dev/null
@@ -1,311 +0,0 @@
-(** 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