Ajout et utilisation de compcert_stdio.h

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 210 insertions, 6 deletions

diff --git a/test/c/Makefile b/test/c/Makefile
index 9f3c553..16fead4 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 f743892..955af7f 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 <compcert_stdio.h>
+#else
 #include <stdio.h>
+#endif
 #include <string.h>
 #include <ctype.h>
 #include <stdlib.h>
diff --git a/test/c/mandelbrot.c b/test/c/mandelbrot.c
index 93aa8ac..f4c0db1 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 <compcert_stdio.h>
+#else
 #include <stdio.h>
+#endif
 #include <stdlib.h>
 
 int main (int argc, char **argv)
diff --git a/test/lib/Makefile b/test/lib/Makefile
new file mode 100644
index 0000000..03ba69e
--- /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 0000000..28c9da4
--- /dev/null
+++ b/test/lib/compcert_stdio.c
@@ -0,0 +1,128 @@
+#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
new file mode 100644
index 0000000..761a893
--- /dev/null
+++ b/test/lib/compcert_stdio.h
@@ -0,0 +1,62 @@
+#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