From b6bdb4b4924b0934aed24335597a89e49f7cbd61 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 22 Oct 2006 08:14:51 +0000 Subject: Ajout et utilisation de compcert_stdio.h git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/c/Makefile | 10 ++-- test/c/knucleotide.c | 4 ++ test/c/mandelbrot.c | 4 ++ test/lib/Makefile | 8 +++ test/lib/compcert_stdio.c | 128 ++++++++++++++++++++++++++++++++++++++++++++++ test/lib/compcert_stdio.h | 62 ++++++++++++++++++++++ 6 files changed, 210 insertions(+), 6 deletions(-) create mode 100644 test/lib/Makefile create mode 100644 test/lib/compcert_stdio.c create mode 100644 test/lib/compcert_stdio.h diff --git a/test/c/Makefile b/test/c/Makefile index 9f3c5531..16fead48 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,13 +1,11 @@ CCOMP=../../ccomp -CCOMPFLAGS=-dump-c +CCOMPFLAGS=-dump-c -I../lib -CC=gcc -arch ppc # MacOS X -#CC=gcc # other systems +CC=gcc -arch ppc CFLAGS=-O1 -Wall -LIBS= # MacOS X -#LIBS=-lm # other systems +LIBS= TIME=xtime -o /dev/null -mintime 1.0 # Xavier's hack #TIME=time >/dev/null # Otherwise @@ -23,7 +21,7 @@ all: $(PROGS:%=%.compcert) all_gcc: $(PROGS:%=%.gcc) %.compcert: %.s - $(CC) $(CFLAGS) -o $*.compcert $*.s $(LIBS) + $(CC) $(CFLAGS) -o $*.compcert $*.s ../lib/libcompcert.a $(LIBS) %.s: %.c ../../ccomp $(CCOMP) $(CCOMPFLAGS) $*.c diff --git a/test/c/knucleotide.c b/test/c/knucleotide.c index f7438926..955af7f9 100644 --- a/test/c/knucleotide.c +++ b/test/c/knucleotide.c @@ -8,7 +8,11 @@ http://cvs.alioth.debian.org/cgi-bin/cvsweb.cgi/shootout/bench/Include/?cvsroot=shootout */ +#ifdef __COMPCERT__ +#include +#else #include +#endif #include #include #include diff --git a/test/c/mandelbrot.c b/test/c/mandelbrot.c index 93aa8acb..f4c0db1b 100644 --- a/test/c/mandelbrot.c +++ b/test/c/mandelbrot.c @@ -10,7 +10,11 @@ compile flags: -O3 -ffast-math -march=pentium4 -funroll-loops */ +#ifdef __COMPCERT__ +#include +#else #include +#endif #include int main (int argc, char **argv) diff --git a/test/lib/Makefile b/test/lib/Makefile new file mode 100644 index 00000000..03ba69eb --- /dev/null +++ b/test/lib/Makefile @@ -0,0 +1,8 @@ +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 new file mode 100644 index 00000000..28c9da4c --- /dev/null +++ b/test/lib/compcert_stdio.c @@ -0,0 +1,128 @@ +#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 new file mode 100644 index 00000000..761a8935 --- /dev/null +++ b/test/lib/compcert_stdio.h @@ -0,0 +1,62 @@ +#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 -- cgit