diff --git a/caml/Driver.ml b/caml/Driver.ml index 09c4622a49d21aee2d8ee1f18c3c4f0dc3eaa6be..659422e98f0f0b023c71f7db42821c10b310cc93 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 diff --git a/configure b/configure index 7214a311025869413b8a7345ef04252aed9ac186..bd1b7bbf6e829aa3922cef63da5451c5bcb98a29 100755 --- a/configure +++ b/configure @@ -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 5729642c27864a2ab5186281fa61a6661e4b1374..54933cc0a329227f006516c38b1dea92faaf842b 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 9a3f621f61ceff37a593a0e1eddc849b6d3706ea..5f1ddc60b92131f9d71b5fee66484cfb911ddbfe 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 43b7b1555c0d2c3a3d6e87e48c5218aff2179bb9..c6cd928908b1b7cb3d82c22c345cdfc3028b9ff4 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 1d0af21a6c27429ec2664b27ac74204e40d39e8d..887d1a9810275c7c1c4644398775691cb3b615b9 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 \