dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead code

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13459 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 75 insertions, 2 deletions

diff --git a/Makefile.common b/Makefile.common
index d18cf73d87..77e4d59f29 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -216,8 +216,7 @@ IDECMA:=ide/ide.cma
 
 # modules known by the toplevel of Coq
 
-OBJSMOD:=Coq_config \
- $(foreach lib,$(CORECMA),$(shell cat $(lib:.cma=.mllib)))
+OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib))
 
 IDEMOD:=$(shell cat ide/ide.mllib)
 
diff --git a/dev/Makefile.oug b/dev/Makefile.oug
new file mode 100644
index 0000000000..ee69ea80df
--- /dev/null
+++ b/dev/Makefile.oug
@@ -0,0 +1,74 @@
+#######################################################################
+#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
+# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
+#   \VV/  #############################################################
+#    //   #      This file is distributed under the terms of the      #
+#         #       GNU Lesser General Public License Version 2.1       #
+#######################################################################
+
+
+#### Source Code Analysis via Oug ####
+#### Cf http://home.gna.org/oug ####
+
+
+# To be used from top dir : make -f dev/Makefile.oug ...
+
+include Makefile.build
+
+# Oug location: in the path by default, native version
+
+OUG:=oug.x
+
+# NB: coq should have been compiled with the same ocaml version as oug
+
+# NOTA: it seems we obtain more useless elements reported when _not_
+# providing the .mli files, and also when giving a precise start point.
+# TO BE INVESTIGATED
+
+ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d))))
+local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1)))
+mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i))
+
+# Analysis of coqtop, without plugins
+
+COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA))
+COREMLI:=$(call mli_of_ml,$(COREML))
+
+core.oug:
+	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML)
+
+core.useless: core.oug
+	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@
+
+core_intf.oug:
+	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI)
+
+core_intf.useless: core_intf.oug
+	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@
+
+# Analysis of coqchk, considering only files in the checker/ subdir
+
+CHECKERML:=$(call local_ml_of_cma,checker/check.cma)
+CHECKERMLI:=$(call mli_of_ml,$(CHECKERML))
+
+## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS
+MYCHKINCL:=$(MLINCLUDES) -I checker
+
+checker.oug:
+	$(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI)
+
+checker.useless: checker.oug
+	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@
+
+# Analysis of extraction
+
+EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA))
+EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI))
+
+extraction.oug:
+	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI)
+
+extraction.useless: extraction.oug
+	$(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@
+
+# More to come ...
\ No newline at end of file