diff options
| -rw-r--r-- | caml/Driver.ml | 10 | ||||
| -rwxr-xr-x | configure | 5 | ||||
| -rw-r--r-- | extraction/Makefile | 6 | ||||
| -rw-r--r-- | runtime/Makefile | 3 | ||||
| -rw-r--r-- | test/c/Makefile | 5 | ||||
| -rw-r--r-- | test/cminor/Makefile | 8 |
6 files changed, 25 insertions, 12 deletions
diff --git a/caml/Driver.ml b/caml/Driver.ml index 09c4622..659422e 100644 --- a/caml/Driver.ml +++ b/caml/Driver.ml @@ -98,7 +98,8 @@ module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator) let preprocess ifile ofile = let cmd = - sprintf "gcc -arch ppc -D__COMPCERT__ -I%s %s -E %s > %s" + sprintf "%s -D__COMPCERT__ -I%s %s %s > %s" + Configuration.prepro !stdlib_path (quote_options !prepro_options) ifile ofile in @@ -190,8 +191,8 @@ let compile_cminor_file ifile ofile = let assemble ifile ofile = let cmd = - sprintf "gcc -arch ppc -c -o %s %s" - ofile ifile in + sprintf "%s -o %s %s" + Configuration.asm ofile ifile in let retcode = command cmd in if not !option_dasm then safe_remove ifile; if retcode <> 0 then begin @@ -204,7 +205,8 @@ let assemble ifile ofile = let linker exe_name files = let cmd = - sprintf "gcc -arch ppc -o %s %s -L%s -lcompcert" + sprintf "%s -o %s %s -L%s -lcompcert" + Configuration.linker (Filename.quote exe_name) (quote_options files) !stdlib_path in @@ -40,6 +40,11 @@ cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir +CC=gcc -arch ppc +CPREPRO=gcc -arch ppc -U__GNUC__ -E +CASM=gcc -arch ppc -c +CLINKER=gcc -arch ppc +LIBMATH= EOF # Extract and configure Cil diff --git a/extraction/Makefile b/extraction/Makefile index 5729642..54933cc 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -103,7 +103,11 @@ clean:: rm -f ../caml/CMlexer.ml ../caml/Configuration.ml: ../Makefile.config - echo 'let stdlib_path = "$(LIBDIR)"' > ../caml/Configuration.ml + (echo 'let stdlib_path = "$(LIBDIR)"'; \ + echo 'let prepro = "$(CPREPRO)"'; \ + echo 'let asm = "$(CASM)"'; \ + echo 'let linker = "$(CLINKER)"') \ + > ../caml/Configuration.ml beforedepend:: ../caml/Configuration.ml clean:: diff --git a/runtime/Makefile b/runtime/Makefile index 9a3f621..5f1ddc6 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -1,7 +1,6 @@ include ../Makefile.config -CFLAGS=-arch ppc -O1 -g -Wall -#CFLAGS=-O1 -g -Wall +CFLAGS=-O1 -g -Wall OBJS=stdio.o calloc.o LIB=libcompcert.a INCLUDES=stdio.h diff --git a/test/c/Makefile b/test/c/Makefile index 43b7b15..c6cd928 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,10 +1,11 @@ +include ../../Makefile.config + CCOMP=../../ccomp CCOMPFLAGS=-stdlib ../../runtime -dclight -dasm -CC=gcc -arch ppc CFLAGS=-O1 -Wall -LIBS= +LIBS=$(LIBMATH) TIME=xtime -o /dev/null -mintime 1.0 # Xavier's hack #TIME=time >/dev/null # Otherwise diff --git a/test/cminor/Makefile b/test/cminor/Makefile index 1d0af21..887d1a9 100644 --- a/test/cminor/Makefile +++ b/test/cminor/Makefile @@ -1,9 +1,11 @@ +include ../../Makefile.config + CCOMP=../../ccomp FLAGS=-S CPP=cpp -P -CC=gcc -CFLAGS=-arch ppc -g -ASFLAGS=-arch ppc +AS=$(CASM) +CFLAGS=-g +ASFLAGS= VPATH=../harness ../lib PROGS=fib integr qsort fft sha1 aes almabench manyargs lists \ |