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

Makefile

+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
 

caml/Main2.ml → caml/Driver.ml

 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:
@@ -28,49 +69,49 @@ module TypeSpecifierTranslator = struct
     | IUShort    -> Some (I16, Unsigned)
     | ILong      -> Some (I32, Signed)
     | IULong     -> Some (I32, Unsigned)
-    | ILongLong  -> (***Some (I32, Signed)***) None
-    | IULongLong -> (***Some (I32, Unsigned)***) None
+    | 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 -> (***Some F64***) None
+    | FLongDouble -> if !option_flonglong then Some F64 else None
 	
 end
 
 module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
 
-let prepro_options = ref []
-let save_csyntax = ref false
+(* From C to preprocessed C *)
 
-let preprocess file =
-  let temp = Filename.temp_file "compcert" ".i" in
+let preprocess ifile ofile =
   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)
+    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
 
-let process_c_file sourcename =
-  let targetname = Filename.chop_suffix sourcename ".c" in
-  (* Preprocessing with cpp *)
-  let preproname = preprocess sourcename in
+(* From preprocessed C to asm *)
+
+let compile_c_file sourcename ifile ofile =
   (* Parsing and production of a CIL.file *)
   let cil =
     try
-      Frontc.parse preproname ()
+      Frontc.parse ifile ()
     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 *)
+  (* 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;
@@ -86,7 +127,8 @@ let process_c_file sourcename =
         eprintf "%s\nPlease report it.\n" msg;
         exit 2 in
   (* Save Csyntax if requested *)
-  if !save_csyntax then begin
+  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
@@ -96,71 +138,208 @@ let process_c_file sourcename =
     match Main.transf_c_program csyntax with
     | Errors.OK x -> x
     | Errors.Error msg ->
-        eprintf "Error in translation Csyntax -> PPC\n";
+        print_error stderr msg;
         exit 2 in
   (* Save PPC asm *)
-  let oc = open_out (targetname ^ ".s") in
+  let oc = open_out ofile 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
+(* 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 ->
-        eprintf "Compiler failure\n";
+        print_error stderr msg;
         exit 2
     | Errors.OK p ->
-        let oc = open_out targetname in
+        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"
-                 sourcename (Lexing.lexeme_start lb);
+                 ifile (Lexing.lexeme_start lb);
          exit 2
      | CMlexer.Error msg ->  
          eprintf "File %s, character %d: %s\n"
-                 sourcename (Lexing.lexeme_start lb) msg;
+                 ifile (Lexing.lexeme_start lb) msg;
          exit 2
      | CMtypecheck.Error msg ->
          eprintf "File %s, type-checking error:\n%s"
-                 sourcename msg;
+                 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 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;
+    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
-      process_c_file s;
+      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
+  parse_cmdline 1;
+  if not (!option_c || !option_S || !option_E) then begin
+    linker !exe_name !linker_options
+  end

configure

+#!/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

extraction/Makefile

+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
 
 

runtime/Makefile

+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)

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
 

test/lib/Makefile

-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

test/lib/compcert_stdio.c

-#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);
-}

test/lib/compcert_stdio.h

-#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

test/lib/staticlib.S

-/* 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