From ca0c62265eb8cdd5fb0d8a8b34ee77baf3de987e Mon Sep 17 00:00:00 2001 From: blazy Date: Fri, 20 Oct 2006 12:37:13 +0000 Subject: Ajout du banc de tests de CCured (Olden benchmark suite, cf. CCured: type-safe retrofitting of legacy code, G.Necula et al.) rapportCompcert_all.txt liste les erreurs produites par ccomp. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/ccured_olden/health/.cvsignore | 30 ++++ test/ccured_olden/health/.gdbinit | 6 + test/ccured_olden/health/CVS/Entries | 16 ++ test/ccured_olden/health/CVS/Repository | 1 + test/ccured_olden/health/CVS/Root | 1 + test/ccured_olden/health/HOWTO | 1 + test/ccured_olden/health/Makefile | 72 ++++++++ test/ccured_olden/health/README | 20 +++ test/ccured_olden/health/args.c | 34 ++++ test/ccured_olden/health/health.c | 309 ++++++++++++++++++++++++++++++++ test/ccured_olden/health/health.h | 76 ++++++++ test/ccured_olden/health/list.c | 55 ++++++ test/ccured_olden/health/out.orig | 64 +++++++ test/ccured_olden/health/out.orig.msvc | 64 +++++++ test/ccured_olden/health/output | 64 +++++++ test/ccured_olden/health/poisson.c | 35 ++++ test/ccured_olden/health/ssplain.c | 70 ++++++++ test/ccured_olden/health/ssplain.h | 130 ++++++++++++++ test/ccured_olden/health/testit | 25 +++ 19 files changed, 1073 insertions(+) create mode 100644 test/ccured_olden/health/.cvsignore create mode 100644 test/ccured_olden/health/.gdbinit create mode 100644 test/ccured_olden/health/CVS/Entries create mode 100644 test/ccured_olden/health/CVS/Repository create mode 100644 test/ccured_olden/health/CVS/Root create mode 100644 test/ccured_olden/health/HOWTO create mode 100644 test/ccured_olden/health/Makefile create mode 100644 test/ccured_olden/health/README create mode 100644 test/ccured_olden/health/args.c create mode 100644 test/ccured_olden/health/health.c create mode 100644 test/ccured_olden/health/health.h create mode 100644 test/ccured_olden/health/list.c create mode 100644 test/ccured_olden/health/out.orig create mode 100644 test/ccured_olden/health/out.orig.msvc create mode 100644 test/ccured_olden/health/output create mode 100644 test/ccured_olden/health/poisson.c create mode 100644 test/ccured_olden/health/ssplain.c create mode 100644 test/ccured_olden/health/ssplain.h create mode 100755 test/ccured_olden/health/testit (limited to 'test/ccured_olden/health') diff --git a/test/ccured_olden/health/.cvsignore b/test/ccured_olden/health/.cvsignore new file mode 100644 index 00000000..4d714a14 --- /dev/null +++ b/test/ccured_olden/health/.cvsignore @@ -0,0 +1,30 @@ +*.o +*.obj +*.exe +*.pdb +*.ilk +*.cpp +*.i +*.s +*.asm +*cil.c +*.rtl +*box.c +*infer.c +*_ppp.c +*.origi +*.stackdump +*_all.c +changes.out +health.cil +health.*box +health.exe_comb.browser +health +allcfiles +ope.m +*cured.c +*.optim.c +*_comb.c +changes +output +out.diff diff --git a/test/ccured_olden/health/.gdbinit b/test/ccured_olden/health/.gdbinit new file mode 100644 index 00000000..ce03cd23 --- /dev/null +++ b/test/ccured_olden/health/.gdbinit @@ -0,0 +1,6 @@ +# .gdbinit + +file health +set args 2 5 1 +break main +run diff --git a/test/ccured_olden/health/CVS/Entries b/test/ccured_olden/health/CVS/Entries new file mode 100644 index 00000000..87bb1a82 --- /dev/null +++ b/test/ccured_olden/health/CVS/Entries @@ -0,0 +1,16 @@ +/.gdbinit/1.1/Sat Jul 21 16:09:41 2001// +/HOWTO/1.1/Sat Jul 14 22:53:03 2001// +/README/1.1/Mon Jun 11 22:47:26 2001// +/health.h/1.3/Sat Jul 21 16:09:41 2001// +/list.c/1.3/Sat Jul 21 16:09:41 2001// +/poisson.c/1.2/Mon Jul 9 16:14:59 2001// +/ssplain.c/1.5/Fri Nov 9 01:27:01 2001// +/args.c/1.5/Mon Nov 12 15:44:12 2001// +/health.c/1.7/Mon Nov 12 15:44:12 2001// +/out.orig/1.2/Mon Nov 12 15:44:12 2001// +/out.orig.msvc/1.1/Tue Dec 4 04:57:46 2001// +/testit/1.2/Tue Dec 4 05:07:50 2001// +/Makefile/1.11/Tue Dec 18 06:56:15 2001// +/.cvsignore/1.14/Fri Oct 4 16:28:44 2002// +/ssplain.h/1.5/Mon Jan 6 23:28:55 2003// +D diff --git a/test/ccured_olden/health/CVS/Repository b/test/ccured_olden/health/CVS/Repository new file mode 100644 index 00000000..8167847a --- /dev/null +++ b/test/ccured_olden/health/CVS/Repository @@ -0,0 +1 @@ +cil/test/olden/health diff --git a/test/ccured_olden/health/CVS/Root b/test/ccured_olden/health/CVS/Root new file mode 100644 index 00000000..35f411e9 --- /dev/null +++ b/test/ccured_olden/health/CVS/Root @@ -0,0 +1 @@ +/home/cvs-repository diff --git a/test/ccured_olden/health/HOWTO b/test/ccured_olden/health/HOWTO new file mode 100644 index 00000000..8f57aa46 --- /dev/null +++ b/test/ccured_olden/health/HOWTO @@ -0,0 +1 @@ +5 500 1 1 diff --git a/test/ccured_olden/health/Makefile b/test/ccured_olden/health/Makefile new file mode 100644 index 00000000..d9c5c767 --- /dev/null +++ b/test/ccured_olden/health/Makefile @@ -0,0 +1,72 @@ +# /* For copyright information, see olden_v1.0/COPYRIGHT */ + +BINARY = health.exe +PROGS = health poisson list args ssplain + +# ------- msvc ------ +ifdef _MSVC +CC = cl + +CFLAGS = +CONLY = /c +SRC = .c +OBJ = .obj +ASM = .s +EXEOUT = /Fe + +EXTRA_CDEFS = /DI_TIME /DI_SYS_TIME /DULTRIX +CDEFS = /DPLAIN /DSS_PLAIN +ifdef _DEBUG +OPTFLAGS = /Zi /MLd +else +OPTFLAGS = /Ox +endif + +LIBS = +LIBPATH = + +# ------- gcc ------ +else +CC = gcc -arch ppc +CCOMP=../../../../ccomp +CCOMPFLAGS=-dump-c + +CFLAGS = -O3 +CONLY = -c +SRC = .c +OBJ = .gcc +OBJCCOMP = .compcert +ASM = .s + +EXTRA_CDEFS = -DI_TIME -DI_SYS_TIME -DULTRIX +CDEFS = -DPLAIN -DSS_PLAIN +OPTFLAGS = -g -Wall -O3 +EXEOUT = -gcc + +LIBS = +LIBPATH = +endif + +# ------- common -------- + +all_s: $(PROGS:%=%.s) + +all: $(PROGS:%=%.compcert) + +all_gcc: $(PROGS:%=%.gcc) + +%.compcert: %.s + $(CC) $(CFLAGS) $(LDFALGS) $(OPTFLAGS) -o $*.compcert $*.s $(LIBS) + +%.s: %.c ../../../../ccomp + $(CCOMP) $(CCOMPFLAGS) $*.c + +%.gcc: %.c + $(CC) $(CFLAGS) $(LDFALGS) $(OPTFLAGS) -o $*.gcc $*.c $(LIBS) + + +clean: + rm -f $(BINARY) *.o *~ *.s *.light.c *.cil.* *.compcert + + + diff --git a/test/ccured_olden/health/README b/test/ccured_olden/health/README new file mode 100644 index 00000000..aff90729 --- /dev/null +++ b/test/ccured_olden/health/README @@ -0,0 +1,20 @@ +/* For copyright information, see olden_v1.0/COPYRIGHT */ +********************** +olden_v1.0/benchmarks/health/README +January 3, 1995 +Martin C. Carlisle + +this directory contains the health benchmark: + +G. Lomow, J. Cleary, B. Unger and D. West. "A Performance Study of Time Warp" +In SCS Multiconference on Distributed Simulation, pages 50-55, Feb. 1988. + +as implemented for Olden by Gordon C. Mackenzie +********************** + +Makefile - use "make health" to create executable + +args.c - process command line args +health.[ch] - health routines +list.c - list routines +poisson.c - random routines diff --git a/test/ccured_olden/health/args.c b/test/ccured_olden/health/args.c new file mode 100644 index 00000000..f8e7a8cc --- /dev/null +++ b/test/ccured_olden/health/args.c @@ -0,0 +1,34 @@ +/* For copyright information, see olden_v1.0/COPYRIGHT */ + +/***************************************************************** + * args.c: Handles arguments to command line. * + * To be used with health.c. * + *****************************************************************/ + +#include +#include +#include "health.h" + +#ifdef SS_PLAIN +#include "ssplain.h" +#endif SS_PLAIN + +void dealwithargs(int argc, char *argv[]) { + + if (argc < 4) + { + fprintf(stderr, "usage: health <# levels>