From 94aea0609bb54f0fde29a558366b646b3b8d21a2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 6 Aug 2007 08:45:25 +0000 Subject: 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 | 23 ++-- caml/Driver.ml | 345 ++++++++++++++++++++++++++++++++++++++++++++++ caml/Main2.ml | 166 ---------------------- configure | 42 ++++++ extraction/.depend | 230 ++++++++++++++++--------------- extraction/Makefile | 22 ++- runtime/Makefile | 7 + test/cminor/Makefile | 2 +- test/lib/Makefile | 8 -- test/lib/compcert_stdio.c | 128 ----------------- test/lib/compcert_stdio.h | 62 --------- test/lib/staticlib.S | 27 ---- 12 files changed, 548 insertions(+), 514 deletions(-) create mode 100644 caml/Driver.ml delete mode 100644 caml/Main2.ml create mode 100755 configure delete mode 100644 test/lib/Makefile delete mode 100644 test/lib/compcert_stdio.c delete mode 100644 test/lib/compcert_stdio.h delete mode 100644 test/lib/staticlib.S 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] +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 .i + -S Compile to assembler only, save result in .s + -c Compile to object file only (no linking), result in .o +Preprocessing options: + -I Add to search path for #include files + -D= Define preprocessor symbol + -U Undefine preprocessor symbol +Compilation options: + -flonglong Treat 'long long' as 'long' and 'long double' as 'double' + -dclight Save generated Clight in .light.c + -dasm Save generated assembly in .s +Linking options: + -l Link library + -L Add to search path for libraries + -o Generate executable in (default: a.out) +General options: + -stdlib 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 < ../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 -#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 - -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 -- cgit v1.2.3