Merge branch 'master' into dwarf

Conflicts:
	powerpc/PrintAsm.ml

1 files changed, 168 insertions, 0 deletions

diff --git a/Makefile.extr b/Makefile.extr
new file mode 100644
index 00000000..266be7c3
--- /dev/null
+++ b/Makefile.extr
@@ -0,0 +1,168 @@
+#######################################################################
+#                                                                     #
+#              The Compcert verified compiler                         #
+#                                                                     #
+#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
+#                                                                     #
+#  Copyright Institut National de Recherche en Informatique et en     #
+#  Automatique.  All rights reserved.  This file is distributed       #
+#  under the terms of the GNU General Public License as published by  #
+#  the Free Software Foundation, either version 2 of the License, or  #
+#  (at your option) any later version.  This file is also distributed #
+#  under the terms of the INRIA Non-Commercial License Agreement.     #
+#                                                                     #
+#######################################################################
+
+# Second-stage Makefile, after Coq extraction
+
+include Makefile.config
+
+# Directories containing plain Caml code (no preprocessing)
+
+DIRS=extraction \
+  lib common $(ARCH) backend cfrontend cparser driver \
+  exportclight debug
+
+# Directories containing Caml code that must be preprocessed by Camlp4
+
+ifeq ($(CCHECKLINK),true)
+DIRS_P4=checklink
+else
+DIRS_P4=
+endif
+
+ALLDIRS=$(DIRS) $(DIRS_P4)
+
+INCLUDES=$(patsubst %,-I %, $(ALLDIRS))
+
+# Control of warnings:
+# warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
+# warning 20 = unused function argument.  There are some in extracted code
+
+WARNINGS=-w -3
+extraction/%.cmx: WARNINGS +=-w -20
+extraction/%.cmo: WARNINGS +=-w -20
+
+COMPFLAGS=-g $(INCLUDES) $(WARNINGS)
+
+# Using the bitstring library and syntax extension (for checklink)
+
+BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o
+
+# Using .opt compilers if available
+
+ifeq ($(OCAML_OPT_COMP),true)
+DOTOPT=.opt
+else
+DOTOPT=
+endif
+
+# Compilers used for non-preprocessed code
+
+OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS)
+OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS)
+OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES)
+
+# Compilers used for Camlp4-preprocessed code.  Note that we cannot
+# use the .opt compilers (because ocamlfind doesn't support them).
+
+OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING)
+OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING)
+OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING)
+
+MENHIR=menhir --explain
+OCAMLLEX=ocamllex -q
+MODORDER=tools/modorder .depend.extr
+
+PARSERS=backend/CMparser.mly cparser/pre_parser.mly
+LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll
+
+LIBS=str.cmxa
+
+EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
+GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml)
+
+# Beginning of part that assumes .depend.extr already exists
+
+ifeq ($(wildcard .depend.extr),.depend.extr)
+
+CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
+
+ccomp: $(CCOMP_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT) -o $@ $(LIBS) $+
+
+ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+
+ifeq ($(CCHECKLINK),true)
+
+CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx)
+
+cchecklink: $(CCHECKLINK_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+
+
+cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+
+
+endif
+
+CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)
+
+clightgen: $(CLIGHTGEN_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT) -o $@ $(LIBS) $+
+
+clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+
+include .depend.extr
+
+endif
+
+# End of part that assumes .depend.extr already exists
+
+checklink/%.cmi: checklink/%.mli
+	@echo "OCAMLC   $<"
+	@$(OCAMLC_P4) -c $<
+checklink/%.cmo: checklink/%.ml
+	@echo "OCAMLC   $<"
+	@$(OCAMLC_P4) -c $<
+checklink/%.cmx: checklink/%.ml
+	@echo "OCAMLOPT $<"
+	@$(OCAMLOPT_P4) -c $<
+
+%.cmi: %.mli
+	@echo "OCAMLC   $<"
+	@$(OCAMLC) -c $<
+%.cmo: %.ml
+	@echo "OCAMLC   $<"
+	@$(OCAMLC) -c $<
+%.cmx: %.ml
+	@echo "OCAMLOPT $<"
+	@$(OCAMLOPT) -c $<
+
+%.ml %.mli: %.mly
+	$(MENHIR) $<
+%.ml: %.mll
+	$(OCAMLLEX) $<
+
+clean:
+	rm -f $(EXECUTABLES)
+	rm -f $(GENERATED)
+	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
+
+# Generation of .depend.extr
+
+depend: $(GENERATED)
+	@echo "Analyzing OCaml dependencies"
+	@for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr
+ifneq ($(strip $(DIRS_P4)),)
+	@for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr
+endif
+
+