Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


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

1 files changed, 12 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 5d572eb..84fc5cf 100644
--- a/Makefile
+++ b/Makefile
@@ -52,7 +52,6 @@ BACKEND=\
   Tailcall.v Tailcallproof.v \
   RTLtyping.v \
   Kildall.v \
-  CastOptim.v CastOptimproof.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CSE.v CSEproof.v \
   Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \
@@ -70,6 +69,8 @@ BACKEND=\
   Machsem.v \
   Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v
 
+#  CastOptim.v CastOptimproof.v \
+
 # C front-end modules (in cfrontend/)
 
 CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \
@@ -136,16 +137,23 @@ doc/coq2html: doc/coq2html.ml
 doc/coq2html.ml: doc/coq2html.mll
 	ocamllex doc/coq2html.mll
 
+tools/ndfun: tools/ndfun.ml
+	ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
+
 latexdoc:
 	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
 
-.SUFFIXES: .v .vo
-
-.v.vo:
+%.vo: %.v
 	@rm -f doc/glob/$(*F).glob
 	@echo "COQC $*.v"
 	@$(COQC) -dump-glob doc/$(*F).glob $*.v
 
+%.v: %.vp tools/ndfun
+	@rm -f $*.v
+	@echo "Preprocessing $*.vp"
+	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
+	@chmod -w $*.v
+
 driver/Configuration.ml: Makefile.config
 	(echo let stdlib_path = "\"$(LIBDIR)\""; \
          echo let prepro = "\"$(CPREPRO)\""; \