Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles

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

12 files changed, 548 insertions, 514 deletions

diff --git a/Makefile b/Makefile
index bea28ac..f54d7c4 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,8 @@
+include Makefile.config
+
 COQC=coqc $(INCLUDES)
 COQDEP=coqdep $(INCLUDES)
 COQDOC=coqdoc
-CILDISTRIB=cil-1.3.5.tar.gz
 
 INCLUDES=-I lib -I common -I backend -I cfrontend
 
@@ -55,16 +56,11 @@ proof: $(FILES:.v=.vo)
 
 all:
 	$(MAKE) proof
-	$(MAKE) cil
+	$(MAKE) -C cil
 	$(MAKE) -C extraction extraction
 	$(MAKE) -C extraction depend
 	$(MAKE) -C extraction
-
-cil:
-	tar xzf $(CILDISTRIB)
-	for i in cil.patch/*; do patch -p1 < $$i; done
-	cd cil; ./configure
-	$(MAKE) -C cil
+	$(MAKE) -C runtime
 
 documentation:
 	@ln -f $(FILES) doc/
@@ -88,11 +84,22 @@ latexdoc:
 depend:
 	$(COQDEP) $(FILES) > .depend
 
+install:
+	$(MAKE) -C extraction install
+	$(MAKE) -C runtime install
+
 clean:
 	rm -f */*.vo *~ */*~
 	rm -rf doc/html doc/*.glob
 	$(MAKE) -C extraction clean
+	$(MAKE) -C runtime clean
 	$(MAKE) -C test/cminor clean
+	$(MAKE) -C test/c clean
+
+distclean:
+	$(MAKE) clean
+	rm -rf cil
+	rm -f Makefile.config
 
 include .depend
 
diff --git a/caml/Driver.ml b/caml/Driver.ml
new file mode 100644
index 0000000..fcd7a57
--- /dev/null
+++ b/caml/Driver.ml
@@ -0,0 +1,345 @@
+open Printf
+
+(* Location of the standard library *)
+
+let stdlib_path = ref(
+  try
+    Sys.getenv "COMPCERT_LIBRARY"
+  with Not_found ->
+    Configuration.stdlib_path)
+
+(* Command-line flags *)
+
+let prepro_options = ref ([]: string list)
+let linker_options = ref ([]: string list)
+let exe_name = ref "a.out"
+let option_flonglong = ref false
+let option_dclight = ref false
+let option_dasm = ref false
+let option_E = ref false
+let option_S = ref false
+let option_c = ref false
+let option_v = ref false
+
+let command cmd =
+  if !option_v then begin
+    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+  end;
+  Sys.command cmd
+
+let quote_options opts =
+  String.concat " " (List.rev_map Filename.quote opts)
+
+let safe_remove file =
+  try Sys.remove file with Sys_error _ -> ()
+
+(* Printing of error messages *)
+
+let print_error oc msg =
+  let print_one_error = function
+  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
+  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
+  in Camlcoq.coqlist_iter print_one_error msg
+
+(* For the CIL -> Csyntax translator:
+
+  * The meaning of some type specifiers may depend on compiler options:
+      the size of an int or the default signedness of char, for instance.
+
+  * Those type conversions may be parameterized thanks to a functor.
+
+  * Remark: [None] means that the type specifier is not supported
+      (that is, an Unsupported exception will be raised if that type
+      specifier is encountered in the program).
+*)
+
+module TypeSpecifierTranslator = struct
+  
+  open Cil
+  open Csyntax
+    
+  (** Convert a Cil.ikind into an (intsize * signedness) option *)
+  let convertIkind = function
+    | IChar      -> Some (I8, Unsigned)
+    | ISChar     -> Some (I8, Signed)
+    | IUChar     -> Some (I8, Unsigned)
+    | IInt       -> Some (I32, Signed)
+    | IUInt      -> Some (I32, Unsigned)
+    | IShort     -> Some (I16, Signed)
+    | IUShort    -> Some (I16, Unsigned)
+    | ILong      -> Some (I32, Signed)
+    | IULong     -> Some (I32, Unsigned)
+    | ILongLong  -> if !option_flonglong then Some (I32, Signed) else None
+    | IULongLong -> if !option_flonglong then Some (I32, Unsigned) else None
+	
+  (** Convert a Cil.fkind into an floatsize option *)
+  let convertFkind = function
+    | FFloat      -> Some F32
+    | FDouble     -> Some F64
+    | FLongDouble -> if !option_flonglong then Some F64 else None
+	
+end
+
+module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
+
+(* From C to preprocessed C *)
+
+let preprocess ifile ofile =
+  let cmd =
+    sprintf "gcc -arch ppc -D__COMPCERT__ -I%s %s -E %s > %s"
+      !stdlib_path
+      (quote_options !prepro_options)
+      ifile ofile in
+  if command cmd <> 0 then begin
+    safe_remove ofile;
+    eprintf "Error during preprocessing.\n";
+    exit 2
+  end
+
+(* From preprocessed C to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  (* Parsing and production of a CIL.file *)
+  let cil =
+    try
+      Frontc.parse ifile ()
+    with
+    | Frontc.ParseError msg ->
+        eprintf "Error during parsing: %s\n" msg;
+        exit 2
+    | Errormsg.Error ->
+        exit 2 in
+  (* Remove preprocessed file (always a temp file) *)
+  safe_remove ifile;
+  (* Restore original source file name *)
+  cil.Cil.fileName <- sourcename;
+  (* Cleanup in the CIL.file *)
+  Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
+  (* Conversion to Csyntax *)
+  let csyntax =
+    try
+      Cil2CsyntaxTranslator.convertFile cil
+    with
+    | Cil2CsyntaxTranslator.Unsupported msg ->
+        eprintf "%s\n" msg;
+        exit 2
+    | Cil2CsyntaxTranslator.Internal_error msg ->
+        eprintf "%s\nPlease report it.\n" msg;
+        exit 2 in
+  (* Save Csyntax if requested *)
+  if !option_dclight then begin
+    let targetname = Filename.chop_suffix sourcename ".c" in
+    let oc = open_out (targetname ^ ".light.c") in
+    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
+  (* Convert to PPC *)
+  let ppc =
+    match Main.transf_c_program csyntax with
+    | Errors.OK x -> x
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2 in
+  (* Save PPC asm *)
+  let oc = open_out ofile in
+  PrintPPC.print_program oc ppc;
+  close_out oc
+
+(* From Cminor to asm *)
+
+let compile_cminor_file ifile ofile =
+  let ic = open_in ifile in
+  let lb = Lexing.from_channel ic in
+  try
+    match Main.transf_cminor_program
+            (CMtypecheck.type_program
+              (CMparser.prog CMlexer.token lb)) with
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2
+    | Errors.OK p ->
+        let oc = open_out ofile in
+        PrintPPC.print_program oc p;
+        close_out oc
+  with Parsing.Parse_error ->
+         eprintf "File %s, character %d: Syntax error\n"
+                 ifile (Lexing.lexeme_start lb);
+         exit 2
+     | CMlexer.Error msg ->  
+         eprintf "File %s, character %d: %s\n"
+                 ifile (Lexing.lexeme_start lb) msg;
+         exit 2
+     | CMtypecheck.Error msg ->
+         eprintf "File %s, type-checking error:\n%s"
+                 ifile msg;
+         exit 2
+
+(* From asm to object file *)
+
+let assemble ifile ofile =
+  let cmd =
+    sprintf "gcc -arch ppc -c -o %s %s"
+      ofile ifile in
+  let retcode = command cmd in
+  if not !option_dasm then safe_remove ifile;
+  if retcode <> 0 then begin
+    safe_remove ofile;
+    eprintf "Error during assembling.\n";
+    exit 2
+  end
+
+(* Linking *)
+
+let linker exe_name files =
+  let cmd =
+    sprintf "gcc -arch ppc -o %s %s -L%s -lcompcert"
+      (Filename.quote exe_name)
+      (quote_options files)
+      !stdlib_path in
+  if command cmd <> 0 then exit 2
+
+(* Processing of a .c file *)
+
+let process_c_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".c" in
+  if !option_E then begin
+    preprocess sourcename (prefixname ^ ".i")
+  end else begin
+    let preproname = Filename.temp_file "compcert" ".i" in
+    preprocess sourcename preproname;
+    if !option_S then begin
+      compile_c_file sourcename preproname (prefixname ^ ".s")
+    end else begin
+      let asmname =
+        if !option_dasm
+        then prefixname ^ ".s"
+        else Filename.temp_file "compcert" ".s" in
+      compile_c_file sourcename preproname asmname;
+      assemble asmname (prefixname ^ ".o")
+    end
+  end;
+  prefixname ^ ".o"
+
+(* Processing of a .cm file *)
+
+let process_cminor_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".cm" in
+  if !option_S then begin
+    compile_cminor_file sourcename (prefixname ^ ".s")
+  end else begin
+    let asmname =
+      if !option_dasm
+      then prefixname ^ ".s"
+      else Filename.temp_file "compcert" ".s" in
+    compile_cminor_file sourcename asmname;
+    assemble asmname (prefixname ^ ".o")
+  end;
+  prefixname ^ ".o"
+
+(* Command-line parsing *)
+
+let starts_with s1 s2 =
+  String.length s1 >= String.length s2 &&
+  String.sub s1 0 (String.length s2) = s2
+
+let usage_string =
+"ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .cm            Cminor source file
+  .o             Object file
+  .a             Library file
+Processing options:
+  -E             Preprocess only, save result in <file>.i
+  -S             Compile to assembler only, save result in <file>.s
+  -c             Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+Compilation options:
+  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
+  -dclight       Save generated Clight in <file>.light.c
+  -dasm          Save generated assembly in <file>.s
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -o <file>      Generate executable in <file> (default: a.out)
+General options:
+  -stdlib <dir>  Set the path of the Compcert run-time library
+  -v             Print external commands before invoking them
+"
+
+let rec parse_cmdline i =
+  if i < Array.length Sys.argv then begin
+    let s = Sys.argv.(i) in
+    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
+    then begin
+      prepro_options := s :: !prepro_options;
+      parse_cmdline (i + 1)
+    end else 
+    if starts_with s "-l" || starts_with s "-L" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-o" && i + 1 < Array.length Sys.argv then begin
+      exe_name := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin
+      stdlib_path := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-flonglong" then begin
+      option_flonglong := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dclight" then begin
+      option_dclight := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dasm" then begin
+      option_dasm := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-E" then begin
+      option_E := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-S" then begin
+      option_S := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-c" then begin
+      option_c := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-v" then begin
+      option_v := true;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".c" then begin
+      let objfile = process_c_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".cm" then begin
+      let objfile = process_cminor_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else begin
+      eprintf "Unknown argument `%s'\n" s;
+      eprintf "Usage: %s" usage_string;
+      exit 2
+    end
+  end
+
+let _ =
+  parse_cmdline 1;
+  if not (!option_c || !option_S || !option_E) then begin
+    linker !exe_name !linker_options
+  end
diff --git a/caml/Main2.ml b/caml/Main2.ml
deleted file mode 100644
index e3399fb..0000000
--- a/caml/Main2.ml
+++ /dev/null
@@ -1,166 +0,0 @@
-open Printf
-
-(* For the CIL -> Csyntax translator:
-
-  * The meaning of some type specifiers may depend on compiler options:
-      the size of an int or the default signedness of char, for instance.
-
-  * Those type conversions may be parameterized thanks to a functor.
-
-  * Remark: [None] means that the type specifier is not supported
-      (that is, an Unsupported exception will be raised if that type
-      specifier is encountered in the program).
-*)
-
-module TypeSpecifierTranslator = struct
-  
-  open Cil
-  open Csyntax
-    
-  (** Convert a Cil.ikind into an (intsize * signedness) option *)
-  let convertIkind = function
-    | IChar      -> Some (I8, Unsigned)
-    | ISChar     -> Some (I8, Signed)
-    | IUChar     -> Some (I8, Unsigned)
-    | IInt       -> Some (I32, Signed)
-    | IUInt      -> Some (I32, Unsigned)
-    | IShort     -> Some (I16, Signed)
-    | IUShort    -> Some (I16, Unsigned)
-    | ILong      -> Some (I32, Signed)
-    | IULong     -> Some (I32, Unsigned)
-    | ILongLong  -> (***Some (I32, Signed)***) None
-    | IULongLong -> (***Some (I32, Unsigned)***) None
-	
-  (** Convert a Cil.fkind into an floatsize option *)
-  let convertFkind = function
-    | FFloat      -> Some F32
-    | FDouble     -> Some F64
-    | FLongDouble -> (***Some F64***) None
-	
-end
-
-module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
-
-let prepro_options = ref []
-let save_csyntax = ref false
-
-let preprocess file =
-  let temp = Filename.temp_file "compcert" ".i" in
-  let cmd =
-    sprintf "gcc -arch ppc %s -D__COMPCERT__ -E %s > %s"
-      (String.concat " " (List.rev !prepro_options))
-      file
-      temp in
-  if Sys.command cmd = 0
-  then temp
-  else (eprintf "Error during preprocessing.\n"; exit 2)
-
-let process_c_file sourcename =
-  let targetname = Filename.chop_suffix sourcename ".c" in
-  (* Preprocessing with cpp *)
-  let preproname = preprocess sourcename in
-  (* Parsing and production of a CIL.file *)
-  let cil =
-    try
-      Frontc.parse preproname ()
-    with
-    | Frontc.ParseError msg ->
-        eprintf "Error during parsing: %s\n" msg;
-        exit 2
-    | Errormsg.Error ->
-        exit 2 in
-  Sys.remove preproname;
-  (* Restore source file name before preprocessing *)
-  cil.Cil.fileName <- sourcename;
-  (* Cleanup in the CIL.file *)
-  Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
-  (* Conversion to Csyntax *)
-  let csyntax =
-    try
-      Cil2CsyntaxTranslator.convertFile cil
-    with
-    | Cil2CsyntaxTranslator.Unsupported msg ->
-        eprintf "%s\n" msg;
-        exit 2
-    | Cil2CsyntaxTranslator.Internal_error msg ->
-        eprintf "%s\nPlease report it.\n" msg;
-        exit 2 in
-  (* Save Csyntax if requested *)
-  if !save_csyntax then begin
-    let oc = open_out (targetname ^ ".light.c") in
-    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
-    close_out oc
-  end;
-  (* Convert to PPC *)
-  let ppc =
-    match Main.transf_c_program csyntax with
-    | Errors.OK x -> x
-    | Errors.Error msg ->
-        eprintf "Error in translation Csyntax -> PPC\n";
-        exit 2 in
-  (* Save PPC asm *)
-  let oc = open_out (targetname ^ ".s") in
-  PrintPPC.print_program oc ppc;
-  close_out oc
-
-let process_cminor_file sourcename =
-  let targetname = Filename.chop_suffix sourcename ".cm" ^ ".s" in
-  let ic = open_in sourcename in
-  let lb = Lexing.from_channel ic in
-  try
-    match Main.transf_cminor_program
-            (CMtypecheck.type_program
-              (CMparser.prog CMlexer.token lb)) with
-    | Errors.Error msg ->
-        eprintf "Compiler failure\n";
-        exit 2
-    | Errors.OK p ->
-        let oc = open_out targetname in
-        PrintPPC.print_program oc p;
-        close_out oc
-  with Parsing.Parse_error ->
-         eprintf "File %s, character %d: Syntax error\n"
-                 sourcename (Lexing.lexeme_start lb);
-         exit 2
-     | CMlexer.Error msg ->  
-         eprintf "File %s, character %d: %s\n"
-                 sourcename (Lexing.lexeme_start lb) msg;
-         exit 2
-     | CMtypecheck.Error msg ->
-         eprintf "File %s, type-checking error:\n%s"
-                 sourcename msg;
-         exit 2
-
-(* Command-line parsing *)
-
-let starts_with s1 s2 =
-  String.length s1 >= String.length s2 &&
-  String.sub s1 0 (String.length s2) = s2
-
-let rec parse_cmdline i =
-  if i < Array.length Sys.argv then begin
-    let s = Sys.argv.(i) in
-    if s = "-dump-c" then begin
-      save_csyntax := true;
-      parse_cmdline (i + 1)
-    end else
-    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
-    then begin
-      prepro_options := s :: !prepro_options;
-      parse_cmdline (i + 1)
-    end else 
-    if Filename.check_suffix s ".cm" then begin
-      process_cminor_file s;
-      parse_cmdline (i + 1)
-    end else
-    if Filename.check_suffix s ".c" then begin
-      process_c_file s;
-      parse_cmdline (i + 1)
-    end else begin
-      eprintf "Unknown argument `%s'\n" s;
-      exit 2
-    end
-  end
-
-let _ =
-  parse_cmdline 1
diff --git a/configure b/configure
new file mode 100755
index 0000000..2f4edf3
--- /dev/null
+++ b/configure
@@ -0,0 +1,42 @@
+#!/bin/sh
+
+cildistrib=cil-1.3.5.tar.gz
+prefix=/usr/local
+bindir='$(PREFIX)/bin'
+libdir='$(PREFIX)/lib/compcert'
+
+# Parse command-line arguments
+
+while : ; do
+  case "$1" in
+    "") break;;
+    -prefix|--prefix)
+        prefix=$2; shift;;
+    -bindir|--bindir)
+        bindir=$2; shift;;
+    -libdir|--libdir)
+        libdir=$2; shift;;
+    *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+  esac
+  shift
+done
+
+# Generate Makefile.config
+
+rm -f Makefile.config
+cat > Makefile.config <<EOF
+PREFIX=$prefix
+BINDIR=$bindir
+LIBDIR=$libdir
+EOF
+
+# Extract and configure Cil
+
+set -e
+tar xzf $cildistrib
+for i in cil.patch/*; do patch -p1 < $i; done
+(cd cil && ./configure)
+
+# Extract 'ARCHOS' info from Cil configuration
+
+grep '^ARCHOS=' cil/config.log >> Makefile.config
diff --git a/extraction/.depend b/extraction/.depend
index 956c4d3..afffe81 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -4,6 +4,14 @@
 ../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \
     InterfGraph.cmi 
 ../caml/PrintPPC.cmi: PPC.cmi 
+../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi 
+../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx 
+../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
+    CList.cmi AST.cmi 
+../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
+    CList.cmx AST.cmx 
 ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \
     ../caml/CMlexer.cmi 
 ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \
@@ -14,24 +22,24 @@
 ../caml/CMparser.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \
     ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
     ../caml/CMparser.cmi 
-../caml/CMtypecheck.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \
+../caml/CMtypecheck.cmo: Integers.cmi Datatypes.cmi Cminor.cmi \
     ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi 
-../caml/CMtypecheck.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \
+../caml/CMtypecheck.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \
     ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi 
-../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi 
-../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx 
-../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
-    CList.cmi AST.cmi 
-../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
-    CList.cmx AST.cmx 
 ../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \
     ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi 
 ../caml/Coloringaux.cmx: Registers.cmx RTLtyping.cmx RTL.cmx Maps.cmx \
     Locations.cmx InterfGraph.cmx Datatypes.cmx Conventions.cmx \
     ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi 
+../caml/Driver.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \
+    Errors.cmi Csyntax.cmi ../caml/Configuration.cmo ../caml/Cil2Csyntax.cmo \
+    ../caml/Camlcoq.cmo ../caml/CMtypecheck.cmi ../caml/CMparser.cmi \
+    ../caml/CMlexer.cmi 
+../caml/Driver.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \
+    Errors.cmx Csyntax.cmx ../caml/Configuration.cmx ../caml/Cil2Csyntax.cmx \
+    ../caml/Camlcoq.cmx ../caml/CMtypecheck.cmx ../caml/CMparser.cmx \
+    ../caml/CMlexer.cmx 
 ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
 ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
 ../caml/Main2.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \
@@ -40,6 +48,10 @@
 ../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \
     Errors.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \
     ../caml/CMparser.cmx ../caml/CMlexer.cmx 
+../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
+    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
+../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
+    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -56,12 +68,12 @@
     ../caml/Camlcoq.cmo CList.cmi AST.cmi 
 ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
     ../caml/Camlcoq.cmx CList.cmx AST.cmx 
-AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi 
 Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
     Maps.cmi Locations.cmi LTL.cmi Errors.cmi Datatypes.cmi Coloring.cmi \
     CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
 Ascii.cmi: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi 
+AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
+    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi 
 BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi 
 BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi 
 BinPos.cmi: Peano.cmi Datatypes.cmi 
@@ -70,18 +82,15 @@ Bounds.cmi: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \
     BinPos.cmi BinInt.cmi AST.cmi 
 CInt.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi 
 CList.cmi: Specif.cmi Datatypes.cmi 
-CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
-CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi 
+Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
+    Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \
+    Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \
+    AST.cmi 
 Cminor.cmi: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
 CminorSel.cmi: Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi CList.cmi \
     BinInt.cmi AST.cmi 
-Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \
-    Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \
-    AST.cmi 
 Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     CList.cmi BinInt.cmi AST.cmi 
@@ -92,12 +101,15 @@ Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
 Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
     BinPos.cmi BinInt.cmi 
+CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
+    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
 Csharpminor.cmi: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
     AST.cmi 
 Cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
     Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi CList.cmi Ascii.cmi \
     AST.cmi 
+CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi 
 Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
     Ascii.cmi AST.cmi 
@@ -105,12 +117,12 @@ Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
     CList.cmi AST.cmi 
 EqNat.cmi: Specif.cmi Datatypes.cmi 
 Errors.cmi: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi 
+Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Datatypes.cmi \
     CList.cmi CInt.cmi BinPos.cmi BinInt.cmi 
 FSetFacts.cmi: Specif.cmi Setoid.cmi FSetInterface.cmi Datatypes.cmi 
 FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
 FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
-Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \
@@ -121,21 +133,21 @@ Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi
 Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
     Lattice.cmi Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi \
     BinPos.cmi BinInt.cmi 
-LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
-LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi 
 Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi 
+Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
 Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
-Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
 Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
+LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
+LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi 
 Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Locations.cmi \
     Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
@@ -152,26 +164,26 @@ Op.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
 Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \
     BinPos.cmi 
 OrderedType.cmi: Specif.cmi Datatypes.cmi 
-PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
-    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi 
 Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi 
 Peano.cmi: Datatypes.cmi 
-RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
+PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
+    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
+PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
+    Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
+    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
 RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \
     Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi \
     CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
+RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi Conventions.cmi CString.cmi CList.cmi BinPos.cmi \
     BinInt.cmi Ascii.cmi AST.cmi 
-Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
 Selection.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
     CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Setoid.cmi: Datatypes.cmi 
@@ -193,10 +205,6 @@ Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi
 Zmax.cmi: Datatypes.cmi BinInt.cmi 
 Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi 
 Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
-AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
-    Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi 
 Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
     Maps.cmi Locations.cmi Lattice.cmi LTL.cmi Kildall.cmi Errors.cmi \
     Datatypes.cmi Coloring.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
@@ -207,6 +215,10 @@ Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx \
     AST.cmx Allocation.cmi 
 Ascii.cmo: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi Ascii.cmi 
 Ascii.cmx: Specif.cmx Peano.cmx Datatypes.cmx Bool.cmx BinPos.cmx Ascii.cmi 
+AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
+    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
+AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
+    Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi 
 BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi 
 BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi 
 BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi 
@@ -223,14 +235,14 @@ CInt.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CInt.cmi
 CInt.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx CInt.cmi 
 CList.cmo: Specif.cmi Datatypes.cmi CList.cmi 
 CList.cmx: Specif.cmx Datatypes.cmx CList.cmi 
-CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \
-    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    AST.cmi CSE.cmi 
-CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \
-    Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
-    AST.cmx CSE.cmi 
-CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi 
-CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi 
+Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
+    Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \
+    Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \
+    BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi 
+Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \
+    Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \
+    Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \
+    BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi 
 Cminor.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi Cminor.cmi 
@@ -241,14 +253,6 @@ CminorSel.cmo: Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi CList.cmi \
     BinInt.cmi AST.cmi CminorSel.cmi 
 CminorSel.cmx: Op.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx CList.cmx \
     BinInt.cmx AST.cmx CminorSel.cmi 
-Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \
-    Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi 
-Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \
-    Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \
-    Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi 
 Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi 
@@ -271,6 +275,12 @@ Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
     BinPos.cmi BinInt.cmi Coqlib.cmi 
 Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \
     BinPos.cmx BinInt.cmx Coqlib.cmi 
+CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \
+    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
+    AST.cmi CSE.cmi 
+CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \
+    Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
+    AST.cmx CSE.cmi 
 Csharpminor.cmo: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
     AST.cmi Csharpminor.cmi 
@@ -283,6 +293,8 @@ Cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
 Cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
     Csyntax.cmx Csharpminor.cmx Cminor.cmx CString.cmx CList.cmx Ascii.cmx \
     AST.cmx Cshmgen.cmi 
+CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi 
+CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi 
 Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
     Ascii.cmi AST.cmi Csyntax.cmi 
@@ -299,6 +311,10 @@ EqNat.cmo: Specif.cmi Datatypes.cmi EqNat.cmi
 EqNat.cmx: Specif.cmx Datatypes.cmx EqNat.cmi 
 Errors.cmo: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi Errors.cmi 
 Errors.cmx: Datatypes.cmx CString.cmx CList.cmx BinPos.cmx Errors.cmi 
+Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
+    Floats.cmi 
+Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
+    Floats.cmi 
 FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi FSetList.cmi \
     Datatypes.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
 FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx FSetList.cmx \
@@ -313,10 +329,6 @@ FSetInterface.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx \
     FSetInterface.cmi 
 FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi 
 FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi 
-Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
-    Floats.cmi 
-Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
-    Floats.cmi 
 Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi 
 Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \
@@ -341,40 +353,40 @@ Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
 Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Ordered.cmx Maps.cmx \
     Lattice.cmx Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx \
     Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi 
-LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi LTL.cmi 
-LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \
-    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx LTL.cmi 
-LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi LTLin.cmi 
-LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx LTLin.cmi 
 Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi Lattice.cmi 
 Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \
     BinPos.cmx Lattice.cmi 
-Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi Linear.cmi 
-Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx Linear.cmi 
 Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
     Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \
     Linearize.cmi 
 Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
     Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \
     Linearize.cmi 
+Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi Linear.cmi 
+Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx Linear.cmi 
 Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
     BinInt.cmi AST.cmi Locations.cmi 
 Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \
     BinInt.cmx AST.cmx Locations.cmi 
 Logic.cmo: Logic.cmi 
 Logic.cmx: Logic.cmi 
+LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi LTLin.cmi 
+LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx LTLin.cmi 
+LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi LTL.cmi 
+LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \
+    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx AST.cmx LTL.cmi 
 Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Maps.cmi \
     Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi 
@@ -407,18 +419,6 @@ Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \
     BinPos.cmx Ordered.cmi 
 OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi 
 OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.cmi 
-PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi PPC.cmi 
-PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
-    Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx PPC.cmi 
-PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
-    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi 
-PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \
-    Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi 
 Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \
     Parallelmove.cmi 
 Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \
@@ -427,12 +427,28 @@ Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi
 Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.cmi 
 Peano.cmo: Datatypes.cmi Peano.cmi 
 Peano.cmx: Datatypes.cmx Peano.cmi 
-RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    RTL.cmi 
-RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    RTL.cmi 
+PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
+    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi 
+PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \
+    Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi 
+PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
+    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi PPC.cmi 
+PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
+    Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx PPC.cmi 
+Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
+    Registers.cmi 
+Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
+    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    Registers.cmi 
+Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
+    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi 
+Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
+    LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi 
 RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \
     Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
     CminorSel.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi \
@@ -441,6 +457,12 @@ RTLgen.cmx: Switch.cmx Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx \
     Op.cmx Maps.cmx Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx \
     CminorSel.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx AST.cmx \
     RTLgen.cmi 
+RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
+    RTL.cmi 
+RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    RTL.cmi 
 RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \
     Op.cmi Maps.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi \
@@ -449,16 +471,6 @@ RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \
     Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
     CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx \
     RTLtyping.cmi 
-Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    Registers.cmi 
-Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
-    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    Registers.cmi 
-Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi 
-Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
-    LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi 
 Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
     CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
     Selection.cmi 
diff --git a/extraction/Makefile b/extraction/Makefile
index cb7f4c5..dd70d88 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -1,3 +1,5 @@
+include ../Makefile.config
+
 FILES=\
   Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml EqNat.ml \
   Bool.ml CList.ml Sumbool.ml Setoid.ml BinPos.ml BinNat.ml BinInt.ml \
@@ -29,13 +31,12 @@ FILES=\
   ../caml/Cil2Csyntax.ml \
   ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \
   ../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \
-  ../caml/Main2.ml
-#  ../caml/Configuration.ml ../caml/Driver.ml
+  ../caml/Configuration.ml ../caml/Driver.ml
 
 EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
 GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
 
-CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX -I ../cil/obj/ppc_DARWIN
+CAMLINCL=-I ../caml -I ../cil/obj/$(ARCHOS)
 OCAMLC=ocamlc -g $(CAMLINCL)
 OCAMLOPT=ocamlopt $(CAMLINCL)
 OCAMLDEP=ocamldep $(CAMLINCL)
@@ -49,12 +50,12 @@ executables: ../ccomp ../ccomp.byt
 ../ccomp.byt: $(FILES:.ml=.cmo)
 	$(OCAMLC) -o ../ccomp.byt $(OCAMLLIBS) $(FILES:.ml=.cmo)
 clean::
-	rm -f ../ccomp
+	rm -f ../ccomp.byt
 
 ../ccomp: $(FILES:.ml=.cmx)
 	$(OCAMLOPT) -o ../ccomp $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
 clean::
-	rm -f ../ccomp.opt
+	rm -f ../ccomp
 
 extraction:
 	@rm -f $(GENFILES)
@@ -89,6 +90,13 @@ beforedepend:: ../caml/CMlexer.ml
 clean::
 	rm -f ../caml/CMlexer.ml
 
+../caml/Configuration.ml: ../Makefile.config
+	echo 'let stdlib_path = "$(LIBDIR)"' > ../caml/Configuration.ml
+
+beforedepend:: ../caml/Configuration.ml
+clean::
+	rm -f ../caml/Configuration.ml
+
 .SUFFIXES: .ml .mli .cmo .cmi .cmx
 
 .mli.cmi:
@@ -106,6 +114,10 @@ clean::
 depend: beforedepend
 	$(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend
 
+install:
+	install -d $(BINDIR)
+	install ../ccomp ../ccomp.byt $(BINDIR)
+
 include .depend
 
 
diff --git a/runtime/Makefile b/runtime/Makefile
index c45c9fb..9a3f621 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -1,7 +1,10 @@
+include ../Makefile.config
+
 CFLAGS=-arch ppc -O1 -g -Wall
 #CFLAGS=-O1 -g -Wall
 OBJS=stdio.o calloc.o
 LIB=libcompcert.a
+INCLUDES=stdio.h
 
 $(LIB): $(OBJS)
 	rm -f $(LIB)
@@ -11,3 +14,7 @@ stdio.o: stdio.h
 
 clean:
 	rm -f *.o $(LIB)
+
+install:
+	install -d $(LIBDIR)
+	install -c $(LIB) $(INCLUDES) $(LIBDIR)
diff --git a/test/cminor/Makefile b/test/cminor/Makefile
index bff498c..1d0af21 100644
--- a/test/cminor/Makefile
+++ b/test/cminor/Makefile
@@ -56,7 +56,7 @@ clean::
 	rm -f manyargs
 
 lists: lists.o mainlists.o
-	$(CC) $(CFLAGS) -o lists lists.o mainlists.o
+	$(CC) $(CFLAGS) -o lists lists.o mainlists.o -L../../runtime -lcompcert
 clean::
 	rm -f lists
 
diff --git a/test/lib/Makefile b/test/lib/Makefile
deleted file mode 100644
index 03ba69e..0000000
--- a/test/lib/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-CFLAGS=-arch ppc -O1 -g -Wall
-OBJS=compcert_stdio.o
-LIB=libcompcert.a
-
-$(LIB): $(OBJS)
-	ar rcs $(LIB) $(OBJS)
-
-compcert_stdio.o: compcert_stdio.h
diff --git a/test/lib/compcert_stdio.c b/test/lib/compcert_stdio.c
deleted file mode 100644
index 28c9da4..0000000
--- a/test/lib/compcert_stdio.c
+++ /dev/null
@@ -1,128 +0,0 @@
-#include <stdarg.h>
-#define INSIDE_COMPCERT_COMPATIBILITY_LIBRARY
-#include "compcert_stdio.h"
-
-compcert_FILE * compcert_stdin = (compcert_FILE *) stdin;
-compcert_FILE * compcert_stdout = (compcert_FILE *) stdout;
-compcert_FILE * compcert_stderr = (compcert_FILE *) stderr;
-
-void	 compcert_clearerr(compcert_FILE * f)
-{
-  clearerr((FILE *) f);
-}
-
-int	 compcert_fclose(compcert_FILE * f)
-{
-  return fclose((FILE *) f);
-}
-
-int	 compcert_feof(compcert_FILE * f)
-{
-  return feof((FILE *) f);
-}
-
-int	 compcert_ferror(compcert_FILE * f)
-{
-  return ferror((FILE *) f);
-}
-
-int	 compcert_fflush(compcert_FILE * f)
-{
-  return fflush((FILE *) f);
-}
-
-int	 compcert_fgetc(compcert_FILE * f)
-{
-  return fgetc((FILE *) f);
-}
-
-char	*compcert_fgets(char * s, int n, compcert_FILE * f)
-{
-  return fgets(s, n, (FILE *) f);
-}
-
-compcert_FILE	*compcert_fopen(const char * p, const char * m)
-{
-  return (compcert_FILE *) fopen(p, m);
-}
-
-int	 compcert_fprintf(compcert_FILE * f, const char * s, ...)
-{
-  va_list ap;
-  int retcode;
-  va_start(ap, s);
-  retcode = vfprintf((FILE *) f, s, ap);
-  va_end(ap);
-  return retcode;
-}
-
-int	 compcert_fputc(int c, compcert_FILE * f)
-{
-  return fputc(c, (FILE *) f);
-}
-
-int	 compcert_fputs(const char * s, compcert_FILE * f)
-{
-  return fputs(s, (FILE *) f);
-}
-
-size_t	 compcert_fread(void * s, size_t p, size_t q, compcert_FILE * f)
-{
-  return fread(s, p, q, (FILE *) f);
-}
-
-compcert_FILE	*compcert_freopen(const char * s, const char * m,
-                                  compcert_FILE * f)
-{
-  return (compcert_FILE *) freopen(s, m, (FILE *) f);
-}
-
-int	 compcert_fscanf(compcert_FILE * f, const char * s, ...)
-{
-  va_list ap;
-  int retcode;
-  va_start(ap, s);
-  retcode = vfscanf((FILE *) f, s, ap);
-  va_end(ap);
-  return retcode;
-}
-
-int	 compcert_fseek(compcert_FILE * f, long p, int q)
-{
-  return fseek((FILE *) f, p, q);
-}
-
-long	 compcert_ftell(compcert_FILE *f)
-{
-  return ftell((FILE *) f);
-}
-
-size_t	 compcert_fwrite(const void * b, size_t p, size_t q, compcert_FILE * f)
-{
-  return fwrite(b, p, q, (FILE *) f);
-}
-
-int	 compcert_getc(compcert_FILE * f)
-{
-  return getc((FILE *) f);
-}
-
-int	 compcert_putc(int c , compcert_FILE * f)
-{
-  return putc(c, (FILE *) f);
-}
-
-void	 compcert_rewind(compcert_FILE * f)
-{
-  rewind((FILE *) f);
-}
-
-int	 compcert_ungetc(int c, compcert_FILE * f)
-{
-  return ungetc(c, (FILE *) f);
-}
-
-int	 compcert_vfprintf(compcert_FILE * f, const char * s, va_list va)
-{
-  return vfprintf((FILE *) f, s, va);
-}
diff --git a/test/lib/compcert_stdio.h b/test/lib/compcert_stdio.h
deleted file mode 100644
index 761a893..0000000
--- a/test/lib/compcert_stdio.h
+++ /dev/null
@@ -1,62 +0,0 @@
-#include <stdio.h>
-
-typedef struct compcert_FILE_ { void * f; } compcert_FILE;
-
-extern compcert_FILE * compcert_stdin;
-extern compcert_FILE * compcert_stdout;
-extern compcert_FILE * compcert_stderr;
-extern void	 compcert_clearerr(compcert_FILE *);
-extern int	 compcert_fclose(compcert_FILE *);
-extern int	 compcert_feof(compcert_FILE *);
-extern int	 compcert_ferror(compcert_FILE *);
-extern int	 compcert_fflush(compcert_FILE *);
-extern int	 compcert_fgetc(compcert_FILE *);
-extern char	*compcert_fgets(char * , int, compcert_FILE *);
-extern compcert_FILE	*compcert_fopen(const char * , const char * );
-extern int	 compcert_fprintf(compcert_FILE * , const char * , ...);
-extern int	 compcert_fputc(int, compcert_FILE *);
-extern int	 compcert_fputs(const char * , compcert_FILE * );
-extern size_t	 compcert_fread(void * , size_t, size_t, compcert_FILE * );
-extern compcert_FILE	*compcert_freopen(const char * , const char * ,
-                                          compcert_FILE * );
-extern int	 compcert_fscanf(compcert_FILE * , const char * , ...);
-extern int	 compcert_fseek(compcert_FILE *, long, int);
-extern long	 compcert_ftell(compcert_FILE *);
-extern size_t	 compcert_fwrite(const void * , size_t, size_t, compcert_FILE * );
-extern int	 compcert_getc(compcert_FILE *);
-extern int	 compcert_putc(int, compcert_FILE *);
-extern void	 compcert_rewind(compcert_FILE *);
-extern int	 compcert_ungetc(int, compcert_FILE *);
-extern int	 compcert_vfprintf(compcert_FILE *, const char *, va_list);
-
-#ifndef INSIDE_COMPCERT_COMPATIBILITY_LIBRARY
-#define FILE compcert_FILE
-#undef stdin
-#define stdin compcert_stdin
-#undef stdout
-#define stdout compcert_stdout
-#undef stderr
-#define stderr compcert_stderr
-#define clearerr compcert_clearerr
-#define fclose compcert_fclose
-#define feof compcert_feof
-#define ferror compcert_ferror
-#define fflush compcert_fflush
-#define fgetc compcert_fgetc
-#define fgets compcert_fgets
-#define fopen compcert_fopen
-#define fprintf compcert_fprintf
-#define fputc compcert_fputc
-#define fputs compcert_fputs
-#define fread compcert_fread
-#define freopen compcert_freopen
-#define fscanf compcert_fscanf
-#define fseek compcert_fseek
-#define ftell compcert_ftell
-#define fwrite compcert_fwrite
-#define getc compcert_getc
-#define putc compcert_putc
-#define rewind compcert_rewind
-#define ungetc compcert_ungetc
-#define vfprintf compcert_vfprintf
-#endif
diff --git a/test/lib/staticlib.S b/test/lib/staticlib.S
deleted file mode 100644
index 374c401..0000000
--- a/test/lib/staticlib.S
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Work around MacOX shared-library lossage.
-   (No static version of the C library.) */
-
-.macro GLUE
-	.text
-	.globl	_$0_static
-_$0_static:
-	addis	r11, 0, ha16(L$0)
-	lwz	r11, lo16(L$0)(r11)
-	mtctr	r11
-	bctr
-	.non_lazy_symbol_pointer
-L$0:	
-	.indirect_symbol _$0
-	.long 0
-.endmacro
-
-	GLUE cos
-	GLUE sin
-	GLUE atan2
-	GLUE asin
-	GLUE sqrt
-	GLUE fmod
-	GLUE fabs
-        GLUE memcpy
-        GLUE memset
-        
\ No newline at end of file