aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/Makefile.oug
blob: ee69ea80df018aa62ac39ac7e2d33e27348550a7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
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 ...