From ba9cd4f93ef991fa3794d333e8da19878df06e2d Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 09:29:08 +0000 Subject: Simplified stdlib wrapper; use it only under MacOS X git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- runtime/Makefile | 14 ++++-- runtime/calloc.c | 28 ----------- runtime/stdio.c | 151 +++---------------------------------------------------- runtime/stdio.h | 92 ++++----------------------------- 4 files changed, 26 insertions(+), 259 deletions(-) delete mode 100644 runtime/calloc.c (limited to 'runtime') diff --git a/runtime/Makefile b/runtime/Makefile index 5f1ddc6..ef8e21b 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -1,19 +1,27 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall -OBJS=stdio.o calloc.o +OBJS=stdio.o LIB=libcompcert.a INCLUDES=stdio.h +ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) +all: $(LIB) $(INCLUDES) +else +all: +endif + $(LIB): $(OBJS) rm -f $(LIB) ar rcs $(LIB) $(OBJS) -stdio.o: stdio.h - clean: rm -f *.o $(LIB) +ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) install: install -d $(LIBDIR) install -c $(LIB) $(INCLUDES) $(LIBDIR) +else +install: +endif diff --git a/runtime/calloc.c b/runtime/calloc.c deleted file mode 100644 index 8e5e0b6..0000000 --- a/runtime/calloc.c +++ /dev/null @@ -1,28 +0,0 @@ -/* *********************************************************************/ -/* */ -/* The Compcert verified compiler */ -/* */ -/* Xavier Leroy, INRIA Paris-Rocquencourt */ -/* */ -/* Copyright Institut National de Recherche en Informatique et en */ -/* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ -/* */ -/* *********************************************************************/ - -#include -#include -#include - -void * compcert_alloc(int sz) -{ - void * res = malloc(sz); - if (res == NULL) { - fprintf(stderr, "Out of memory in compcert_alloc().\n"); - abort(); - } - return res; -} diff --git a/runtime/stdio.c b/runtime/stdio.c index 5a2f33e..881a7fa 100644 --- a/runtime/stdio.c +++ b/runtime/stdio.c @@ -13,150 +13,11 @@ /* */ /* *********************************************************************/ -#include -#include -#define _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY -#include "stdio.h" +/* Thin wrapper around stdio, redefining stdin, stdout and stderr. + Needed under MacOS X because of linking issues with dynamic libraries. */ -static compcert_FILE * compcert_alloc_file(FILE * f) -{ - struct compcert_FILE_ * r; - r = malloc(sizeof(struct compcert_FILE_)); - if (r == NULL) return NULL; - r->fstr = (void *) f; - return r; -} +#include "/usr/include/stdio.h" -compcert_FILE * compcert_stdin; -compcert_FILE * compcert_stdout; -compcert_FILE * compcert_stderr; - -static __attribute__((constructor)) void compcert_stdio_init(void) -{ - compcert_stdin = compcert_alloc_file(stdin); - compcert_stdout = compcert_alloc_file(stdout); - compcert_stderr = compcert_alloc_file(stderr); -} - -void compcert_clearerr(compcert_FILE * f) -{ - clearerr((FILE *)(f->fstr)); -} - -int compcert_fclose(compcert_FILE * f) -{ - int errcode = fclose((FILE *)(f->fstr)); - free(f); - return errcode; -} - -int compcert_feof(compcert_FILE * f) -{ - return feof((FILE *)(f->fstr)); -} - -int compcert_ferror(compcert_FILE * f) -{ - return ferror((FILE *)(f->fstr)); -} - -int compcert_fflush(compcert_FILE * f) -{ - return fflush((FILE *)(f->fstr)); -} - -int compcert_fgetc(compcert_FILE * f) -{ - return fgetc((FILE *)(f->fstr)); -} - -char *compcert_fgets(char * s, int n, compcert_FILE * f) -{ - return fgets(s, n, (FILE *)(f->fstr)); -} - -compcert_FILE *compcert_fopen(const char * p, const char * m) -{ - FILE * f = fopen(p, m); - if (f == NULL) return NULL; - return compcert_alloc_file(f); -} - -int compcert_fprintf(compcert_FILE * f, const char * s, ...) -{ - va_list ap; - int retcode; - va_start(ap, s); - retcode = vfprintf((FILE *)(f->fstr), s, ap); - va_end(ap); - return retcode; -} - -int compcert_fputc(int c, compcert_FILE * f) -{ - return fputc(c, (FILE *)(f->fstr)); -} - -int compcert_fputs(const char * s, compcert_FILE * f) -{ - return fputs(s, (FILE *)(f->fstr)); -} - -size_t compcert_fread(void * s, size_t p, size_t q, compcert_FILE * f) -{ - return fread(s, p, q, (FILE *)(f->fstr)); -} - -compcert_FILE *compcert_freopen(const char * s, const char * m, - compcert_FILE * f) -{ - FILE * nf = freopen(s, m, (FILE *)(f->fstr)); - if (nf == NULL) return NULL; - f->fstr = nf; - return f; -} - -int compcert_fscanf(compcert_FILE * f, const char * s, ...) -{ - va_list ap; - int retcode; - va_start(ap, s); - retcode = vfscanf((FILE *)(f->fstr), s, ap); - va_end(ap); - return retcode; -} - -int compcert_fseek(compcert_FILE * f, long p, int q) -{ - return fseek((FILE *)(f->fstr), p, q); -} - -long compcert_ftell(compcert_FILE *f) -{ - return ftell((FILE *)(f->fstr)); -} - -size_t compcert_fwrite(const void * b, size_t p, size_t q, compcert_FILE * f) -{ - return fwrite(b, p, q, (FILE *)(f->fstr)); -} - -int compcert_getc(compcert_FILE * f) -{ - return getc((FILE *)(f->fstr)); -} - -int compcert_putc(int c , compcert_FILE * f) -{ - return putc(c, (FILE *)(f->fstr)); -} - -void compcert_rewind(compcert_FILE * f) -{ - rewind((FILE *)(f->fstr)); -} - -int compcert_ungetc(int c, compcert_FILE * f) -{ - return ungetc(c, (FILE *)(f->fstr)); -} +FILE * compcert_stdin(void) { return stdin; } +FILE * compcert_stdout(void) { return stdout; } +FILE * compcert_stderr(void) { return stderr; } diff --git a/runtime/stdio.h b/runtime/stdio.h index 9aa3ae1..daf0198 100644 --- a/runtime/stdio.h +++ b/runtime/stdio.h @@ -13,97 +13,23 @@ /* */ /* *********************************************************************/ +/* Thin wrapper around stdio, redefining stdin, stdout and stderr. + Needed under MacOS X because of linking issues with dynamic libraries. */ + #ifndef _COMPCERT_STDIO_H #define _COMPCERT_STDIO_H -#ifdef __GNUC__ -#include_next "stdio.h" -#else #include "/usr/include/stdio.h" -#endif -typedef struct compcert_FILE_ { void * fstr; } compcert_FILE; +extern FILE * compcert_stdin(void); +extern FILE * compcert_stdout(void); +extern FILE * compcert_stderr(void); -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 *); - -#ifndef _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY -#define FILE compcert_FILE #undef stdin -#define stdin compcert_stdin +#define stdin (compcert_stdin()) #undef stdout -#define stdout compcert_stdout +#define stdout (compcert_stdout()) #undef stderr -#define stderr compcert_stderr -#undef clearerr -#define clearerr compcert_clearerr -#undef fclose -#define fclose compcert_fclose -#undef feof -#define feof compcert_feof -#undef ferror -#define ferror compcert_ferror -#undef fflush -#define fflush compcert_fflush -#undef fgetc -#define fgetc compcert_fgetc -#undef fgets -#define fgets compcert_fgets -#undef fopen -#define fopen compcert_fopen -#undef fprintf -#define fprintf compcert_fprintf -#undef fputc -#define fputc compcert_fputc -#undef fputs -#define fputs compcert_fputs -#undef fread -#define fread compcert_fread -#undef freopen -#define freopen compcert_freopen -#undef fscanf -#define fscanf compcert_fscanf -#undef fseek -#define fseek compcert_fseek -#undef ftell -#define ftell compcert_ftell -#undef fwrite -#define fwrite compcert_fwrite -#undef getc -#define getc compcert_getc -#undef getchar -#define getchar() compcert_getc(compcert_stdin) -#undef putc -#define putc compcert_putc -#undef putchar -#define putchar(c) compcert_putc(c, compcert_stdout) -#undef rewind -#define rewind compcert_rewind -#undef ungetc -#define ungetc compcert_ungetc -#endif +#define stderr (compcert_stderr()) #endif -- cgit v1.2.3