diff --git a/Makefile b/Makefile
index bea28aca811e1386f63cf0e38f6538b40dfae244..f54d7c4f0ae578645d781182f291fb3023fb493b 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 0000000000000000000000000000000000000000..fcd7a57bf74710c05115f5611e008c3052208b1e
--- /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 e3399fb99e840ec8f991da30bde0cc3946c6a0c1..0000000000000000000000000000000000000000
--- 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 0000000000000000000000000000000000000000..2f4edf34b6ad036cdbe4a18909b7340dc5d0286f
--- /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 956c4d338bcb284727e5e5a2de484d1aa7c6974e..afffe816909beaf3baa75d1783955595561663dc 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 cb7f4c5a830ec1dd2eb47209f46504f10ade13f6..dd70d88031fa501b4c8be0162cbcf509cb14950b 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 c45c9fb80b65d5e0699c13ee4de2b4fd424c2124..9a3f621f61ceff37a593a0e1eddc849b6d3706ea 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 bff498c861f7153df61c180ed83e422103bc5bbe..1d0af21a6c27429ec2664b27ac74204e40d39e8d 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 03ba69eb6067dfe6b4acc1e535c503dbd60fce5f..0000000000000000000000000000000000000000
--- 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 28c9da4c0eb8c0b61b2ef542beedf2d1ae325724..0000000000000000000000000000000000000000
--- 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 761a8935ddb19c28b908260f2600e03ba5a8b795..0000000000000000000000000000000000000000
--- 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 374c40165aec1239c2a22b580a36956bd51a7d78..0000000000000000000000000000000000000000
--- 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