1
##########################################################################
3
# This file is part of Frama-C. #
5
# Copyright (C) 2007-2008 #
6
# CEA (Commissariat � l'�nergie Atomique) #
7
# INRIA (Institut National de Recherche en Informatique et en #
10
# you can redistribute it and/or modify it under the terms of the GNU #
11
# Lesser General Public License as published by the Free Software #
12
# Foundation, version 2.1. #
14
# It is distributed in the hope that it will be useful, #
15
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
16
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
17
# GNU Lesser General Public License for more details. #
19
# See the GNU Lesser General Public License version v2.1 #
20
# for more details (enclosed in the file licenses/LGPLv2.1). #
22
##########################################################################
24
###################################
25
# Global variables from configure #
26
###################################
28
VERBOSEMAKE?=@VERBOSEMAKE@
29
ifeq ($(VERBOSEMAKE),yes)
35
# Be on the safe side with \r and cygwin
36
export CYGWIN=nobinmode
39
datarootdir= @datarootdir@
40
datadir = @datadir@/frama-c
41
plugindir =$(datadir)/plugins
42
libdir = $(datadir)/lib
43
exec_prefix= @exec_prefix@
47
# where to install the man page
50
# other variables set by ./configure
53
OCAMLDEP= @OCAMLDEP@ -slash
55
OCAMLYACC= @OCAMLYACC@
56
OCAMLMKTOP= @OCAMLMKTOP@
58
OCAMLBEST= @OCAMLBEST@
60
OCAMLVERSION = @OCAMLVERSION@
61
LOWER_THAN_311= @LOWER_THAN_311@
63
#CAMLP4OOF= @CAMLP4OOF@
64
OCAMLWIN32= @OCAMLWIN32@
65
LOCAL_MACHDEP=@LOCAL_MACHDEP@
67
OCAMLGRAPH = @OCAMLGRAPH@
68
OCAMLGRAPH_LOCAL = @OCAMLGRAPH_LOCAL@
69
HAS_LABLGTK= @HAS_LABLGTK@
70
HAS_LABLGLADECC= @HAS_LABLGLADECC@
71
LABLGLADECC= @LABLGLADECC@ -hide-default
72
HAS_GTKSOURCEVIEW=@HAS_GTKSOURCEVIEW@
73
HAS_GNOMECANVAS=@HAS_GNOMECANVAS@
74
HAS_LEGACY_GTKSOURCEVIEW=@HAS_LEGACY_GTKSOURCEVIEW@
75
HAS_LABLGTK_CUSTOM_MODEL=@HAS_LABLGTK_CUSTOM_MODEL@
97
N_OCAMLOPT =Ocamlopt #
98
N_OCAMLLEX =Ocamllex #
99
N_OCAMLYACC=Ocamlyacc #
105
N_MKTOP =Ocamlmktop #
108
N_MAKING =Generating #
112
N_UNTAR =Unarchiving #
118
###########################
119
# Global plugin variables #
120
###########################
122
ENABLE_MIEL= @ENABLE_MIEL@
123
ENABLE_CXX=@ENABLE_CXX@
124
ENABLE_SLICING=@ENABLE_SLICING@
126
# the directory where compiled plugin files are stored
127
PLUGIN_LIB_DIR=lib/plugins
129
# Shared lists between Makefile.plugin and Makefile.in :
130
# initialized them as "simply extended variables" (with :=)
131
# for a correct behavior of += (see section 6.6 of GNU Make manual)
133
PLUGIN_DYN_EXISTS:="no"
137
PLUGIN_DYN_CMO_LIST :=
138
PLUGIN_DYN_CMX_LIST :=
139
PLUGIN_INTERNAL_CMO_LIST:=
140
PLUGIN_INTERNAL_CMX_LIST:=
141
PLUGIN_DEP_GUI_CMO_LIST:=
142
PLUGIN_DEP_GUI_CMX_LIST:=
143
PLUGIN_GUI_CMO_LIST:=
144
PLUGIN_GUI_CMX_LIST:=
145
PLUGIN_DYN_DEP_GUI_CMO_LIST:=
146
PLUGIN_DYN_DEP_GUI_CMX_LIST:=
147
PLUGIN_DYN_GUI_CMO_LIST :=
148
PLUGIN_DYN_GUI_CMX_LIST :=
149
PLUGIN_TYPES_CMO_LIST :=
150
PLUGIN_TYPES_CMX_LIST :=
151
PLUGIN_GENERATED_LIST :=
154
PLUGIN_DISTRIBUTED_LIST:=
155
PLUGIN_DIST_TARGET_LIST:=
156
PLUGIN_DIST_DOC_LIST:=
157
PLUGIN_BIN_DOC_LIST:=
158
PLUGIN_DIST_EXTERNAL_LIST:=
161
# put here any config option for the binary distribution outside of
165
###############################
166
# Additional global variables #
167
###############################
169
# additional compilation targets for 'make all'.
170
# cannot be delayed after 'make all'
172
ifeq ("$(ENABLE_CXX)","yes")
173
EXTRAS += bin/cxx_translate
176
# Directories containing some source code
177
SRC_DIRS= ptests $(PLUGIN_LIB_DIR)
179
# Directory containing source code documentation
182
# Source files to document
185
# Frama-C directories containing files which are not part of any plugin
186
UNPACKED_DIRS= misc ai memory_state toplevel slicing_types pdg_types \
187
kernel logic cxx_types gui
188
ifneq ($(ENABLE_MIEL),no)
191
UNPACKED_DIRS:= $(addprefix src/, $(UNPACKED_DIRS))
193
UNPACKED_DIRS+= external
196
# Directories containing some source code
197
SRC_DIRS+= $(UNPACKED_DIRS)
199
# Directories to include when compiling
200
INCLUDES=$(addprefix -I , $(UNPACKED_DIRS)) -I $(PLUGIN_LIB_DIR) -I lib
202
# Directories to include for ocamldep
203
INCLUDES_FOR_OCAMLDEP= $(patsubst +%,.,$(INCLUDES) $(GUI_INCLUDES))
206
DEP_FLAGS= $(INCLUDES_FOR_OCAMLDEP)
208
# Files for which dependencies are computed
209
FILES_FOR_OCAMLDEP+=$(PLUGIN_LIB_DIR)/*.mli \
210
$(addsuffix /*.mli, $(UNPACKED_DIRS)) \
211
$(addsuffix /*.ml, $(UNPACKED_DIRS))
213
#OPTIM="-unsafe -noassert"
215
# Flags to use by ocamlc and ocamlopt
216
FLAGS = -w Ael -warn-error A -dtypes $(OPTIM) $(INCLUDES)
217
BFLAGS = $(FLAGS) -g $(COVERAGE_COMPILER_BYTE)
218
OFLAGS = $(FLAGS) $(COVERAGE_COMPILER_OPT)
220
# Libraries generated by Frama-C
224
# Libraries used in Frama-C
225
BYTE_LIBS = nums.cma unix.cma bigarray.cma str.cma dynlink.cma \
226
$(GRAPH_BYTE) $(GEN_BYTE_LIBS)
227
OPT_LIBS = nums.cmxa unix.cmxa bigarray.cmxa str.cmxa
229
ifeq ("$(LOWER_THAN_311)","no")
230
OPT_LIBS+= dynlink.cmxa
233
OPT_LIBS+= $(GRAPH_OPT) $(GEN_OPT_LIBS)
235
# files to be included in the distribution.
236
# plugins may add some files to this list if they include files that are
238
DISTRIB_FILES:=cil/*/*.ml* cil/src/*/*.ml* cil/*/*.in cil/LICENSE \
239
cil/CHANGES cil/doc/*.html cil/doc/*.tex cil/doc/*.gif \
240
cil/doc/*.pdf cil/doc/api/*.html cil/doc/examples/*.txt \
241
doc/manuals/*.pdf doc/README doc/code/*.ml* \
242
doc/code/*.css doc/code/*.txt tests/*/*.c \
243
tests/*/*.h tests/*/*.ml ptests/*.ml* \
244
configure.in Makefile.in Makefile.plugin configure Changelog \
245
config.h.in VERSION \
246
$(filter-out CVS,licenses/*) \
247
share/*.c share/*.h share/Makefile.template \
248
share/jessie/*.c share/jessie/*.h share/why/*.why \
249
$(filter-out %kui%,src/kernel/*.ml*) \
251
src/ai/*.ml* src/buckx/*.ml* src/buckx/*.c \
252
src/gui/*.ml* src/lib/*.ml* src/logic/*.ml* \
253
src/memory_state/*.ml* src/misc/*.ml* src/project/*.ml* \
254
src/toplevel/*.ml* bin/sed_get_make_major bin/sed_get_make_minor \
255
INSTALL .make-clean-stamp .make-ocamlgraph-stamp
261
ifeq (@JESSIE_LOCAL@,yes)
262
all: why byte $(EXTRAS)
263
$(MAKE) $(OCAMLBEST) $(EXTRAS_AFTER_BYTE)
266
$(MAKE) $(OCAMLBEST) $(EXTRAS_AFTER_BYTE)
270
$(call QUIET,'$(N_REMOVING) $(OBJ_PERFCOUNT)') \
271
$(RM) $(OBJ_PERFCOUNT)
273
.PHONY: top opt byte dist bdist archclean rebuild cxx
274
top: bin/toplevel.top$(EXE)
275
byte: bin/toplevel.byte$(EXE)
276
opt: bin/toplevel.opt$(EXE)
279
OPTIM="-unsafe -noassert" $(MAKE) all
281
OPTIM="-unsafe -noassert" $(MAKE) byte
283
ifneq ("$(OCAMLGRAPH_LOCAL)","")
285
$(MAKE) -C $(OCAMLGRAPH_LOCAL) distclean
286
cd $(OCAMLGRAPH_LOCAL) ; ./configure
289
$(MAKE) -C $(OCAMLGRAPH_LOCAL) && $(MAKE) all
303
ifeq ($(USE_COVERAGE_TOOL),yes)
305
COVERAGE_PREPRO=camlp4o -no_quot -filter $(COVERAGE_PATH)/coverage_filter.cmo
306
COVERAGE_COMPILER_BYTE=-I $(COVERAGE_PATH) -pp "$(COVERAGE_PREPRO)"
307
COVERAGE_COMPILER_OPT=-I $(COVERAGE_PATH) -pp "$(COVERAGE_PREPRO)"
308
COVERAGE_LIB_BYTE=coverage.cma
309
COVERAGE_LIB_OPT=coverage.cmxa
312
INCLUDES+=$(COVERAGE_COMPILER_BYTE)
313
GEN_BYTE_LIBS+=$(COVERAGE_LIB_BYTE)
314
GEN_OPT_LIBS+=$(COVERAGE_LIB_OPT)
315
SRC_DIRS+=$(COVERAGE_PATH)
321
ifneq ("$(OCAMLGRAPH_LOCAL)","")
322
lib/graph%: $(OCAMLGRAPH_LOCAL)/graph%
323
$(call QUIET,'$(N_CP) $@') \
326
$(OCAMLGRAPH_LOCAL)/graph.cmo: $(OCAMLGRAPH_LOCAL)/Makefile \
327
$(OCAMLGRAPH_LOCAL)/src/*.ml*
328
$(MAKE) -C $(OCAMLGRAPH_LOCAL) $(notdir $@)
330
$(OCAMLGRAPH_LOCAL)/%.cmi: $(OCAMLGRAPH_LOCAL)/%.cmo
333
$(OCAMLGRAPH_LOCAL)/graph.cmx: $(OCAMLGRAPH_LOCAL)/graph.cmi \
334
$(OCAMLGRAPH_LOCAL)/src/*.ml*
335
$(MAKE) -C $(OCAMLGRAPH_LOCAL) $(notdir $@)
337
$(OCAMLGRAPH_LOCAL)/%.o: $(OCAMLGRAPH_LOCAL)/%.cmx
340
$(OCAMLGRAPH_LOCAL)/Makefile: $(OCAMLGRAPH_LOCAL)/configure \
341
$(OCAMLGRAPH_LOCAL)/Makefile.in
342
cd $(OCAMLGRAPH_LOCAL); ./configure
344
$(OCAMLGRAPH_LOCAL)/configure: $(OCAMLGRAPH_LOCAL)/configure.in
345
cd $(OCAMLGRAPH_LOCAL); autoconf
347
# Correct over-approximation: all frama-c source files depend on ocamlgraph
348
# Required because ocamldep doesn't see any dependency to packed module
349
src/*/*.cmi: lib/graph.cmi
350
src/*/*.cmo src/*/*.cma: lib/graph.cmo
351
src/*/*.cmxa src/*/*.cmx: lib/graph.cmx
353
GENERATED+= lib/graph.cmo lib/graph.cmx lib/graph.o lib/graph.cmi
357
GRAPH_BYTE_LIBS=lib/graph.cmo
358
GRAPH_OPT_LIBS=lib/graph.cmx
359
GEN_BYTE_LIBS+=$(GRAPH_BYTE_LIBS)
360
GEN_OPT_LIBS+=$(GRAPH_OPT_LIBS)
362
# viewgraph (included in ocamlgraph)
363
ifeq ($(HAS_GNOMECANVAS),yes)
364
ifeq (@ENABLE_SYNTACTIC_CALLGRAPH@,yes)
366
$(OCAMLGRAPH_LOCAL)/view_graph/%.cmo: $(OCAMLGRAPH_LOCAL)/graph.cmi \
367
$(OCAMLGRAPH_LOCAL)/view_graph/%.ml
368
$(MAKE) -C $(OCAMLGRAPH_LOCAL) $(patsubst $(OCAMLGRAPH_LOCAL)/%,%,$@)
370
$(OCAMLGRAPH_LOCAL)/view_graph/%.cmx: $(OCAMLGRAPH_LOCAL)/graph.cmx \
371
$(OCAMLGRAPH_LOCAL)/view_graph/%.ml
372
$(MAKE) -C $(OCAMLGRAPH_LOCAL) $(patsubst $(OCAMLGRAPH_LOCAL)/%,%,$@)
374
lib/viewGraph%: $(OCAMLGRAPH_LOCAL)/view_graph/viewGraph%
375
$(call QUIET,'$(N_CP) $@') \
378
GRAPH_GUICMO= lib/viewGraph.cmo lib/viewGraph_select.cmo
379
GRAPH_GUICMX= $(GRAPH_GUICMO:.cmo=.cmx)
381
GENERATED+= lib/viewGraph.cmo lib/viewGraph.cmx lib/viewGraph.o \
382
lib/viewGraph.cmi lib/viewGraph_select.cmo lib/viewGraph_select.cmx \
383
lib/viewGraph_select.o lib/viewGraph_select.cmi
385
INCLUDES_FOR_OCAMLDEP+=-I $(OCAMLGRAPH_LOCAL)/view_graph
389
endif # viewgraph available
391
# If 'make untar-ocamlgraph' have to be performed after 'cvs update':
392
# change '.make-ocamlgraph-stamp' before 'cvs commit'
393
.make-ocamlgraph: .make-ocamlgraph-stamp
395
$(MAKE) untar-ocamlgraph
397
include .make-ocamlgraph
399
# force "make untar-ocamlgraph" to be executed for all users of CVS
401
expr `$(CAT) .make-ocamlgraph-stamp` + 1 > .make-ocamlgraph-stamp
403
.PHONY: untar-ocamlgraph
404
untar-ocamlgraph: ocamlgraph.tar.gz
405
$(call QUIET,'$(N_UNTAR) $@') \
406
($(RM) -r $(OCAMLGRAPH_LOCAL); \
409
else # does not use ocamlgraph local version
411
INCLUDES+=$(OCAMLGRAPH)
415
# viewgraph (included in ocamlgraph)
416
ifeq ($(HAS_GNOMECANVAS),yes)
417
ifeq (@ENABLE_SYNTACTIC_CALLGRAPH@,yes)
418
GRAPH_GUICMO= viewGraph.cmo viewGraph_select.cmo
419
GRAPH_GUICMX= $(GRAPH_GUICMO:.cmo=.cmx)
424
endif # whether ocamlgraph is local
426
####################################
427
# Internal miscellaneous libraries #
428
####################################
431
LIB_CMO = myDynlink extlib pretty_utils hook mergemap rangemap \
432
binary_cache ptset type funTbl journal
433
LIB_CMO:= $(patsubst %, $(LIB_PATH)/%.cmo, $(LIB_CMO))
434
LIB_CMX = $(LIB_CMO:.cmo=.cmx)
435
LIB_CMI = $(LIB_CMO:.cmo=.cmi)
437
$(LIB_CMI) $(LIB_CMO) $(LIB_CMX): INCLUDES=-I $(LIB_PATH) -I src/project \
440
MODULES_TODOC+= $(LIB_PATH)/myDynlink.mli $(LIB_PATH)/extlib.mli \
441
$(LIB_PATH)/pretty_utils.mli $(LIB_PATH)/hook.mli \
442
$(LIB_PATH)/mergemap.mli $(LIB_PATH)/rangemap.mli \
443
$(LIB_PATH)/binary_cache.mli $(LIB_PATH)/ptset.mli \
444
$(LIB_PATH)/type.mli $(LIB_PATH)/funTbl.mli $(LIB_PATH)/journal.mli \
446
INCLUDES+=-I $(LIB_PATH)
447
# binary_cache and ptset depends of project.
448
# So delay its addition to GEN_*_LIBS
449
GEN_BYTE_LIBS+=$(filter-out $(LIB_PATH)/binary_cache.cmo $(LIB_PATH)/ptset.cmo, $(LIB_CMO))
450
GEN_OPT_LIBS+=$(filter-out $(LIB_PATH)/binary_cache.cmx $(LIB_PATH)/ptset.cmx, $(LIB_CMX))
451
FILES_FOR_OCAMLDEP+=$(addsuffix /*.mli, $(LIB_PATH)) \
452
$(addsuffix /*.ml, $(LIB_PATH))
453
SRC_DIRS+=$(LIB_PATH)
458
GENERATED += src/lib/myDynlink.ml
459
src/lib/myDynlink.ml: Makefile
461
ifeq ("$(LOWER_THAN_311)","yes")
464
src/lib/myDynlink.ml: src/lib/dynlink_lower_311_byte.ml
465
$(call QUIET,'$(N_CP) $@') \
469
src/lib/myDynlink.cmo: src/lib/dynlink_lower_311_byte.ml
470
$(call QUIET,'$(N_CP) src/lib/myDynlink.ml') \
471
($(CP) $< src/lib/myDynlink.ml; \
472
$(CHMOD_RO) src/lib/myDynlink.ml)
473
$(call QUIET,'$(N_OCAMLC) $@') \
474
$(OCAMLC) -c $(BFLAGS) src/lib/myDynlink.ml
476
src/lib/myDynlink.o src/lib/myDynlink.cmx: src/lib/dynlink_lower_311_opt.ml
477
$(call QUIET,'$(N_CP) src/lib/myDynlink.ml') \
478
($(CP) $< src/lib/myDynlink.ml; \
479
$(CHMOD_RO) src/lib/myDynlink.ml)
480
$(call QUIET,'$(N_OCAMLOPT) $@') \
481
$(OCAMLOPT) -c $(OFLAGS) src/lib/myDynlink.ml
485
src/lib/myDynlink.ml: src/lib/dynlink_311_or_higher.ml
486
$(call QUIET,'$(N_CP) $@') \
496
PROJECT_PATH=src/project
497
PROJECT_CMO= qstack namespace kind project datatype computation
498
PROJECT_CMO:= $(patsubst %, $(PROJECT_PATH)/%.cmo, $(PROJECT_CMO))
499
PROJECT_CMX= $(PROJECT_CMO:.cmo=.cmx)
500
PROJECT_CMI= signature.cmi $(PROJECT_CMO:.cmo=.cmi)
502
PROJECT_CMA=$(PROJECT_PATH)/project.cma
503
PROJECT_CMXA=$(PROJECT_CMA:.cma=.cmxa)
505
$(PROJECT_CMA): $(PROJECT_CMO)
506
$(call QUIET,'$(N_LINKING) $@') \
507
$(OCAMLC) -a -o $@ $(PROJECT_CMO)
509
$(PROJECT_CMXA): $(PROJECT_CMX)
510
$(call QUIET,'$(N_LINKING) $@') \
511
$(OCAMLOPT) -a -o $@ $(PROJECT_CMX)
513
MODULES_TODOC+= $(PROJECT_PATH)/kind.mli $(PROJECT_PATH)/project.mli \
514
$(PROJECT_PATH)/signature.mli $(PROJECT_PATH)/namespace.mli \
515
$(PROJECT_PATH)/datatype.mli $(PROJECT_PATH)/computation.mli
517
$(PROJECT_CMI) $(PROJECT_CMO) $(PROJECT_CMX): INCLUDES=-I $(PROJECT_PATH) \
518
-I $(LIB_PATH) $(OCAMLGRAPH)
520
INCLUDES+=-I $(PROJECT_PATH)
521
GEN_BYTE_LIBS+=$(PROJECT_CMA) $(LIB_PATH)/binary_cache.cmo
522
GEN_OPT_LIBS+=$(PROJECT_CMXA) $(LIB_PATH)/binary_cache.cmx
523
FILES_FOR_OCAMLDEP+=$(addsuffix /*.mli, $(PROJECT_PATH)) \
524
$(addsuffix /*.ml, $(PROJECT_PATH))
525
SRC_DIRS+=$(PROJECT_PATH)
530
PLUGIN_TESTS_LIST += saveload
532
tests/saveload/%.cmx: tests/saveload/%.ml $(GEN_OPT_LIBS)
533
$(OCAMLOPT) -c $(OFLAGS) -I tests/saveload $(OPT_LIBS) $<
535
tests/saveload/%.opt: tests/saveload/%.cmx bin/toplevel.opt$(EXE)
536
$(OCAMLOPT) $(OFLAGS) -o $@ -I tests/saveload \
537
$(OPT_LIBS) $< $(ALL_CMX) $(STARTUPCMX)
539
tests/saveload/%.cmo: tests/saveload/%.ml $(GEN_BYTE_LIBS)
540
$(OCAMLC) -c $(BFLAGS) -I tests/saveload $(BYTE_LIBS) $<
542
tests/saveload/%.byte: tests/saveload/%.cmo bin/toplevel.byte$(EXE)
543
$(OCAMLC) $(BFLAGS) -o $@ -I tests/saveload \
544
$(BYTE_LIBS) $< $(ALL_CMO) $(STARTUPCMO)
546
# Testing dynamic loading
547
##########################
549
PLUGIN_TESTS_LIST += dynamic
551
DYNAMIC_TESTS_TARGETS:=tests/dynamic/empty.cmo tests/dynamic/empty_gui.cmo \
552
tests/dynamic/.cmo tests/dynamic/empty.cmofoo \
553
tests/dynamic/Register_mod1.cmo tests/dynamic/Register_mod2.cmo \
554
tests/dynamic/Apply.cmo
556
tests/dynamic/%.cmo: tests/dynamic/%.ml $(GEN_BYTE_LIBS)
557
$(OCAMLC) -c $(BFLAGS) -I tests/dynamic $<
559
tests/dynamic_plugin/%.cmo: tests/dynamic_plugin/%.ml $(GEN_BYTE_LIBS)
560
$(OCAMLC) -c $(BFLAGS) -I tests/dynamic_plugin $<
562
tests/dynamic/.cmi tests/dynamic/empty.cmifoo:tests/dynamic/empty.cmi
565
tests/dynamic/.cmo tests/dynamic/empty.cmofoo:tests/dynamic/empty.cmo \
566
tests/dynamic/.cmi tests/dynamic/empty.cmifoo
569
tests/dynamic/Register_mod1.cmo:tests/dynamic_plugin/register_mod1.cmo
570
$(OCAMLC) -o $@ -pack $^
572
tests/dynamic/Register_mod2.cmo:tests/dynamic_plugin/register_mod2.cmo
573
$(OCAMLC) -o $@ -pack $^
575
tests/dynamic/Apply.cmo:tests/dynamic_plugin/apply.cmo
576
$(OCAMLC) -o $@ -pack $^
578
.PHONY:tests/dynamic/all
580
$(RM) tests/dynamic/.cm* tests/dynamic/*.cm* tests/dynamic_plugin/*.cm*
581
$(MAKE) $(DYNAMIC_TESTS_TARGETS)
589
BUCKX_CMO:= $(patsubst %, $(BUCKX_PATH)/%.cmo, $(BUCKX_CMO))
590
BUCKX_CMX= $(BUCKX_CMO:.cmo=.cmx)
591
BUCKX_CMI= $(BUCKX_CMO:.cmo=.cmi)
593
MODULES_TODOC+= $(BUCKX_PATH)/buckx.mli
595
$(BUCKX_CMI) $(BUCKX_CMO) $(BUCKX_CMX): INCLUDES=-I $(BUCKX_PATH) \
598
INCLUDES+=-I $(BUCKX_PATH)
599
GEN_BUCKX=src/buckx/mybigarray.o src/buckx/buckx_c.o
600
GEN_BYTE_LIBS+=$(GEN_BUCKX) $(BUCKX_CMO)
601
GEN_OPT_LIBS+=$(GEN_BUCKX) $(BUCKX_CMX)
602
FILES_FOR_OCAMLDEP+=$(addsuffix /*.mli, $(BUCKX_PATH)) \
603
$(addsuffix /*.ml, $(BUCKX_PATH))
604
SRC_DIRS+=$(BUCKX_PATH)
606
src/buckx/buckx_c.o: src/buckx/buckx_c.c
607
$(call QUIET,'$(N_OCAMLC) $@') \
608
$(OCAMLC) $(BFLAGS) -ccopt "-O3 -fno-pic -fomit-frame-pointer -o $@" $<
617
ifeq ("$(LOCAL_MACHDEP)","yes")
619
# Create the machine dependency module
620
# If the cl command cannot be run then the MSVC part will be identical to GCC
621
.PHONY : machdep $(CIL_PATH)/local_machdep.ml
622
machdep: $(CIL_PATH)/local_machdep.ml
623
bin/machdep.exe: machdep
625
$(CIL_PATH)/local_machdep.ml : cil/src/machdep.c configure.in Makefile.in
626
$(call QUIET,'$(N_MAKING) $@') \
628
$(ECHO) "(* This module was generated automatically by code in Makefile and machdep.c *)" >$@; \
629
# Now generate the type definition
630
$(ECHO) "open Cil_types" >> $@; \
631
if gcc -D_GNUCC $< -o bin/machdep.exe ;then \
632
$(ECHO) "machdep.exe created succesfully." \
636
$(ECHO) "let gcc = {" >>$@; \
637
bin/machdep.exe >>$@; \
638
$(ECHO) " underscore_name = @UNDERSCORE_NAME@ ;" >> $@;\
640
if cl /D_MSVC $< /Febin/machdep.exe /Fobin/machdep.obj ;then \
641
$(ECHO) "let hasMSVC = true" >>$@ \
643
$(ECHO) "let hasMSVC = false" >>$@ ;fi; \
644
$(ECHO) "let msvc = {" >>$@; \
645
bin/machdep.exe >>$@; \
646
$(ECHO) " underscore_name = true ;" >> $@; \
648
$(ECHO) "let gccHas__builtin_va_list = @HAVE_BUILTIN_VA_LIST@" >>$@; \
649
$(ECHO) "let __thread_is_keyword = @THREAD_IS_KEYWORD@" >>$@; \
650
$(ECHO) "$@ generated. You may have this file merged into Frama-C by developers."; \
655
# Create the cil version information module
657
cilversion: $(CIL_PATH)/cilversion.ml
658
GENERATED += $(CIL_PATH)/cilversion.ml
659
$(CIL_PATH)/cilversion.ml: Makefile.in
660
$(call QUIET,'$(N_MAKING) $@') \
662
$(ECHO) "(* This module was generated automatically by code in Makefile *)" >$@; \
663
$(ECHO) "let cilVersionMajor = 1" >>$@; \
664
$(ECHO) "let cilVersionMinor = 3" >>$@; \
665
$(ECHO) "let cilVersionRev = 6" >>$@; \
666
$(ECHO) "let cilVersion = \"1.3.6\"" >>$@; \
669
# Performance counters
670
PERFCOUNT=cil/ocamlutil/perfcount
672
ifeq ($(USE_PERFCOUNT),yes)
673
OBJ_PERFCOUNT=$(PERFCOUNT).o
674
STATS=cil/ocamlutil/stats.cmo
681
CIL_CMO = cil/ocamlutil/pretty.cmo \
682
cil/ocamlutil/errormsg.cmo \
683
cil/ocamlutil/alpha.cmo cil/ocamlutil/clist.cmo \
684
cil/ocamlutil/growArray.cmo \
685
cil/ocamlutil/inthash.cmo $(STATS) \
686
cil/ocamlutil/trace.cmo cil/ocamlutil/cilutil.cmo \
687
cil/ocamlutil/setWithNearest.cmo \
688
$(addprefix $(CIL_PATH)/, \
689
cil_datatype.cmo cil_computation.cmo \
690
logic/utf8_logic.cmo \
691
messages_manager.cmo \
694
machdep_x86_16.cmo machdep_x86_32.cmo machdep_x86_64.cmo \
695
machdep_ppc_32.cmo machdep_ppc_32_diab.cmo \
696
machdep.cmo logic/logic_env.cmo \
697
escape.cmo cil.cmo frontc/cabs.cmo \
698
frontc/cabshelper.cmo frontc/whitetrack.cmo \
699
logic/logic_const.cmo \
700
logic/logic_parser.cmo logic/logic_lexer.cmo \
701
frontc/lexerhack.cmo \
702
mergecil.cmo rmtmps.cmo testcil.cmo \
703
logic/logic_typing.cmo \
705
frontc/cabsvisit.cmo frontc/cabs2cil.cmo \
706
frontc/clexer.cmo frontc/cparser.cmo \
707
logic/logic_preprocess.cmo \
708
frontc/patch.cmo frontc/frontc.cmo \
709
ext/obfuscate.cmo ext/ciltools.cmo \
710
ext/callgraph.cmo ext/dataflow.cmo ext/dominators.cmo \
711
ext/oneret.cmo ext/cfg.cmo ext/expcompare.cmo \
712
ext/usedef.cmo ext/liveness.cmo ext/reachingdefs.cmo \
713
ext/availexpslv.cmo ext/rmciltmps.cmo ext/deadcodeelim.cmo \
714
zrapp.cmo) # end of addprefix
715
CIL_CMX = $(CIL_CMO:.cmo=.cmx)
716
CIL_CMI = cil/src/cil_types.cmi cil/src/logic/logic_ptree.cmi \
719
GENERATED += $(addprefix $(CIL_PATH)/, \
720
frontc/clexer.ml frontc/cparser.ml frontc/cparser.mli \
721
logic/logic_lexer.ml logic/logic_parser.ml \
722
logic/logic_parser.mli logic/logic_preprocess.ml \
725
MODULES_TODOC += cil/ocamlutil/pretty.mli \
726
cil/ocamlutil/errormsg.mli \
727
cil/ocamlutil/alpha.mli cil/ocamlutil/clist.mli \
728
cil/ocamlutil/growArray.mli \
729
cil/ocamlutil/inthash.mli cil/ocamlutil/stats.mli \
730
cil/ocamlutil/trace.mli cil/ocamlutil/cilutil.mli \
731
cil/ocamlutil/setWithNearest.mli \
732
$(addprefix $(CIL_PATH)/, \
733
messages_manager.mli \
735
cilversion.ml machdep.mli \
737
escape.mli cil.mli frontc/cabs.ml \
738
frontc/cabshelper.mli frontc/whitetrack.mli \
739
logic/logic_parser.mli \
740
frontc/lexerhack.ml \
741
mergecil.mli rmtmps.mli \
742
logic/logic_const.ml logic/logic_typing.mli \
743
frontc/cprint.mli frontc/cabsvisit.mli frontc/cabs2cil.mli \
744
frontc/cparser.mli logic/logic_preprocess.mli \
745
frontc/patch.mli frontc/frontc.mli \
746
logic/logic_ptree.mli \
748
ext/callgraph.mli ext/dataflow.mli ext/dominators.mli \
749
ext/oneret.mli) # end of addprefix
751
CIL_CMA =$(CIL_PATH)/cil.cma
752
CIL_CMXA=$(CIL_PATH)/cil.cmxa
754
$(CIL_CMA): $(CIL_CMO) $(OBJ_PERFCOUNT)
755
$(call QUIET,'$(N_LINKING) $@') \
756
$(OCAMLC) -a -custom -o $@ $(CIL_CMO) $(OBJ_PERFCOUNT)
757
$(CIL_CMXA): $(CIL_CMX) $(OBJ_PERFCOUNT)
758
$(call QUIET,'$(N_LINKING) $@') \
759
$(OCAMLOPT) -a -o $@ $(CIL_CMX) $(OBJ_PERFCOUNT)
761
CIL_DIRS= $(CIL_PATH) $(CIL_PATH)/ext $(CIL_PATH)/frontc $(CIL_PATH)/logic \
764
SRC_DIRS+=$(CIL_DIRS)
766
$(CIL_CMI) $(CIL_CMO) $(CIL_CMX):INCLUDES=$(addprefix -I , $(CIL_DIRS) \
767
$(LIB_PATH) $(PROJECT_PATH)) $(OCAMLGRAPH)
769
INCLUDES+=$(addprefix -I , $(CIL_DIRS))
770
GEN_BYTE_LIBS+=$(CIL_CMA)
771
GEN_OPT_LIBS+=$(CIL_CMXA)
772
FILES_FOR_OCAMLDEP+=$(addsuffix /*.mli, $(CIL_DIRS)) \
773
$(addsuffix /*.ml, $(CIL_DIRS))
775
.PHONY : cil.byte cil.opt
776
cil.byte: $(CIL_PATH)/cil.cma
777
cil.opt: $(CIL_PATH)/cil.cmxa
783
# modules to be linked before ptmap
784
PRECMO = src/kernel/version.cmo src/kernel/ast_printer.cmo \
785
src/kernel/ast_info.cmo \
786
src/kernel/kernel_type.cmo src/kernel/alarms.cmo src/kernel/cilE.cmo \
787
src/kernel/cil_state.cmo
789
PRECMX = $(PRECMO:.cmo=.cmx)
791
PRECMI = $(PRECMO:.cmo=.cmi)
793
$(PRECMI) $(PRECMO) $(PRECMX): INCLUDES= $(addprefix -I , $(CIL_DIRS)) \
794
-I $(LIB_PATH) -I $(BUCKX_PATH) -I $(PROJECT_PATH) -I src/kernel
796
GEN_BYTE_LIBS+=$(PRECMO)
797
GEN_OPT_LIBS+=$(PRECMX)
800
#################################
801
# External libraries to compile #
802
#################################
804
EXTERNAL_PATH= external
805
EXTERNAL_CMO = ptmap #size
806
EXTERNAL_CMO:= $(patsubst %, $(EXTERNAL_PATH)/%.cmo, $(EXTERNAL_CMO))
807
EXTERNAL_CMX:= $(EXTERNAL_CMO:.cmo=.cmx)
808
EXTERNAL_CMI:= $(EXTERNAL_CMO:.cmo=.cmi)
810
$(EXTERNAL_CMI) $(EXTERNAL_CMO) $(EXTERNAL_CMX): INCLUDES=-I $(EXTERNAL_PATH) \
811
-I $(LIB_PATH) -I $(BUCKX_PATH) -I $(PROJECT_PATH) -I src/kernel
813
INCLUDES+=-I $(EXTERNAL_PATH)
814
FILES_FOR_OCAMLDEP+=$(addsuffix /*.mli, $(EXTERNAL_PATH)) \
815
$(addsuffix /*.ml, $(EXTERNAL_PATH))
816
SRC_DIRS+=$(EXTERNAL_PATH)
818
# Ptset depends on Ptmap
819
GEN_BYTE_LIBS+= $(EXTERNAL_CMO) $(LIB_PATH)/ptset.cmo
820
GEN_OPT_LIBS+= $(EXTERNAL_CMX) $(LIB_PATH)/ptset.cmx
826
ACMO = src/ai/my_bigint.cmo \
827
src/ai/abstract_interp.cmo \
828
src/memory_state/mweak.cmo \
829
src/ai/int_Base.cmo \
830
src/kernel/cmdline.cmo \
831
src/kernel/unicode.cmo \
832
src/misc/bit_utils.cmo \
834
src/kernel/annotations.cmo src/kernel/globals.cmo \
835
src/kernel/kernel_function.cmo \
836
src/misc/service_graph.cmo \
838
src/ai/base_Set_Lattice.cmo \
840
src/ai/map_Lattice.cmo \
842
src/memory_state/abstract_value.cmo \
843
src/memory_state/baseUtils.cmo \
844
src/memory_state/locations.cmo \
845
src/memory_state/inout_type.cmo \
846
src/memory_state/shifted_Location.cmo \
847
src/memory_state/path_lattice.cmo \
848
src/memory_state/int_Interv.cmo \
849
src/memory_state/int_Interv_Map.cmo \
850
src/memory_state/offsetmap.cmo \
851
src/memory_state/offsetmap_bitwise.cmo \
852
src/memory_state/lmap.cmo \
853
src/memory_state/lmap_bitwise.cmo \
854
src/memory_state/lmap_whole.cmo \
855
src/memory_state/function_Froms.cmo \
856
src/memory_state/cvalue_type.cmo \
857
src/memory_state/memzone_type.cmo \
858
src/memory_state/widen_type.cmo \
859
src/memory_state/relations_type.cmo \
860
src/logic/why_output.cmo
862
ACMX = $(ACMO:.cmo=.cmx)
864
MODULES_TODOC += src/kernel/version.mli \
865
src/kernel/alarms.mli src/kernel/cilE.mli \
866
src/kernel/ast_info.mli \
867
src/kernel/kernel_type.mli \
868
src/kernel/cil_state.mli \
869
src/ai/my_bigint.ml \
870
src/ai/abstract_interp.mli \
871
src/memory_state/mweak.mli \
873
src/kernel/cmdline.mli \
874
src/misc/bit_utils.mli \
877
src/ai/base_Set_Lattice.ml \
879
src/ai/map_Lattice.ml \
881
src/memory_state/abstract_value.ml \
882
src/toplevel/options.mli \
883
src/memory_state/baseUtils.ml \
884
src/memory_state/locations.mli \
885
src/memory_state/inout_type.ml \
886
src/memory_state/shifted_Location.mli \
887
src/memory_state/path_lattice.mli \
888
src/memory_state/int_Interv.ml \
889
src/memory_state/int_Interv_Map.ml \
890
src/memory_state/offsetmap.mli \
891
src/memory_state/offsetmap_bitwise.mli \
892
src/memory_state/lmap.mli \
893
src/memory_state/lmap_bitwise.mli \
894
src/memory_state/lmap_whole.mli \
895
src/memory_state/function_Froms.ml \
896
src/memory_state/cvalue_type.ml \
897
src/memory_state/memzone_type.ml \
898
src/memory_state/widen_type.mli \
899
src/memory_state/relations_type.mli \
900
src/logic/why_output.mli
902
KERNEL_CMO = src/kernel/stmts_graph.cmo \
903
src/kernel/visitor.cmo \
904
src/kernel/printer.cmo src/kernel/unroll_loops.cmo \
905
src/kernel/loop.cmo \
907
src/kernel/dynamic.cmo \
908
src/toplevel/options.cmo \
909
src/kernel/file.cmo \
913
KERNEL_CMX =$(KERNEL_CMO:.cmo=.cmx)
915
MODULES_TODOC += src/kernel/db_types.mli \
916
src/kernel/stmts_graph.mli \
917
src/kernel/annotations.mli src/kernel/globals.mli \
918
src/kernel/visitor.mli src/kernel/printer.mli \
919
src/kernel/unroll_loops.ml \
920
src/kernel/file.mli src/kernel/kernel_function.mli src/kernel/loop.mli \
921
src/kernel/db.mli src/kernel/dynamic.mli \
924
########################################################
925
# Alias, dependency analysis, locations interpretation #
926
########################################################
928
LOCCMO = src/memory_state/widen.cmo \
929
src/memory_state/memzone.cmo \
930
src/memory_state/bit_model_access.cmo
931
LOCCMX = $(LOCCMO:.cmo=.cmx)
933
MODULES_TODOC += src/memory_state/widen.ml \
934
src/memory_state/memzone.ml \
935
src/memory_state/bit_model_access.mli
941
PLUGIN_ENABLE:=@ENABLE_JOURNAL_LOADER@
942
PLUGIN_NAME:=Journal_loader
943
PLUGIN_DISTRIBUTED:=yes
945
PLUGIN_GUI_HAS_MLI:=yes
946
PLUGIN_DIR:=src/journal_loader
948
PLUGIN_GUI_CMO:=register_gui
950
PLUGIN_TESTS_DIRS:=journal
951
include Makefile.plugin
953
# Disabling warnings for journal
954
tests/journal/result/%.cmo: FLAGS+=-w x
960
PLUGIN_ENABLE:=@ENABLE_OCCURRENCE@
961
PLUGIN_NAME:=Occurrence
962
PLUGIN_DISTRIBUTED:=yes
964
PLUGIN_GUI_HAS_MLI:=yes
965
PLUGIN_DIR:=src/occurrence
966
PLUGIN_CMO:= register
967
PLUGIN_GUI_CMO:=register_gui
968
include Makefile.plugin
970
######################
971
# Occurrence dynamic #
972
######################
973
# PLUGIN_ENABLE:=@ENABLE_OCCURRENCE_DYN@
974
# PLUGIN_DYNAMIC:=yes
975
# PLUGIN_NAME:=Occurrence_dyn
976
# PLUGIN_HAS_MLI:=yes
977
# PLUGIN_NO_TEST:=yes
978
# PLUGIN_DIR:=src/occurrence_dyn
979
# PLUGIN_CMO:= register
980
# PLUGIN_GUI_CMO:=register_gui
981
# include Makefile.plugin
987
PLUGIN_ENABLE:=@ENABLE_METRICS@
989
PLUGIN_DISTRIBUTED:=yes
991
#PLUGIN_GUI_HAS_MLI:=yes
993
PLUGIN_DIR:=src/metrics
994
PLUGIN_CMO:= register
996
PLUGIN_GUI_CMO:=register_gui
997
include Makefile.plugin
999
#######################
1000
# Syntactic callgraph #
1001
#######################
1003
# Extension of the GUI for syntactic callgraph is compilable
1004
# only if viewgraph is available
1005
ifeq ($(HAS_VIEWGRAPH),yes)
1006
PLUGIN_GUI_CMO:=cg_viewer
1009
PLUGIN_ENABLE:=@ENABLE_SYNTACTIC_CALLGRAPH@
1010
PLUGIN_NAME:=Syntactic_callgraph
1011
PLUGIN_DISTRIBUTED:=yes
1013
PLUGIN_GUI_HAS_MLI:=yes
1014
PLUGIN_DIR:=src/syntactic_callgraph
1015
PLUGIN_CMO:= register
1017
include Makefile.plugin
1023
PLUGIN_ENABLE:=@ENABLE_VALUE@
1025
PLUGIN_DIR:=src/value
1026
PLUGIN_CMO:= state_set kf_state eval kinstr register
1027
PLUGIN_GUI_CMO:=register_gui
1029
PLUGIN_GUI_HAS_MLI:=yes
1031
PLUGIN_DISTRIBUTED:=yes
1032
include Makefile.plugin
1038
PLUGIN_ENABLE:=@ENABLE_FROM@
1040
PLUGIN_DIR:=src/from
1041
PLUGIN_CMO:= register
1042
PLUGIN_GUI_CMO:=register_gui
1044
PLUGIN_GUI_HAS_MLI:=yes
1045
PLUGIN_TESTS_DIRS:=idct test misc float
1046
PLUGIN_DISTRIBUTED:=yes
1047
include Makefile.plugin
1053
PLUGIN_ENABLE:=@ENABLE_USERS@
1055
PLUGIN_DIR:=src/users
1056
PLUGIN_CMO:= users_register
1059
PLUGIN_DISTRIBUTED:=yes
1060
include Makefile.plugin
1062
########################
1063
# Constant propagation #
1064
########################
1066
PLUGIN_ENABLE:=@ENABLE_CONSTANT_PROPAGATION@
1067
PLUGIN_NAME:=Constant_Propagation
1068
PLUGIN_DIR:=src/constant_propagation
1069
PLUGIN_CMO:= register
1071
PLUGIN_DISTRIBUTED:=yes
1072
include Makefile.plugin
1078
PLUGIN_ENABLE:=@ENABLE_POSTDOMINATORS@
1079
PLUGIN_NAME:=Postdominators
1080
PLUGIN_DIR:=src/postdominators
1081
PLUGIN_CMO:= print compute
1084
PLUGIN_DISTRIBUTED:=yes
1085
include Makefile.plugin
1091
PLUGIN_ENABLE:=@ENABLE_INOUT@
1093
PLUGIN_DIR:=src/inout
1094
PLUGIN_CMO:= kf_state context inputs outputs derefs access_path register
1097
PLUGIN_DISTRIBUTED:=yes
1098
include Makefile.plugin
1100
######################
1101
# Semantic callgraph #
1102
######################
1104
PLUGIN_ENABLE:=@ENABLE_SEMANTIC_CALLGRAPH@
1105
PLUGIN_NAME:=Semantic_callgraph
1106
PLUGIN_DIR:=src/semantic_callgraph
1107
PLUGIN_CMO:= register
1110
PLUGIN_DISTRIBUTED:=yes
1111
include Makefile.plugin
1117
PLUGIN_ENABLE:=@ENABLE_WP@
1120
PLUGIN_CMO:= macros wpBase wpFol translate \
1121
cil2cfg calculus lowlevel_model hoare_model \
1125
PLUGIN_GUI_CMO:=wp_gui
1126
PLUGIN_DISTRIBUTED:=no
1127
PLUGIN_DISTRIB_BIN:=no
1128
PLUGIN_NO_DEFAULT_TEST:=yes
1129
include Makefile.plugin
1131
#####################
1132
# Security analysis #
1133
#####################
1135
PLUGIN_ENABLE:=@ENABLE_SECURITY@
1136
PLUGIN_NAME:=Security
1137
PLUGIN_DIR:=src/security
1138
PLUGIN_CMO:= lattice model components analysis register
1139
PLUGIN_GUI_CMO:=register_gui
1141
PLUGIN_GUI_HAS_MLI:=yes
1142
PLUGIN_UNDOC:=analysis.ml
1143
# ocamldoc doesn't like recursive modules!
1144
PLUGIN_DISTRIBUTED:=yes
1145
include Makefile.plugin
1151
PLUGIN_ENABLE:=@ENABLE_IMPACT@
1153
PLUGIN_DIR:=src/impact
1154
PLUGIN_CMO:= register
1155
PLUGIN_GUI_CMO:= register_gui
1157
PLUGIN_GUI_HAS_MLI:=yes
1158
PLUGIN_DISTRIBUTED:=yes
1159
# PLUGIN_UNDOC:=impact_gui.ml
1160
include Makefile.plugin
1166
JESSIE_INCLUDES=@JESSIE_INCLUDES@
1168
PLUGIN_ENABLE:=@ENABLE_JESSIE@
1170
PLUGIN_DIR:=src/jessie
1171
PLUGIN_CMO:= integer common rewrite norm retype interp register
1173
PLUGIN_BFLAGS:=$(JESSIE_INCLUDES)
1174
PLUGIN_OFLAGS:=$(JESSIE_INCLUDES)
1175
PLUGIN_DEPFLAGS:=$(JESSIE_INCLUDES)
1176
PLUGIN_DOCFLAGS:=$(JESSIE_INCLUDES)
1177
PLUGIN_DISTRIBUTED:=yes
1178
PLUGIN_DISTRIB_BIN:=no
1179
PLUGIN_DISTRIB_EXTERNAL:=src-distrib-jessie
1180
include Makefile.plugin
1182
ifeq (@JESSIE_LOCAL@,yes)
1183
# Same variable JCCML_EXPORT as in Why Makefile
1184
JCCML_EXPORT = src/lib.ml src/rc.ml src/loc.ml src/pp.ml src/option_misc.ml \
1185
jc/jc_type_var.ml jc/output.ml \
1186
jc/jc_common_options.ml jc/jc_stdlib.ml \
1187
jc/jc_envset.ml jc/jc_region.ml jc/jc_fenv.ml jc/jc_constructors.ml \
1188
jc/jc_pervasives.ml jc/jc_iterators.ml \
1189
jc/jc_output_misc.ml jc/jc_poutput.ml jc/jc_output.ml jc/jc_noutput.ml
1190
JCCML_EXPORT := $(addprefix @WHYDISTRIB@/, $(JCCML_EXPORT))
1192
# Use the makefile of Why in order to compile Why's source files
1193
@JCCMO@ @JCCMX@: $(JCCML_EXPORT)
1194
$(MAKE) -j 1 FRAMAC=yes -C @WHYDISTRIB@ \
1195
$(patsubst @WHYDISTRIB@/%, %, $@)
1197
$(Jessie_CMI) $(Jessie_CMO): @JCCMO@
1198
$(Jessie_CMX): @JCCMX@
1200
# Call Why makefile from all, only if installed locally
1203
$(MAKE) -j 1 FRAMAC=yes -C @WHYDISTRIB@
1205
GEN_BYTE_LIBS+=@JCCMO@
1206
GEN_OPT_LIBS+=@JCCMX@
1207
else ifeq (@ENABLE_JESSIE@,yes)
1212
##################################
1213
# PDG : program dependence graph #
1214
##################################
1216
PLUGIN_ENABLE:=@ENABLE_PDG@
1220
PLUGIN_CMO:= print \
1222
lexical_successors \
1231
PDG_TYPES:=pdgIndex pdgTypes pdgMarks
1232
PDG_TYPES:=$(addprefix src/pdg_types/, $(PDG_TYPES))
1233
PLUGIN_TYPES_CMO:=$(PDG_TYPES)
1235
PLUGIN_INTRO:=doc/code/intro_pdg.txt
1236
PLUGIN_TYPES_TODOC:=$(addsuffix .mli, $(PDG_TYPES))
1238
PLUGIN_DISTRIBUTED:=yes
1239
include Makefile.plugin
1241
#####################################
1242
# Scope : (very experimental !) #
1243
#####################################
1245
PLUGIN_ENABLE:=@ENABLE_SCOPE@
1247
PLUGIN_DIR:=src/scope
1248
PLUGIN_CMO:= datascope zones
1250
PLUGIN_GUI_CMO:=dpds_gui
1251
PLUGIN_INTRO:=doc/code/intro_scope.txt
1252
PLUGIN_DISTRIBUTED:=yes
1253
include Makefile.plugin
1255
#####################################
1256
# Sparecode : unused code detection #
1257
#####################################
1259
PLUGIN_ENABLE:=@ENABLE_SPARECODE@
1260
PLUGIN_NAME:=Sparecode
1261
PLUGIN_DIR:=src/sparecode
1262
PLUGIN_CMO:= globs marks transform register
1265
PLUGIN_INTRO:=doc/code/intro_sparecode.txt
1266
PLUGIN_DISTRIBUTED:=yes
1267
include Makefile.plugin
1273
PLUGIN_ENABLE:=$(ENABLE_SLICING)
1274
PLUGIN_NAME:=Slicing
1275
PLUGIN_DIR:=src/slicing
1276
PLUGIN_CMO:= slicingMacros \
1285
SLICING_TYPES:=slicingTypes
1286
SLICING_TYPES:=$(addprefix src/slicing_types/, $(SLICING_TYPES))
1287
PLUGIN_TYPES_CMO:=$(SLICING_TYPES)
1289
PLUGIN_GUI_CMO:=register_gui
1291
PLUGIN_INTRO:=doc/code/intro_slicing.txt
1292
PLUGIN_TYPES_TODOC:= $(addsuffix .ml, $(SLICING_TYPES))
1293
PLUGIN_UNDOC:=register.ml # slicing_gui.ml
1295
PLUGIN_TESTS_DIRS:= slicing slicing2
1296
PLUGIN_TESTS_LIB:= tests/slicing/libSelect tests/slicing/libAnim
1298
PLUGIN_DISTRIBUTED:=yes
1299
include Makefile.plugin
1301
FILES_FOR_OCAMLDEP+=$(TEST_SLICING_ML)
1303
##########################
1304
# C++ analysis extension #
1305
##########################
1307
PPCHOME=@abs_top_srcdir@
1309
CXX_ELSADISTRIB=cxx_elsa/elsa-2006.06.11
1311
CXX_ELSAHOME=$(CXX_ELSADISTRIB)/elsa
1315
$(MAKE) -C $(CXX_ELSADISTRIB)
1317
### the ast generator.
1318
# Can not be part of the generic plugin mechanism, as we need it to
1319
# generate some of the sources of the plugin itself (i.e. it must be
1320
# built before the dependencies computation for the plugin takes place.
1323
CXX_ASTGENINT=std_utils loc astgen_type astgen_parse astgen_main
1324
CXX_ASTGENMOD=std_utils loc astgen_type astgen_parse astgen_lex astgen_main
1325
$(CXX_ASTGENMOD:%=cxx_elsa/%.cmo) $(CXX_OBJ:%=cxx_elsa/%.cmi): BFLAGS:=-I cxx_elsa $(BFLAGS)
1326
$(CXX_ASTGENMOD:%=cxx_elsa/%.cmx): OFLAGS:=-I cxx_elsa $(OFLAGS)
1328
# generator dependencies
1330
cxx_depend: cxx_elsa/.cxx_depend
1332
ifeq ($(ENABLE_CXX),yes)
1333
include cxx_elsa/.cxx_depend
1335
cxx_elsa/.cxx_depend: $(CXX_ASTGENMOD:%=cxx_elsa/%.ml) \
1336
$(CXX_ASTGENINT:%=cxx_elsa/%.mli)
1337
$(call QUIET,'$(N_DEP) $@') \
1338
$(OCAMLDEP) -pp $(CAMLP4O) -I cxx_elsa $^ > cxx_elsa/.cxx_depend
1341
bin/astgen$(EXE): $(CXX_ASTGENMOD:%=cxx_elsa/%.cmo)
1342
$(call QUIET,'$(N_LINKING) $@') \
1343
$(OCAMLC) -I cxx_elsa -o $@ -g str.cma $^
1345
### main modules of the elsa-to-cil translator
1346
CXX_TRANSLATE=std_utils install elsa_loc loc config astgen_lex \
1347
parse_tree predef_cxx cc_ast_parse cc_ast_visitor elsa_utils \
1348
cc_analyse_types mangling expr nameSpace types logic normalize cxx_print class \
1349
statements translate
1351
### c++ ast description from elsa
1352
CXX_ELSAAST=cc.ast cc_tcheck.ast cc_elaborate.ast gnu.ast annot_ast.ast
1354
# local c++ ast descriptions (needed because some AST nodes are in the
1355
# verbatim sections of elsa's *.ast)
1356
CXX_EXTRAAST=cxx_elsa/extra.ast
1359
# cxx_elsa/annot_ast.ml cxx_elsa/annot_ast_parse.ml
1361
### local configuration
1362
cxx_elsa/install.ml: Makefile
1363
@$(ECHO) "(* local installation related variables. " > $@
1364
@$(ECHO) "Automatically generated by Makefile. DO NOT EDIT! *)" >> $@
1365
@$(ECHO) "let framac_home = \"$(PPCHOME)\";;" >> $@
1367
"let elsa_home = Filename.concat framac_home \"$(CXX_ELSAHOME)\";;" >> $@
1369
### stand-alone translator
1371
cxx_elsa/test.cmo: $(CXX_TRANSLATE:%=cxx_elsa/%.cmo)
1372
cxx_elsa/test.cmo: BFLAGS:=-I cxx_elsa $(BFLAGS)
1373
bin/cxx_translate$(EXE):$(GEN_BYTE_LIBS) \
1374
$(CXX_TRANSLATE:%=cxx_elsa/%.cmo) cxx_elsa/test.cmo
1375
$(call QUIET,'$(N_LINKING) $@') \
1376
$(OCAMLC) $(BFLAGS) -I cxx_elsa $(BYTE_LIBS) \
1377
$(CXX_TRANSLATE:%=cxx_elsa/%.cmo) cxx_elsa/test.cmo -o $@
1379
CXX_TESTS_DIR=basic class val_analysis template specs
1381
#NB: PTESTS_OPTS is intended to be set outside of the Makefile
1382
#In particular make cxx_tests PTESTS_OPTS=-update will update the oracles.
1384
cxx_tests: bin/cxx_translate ptests
1386
../bin/ptests.byte$(EXE) $(PTESTS_OPTS) $(CXX_TESTS_DIR)
1388
ifeq ($(ENABLE_CXX),yes)
1393
GENERATED += src/cxx_types/cc_ast.mli
1395
DISTRIB_FILES += src/cxx_types/cc_ast.mli.in
1397
ifeq ($(ENABLE_CXX),yes)
1398
src/cxx_types/cc_ast.mli: Makefile \
1399
bin/astgen$(EXE) $(CXX_ELSAAST:%=$(CXX_ELSAHOME)/%) $(CXX_EXTRAAST)
1400
bin/astgen$(EXE) -prefix "cxx_elsa/cc_ast" \
1401
$(CXX_ELSAAST:%=$(CXX_ELSAHOME)/%) $(CXX_EXTRAAST)
1402
mv cxx_elsa/cc_ast.mli $@
1406
CC_AST_STUB=src/cxx_types/cc_ast.mli.in
1408
src/cxx_types/cc_ast.mli: Makefile $(CC_AST_STUB)
1409
$(call QUIET,'$(N_CP) $@') \
1410
$(CP) $(CC_AST_STUB) $@
1413
cxx_elsa/cc_ast_parse.ml: src/cxx_types/cc_ast.mli
1416
cxx_elsa/cc_ast_visitor.ml: src/cxx_types/cc_ast.mli
1419
cxx_elsa/annot_ast.ml cxx_elsa/annot_ast_parse.ml: \
1420
bin/astgen $(CXX_ELSAHOME)/annot.ast
1421
bin/astgen -prefix "cxx_elsa/annot_ast" \
1422
$(CXX_ELSAHOME)/annot.ast
1424
cxx_elsa/.depend: cxx_elsa/.cxx_depend bin/astgen$(EXE)
1426
PLUGIN_ENABLE:=$(ENABLE_CXX)
1428
PLUGIN_DIR:=cxx_elsa
1430
PLUGIN_NO_DEFAULT_TEST:=yes
1431
PLUGIN_BFLAGS:=-pp $(CAMLP4O)
1432
PLUGIN_OFLAGS:=-pp $(CAMLP4O)
1433
PLUGIN_DEPFLAGS:=-pp $(CAMLP4O)
1434
PLUGIN_DOCFLAGS:=-pp $(CAMLP4O)
1435
PLUGIN_CMO:= $(CXX_TRANSLATE) cxx_state register
1436
PLUGIN_GENERATED:= cxx_elsa/.cxx_depend bin/astgen \
1437
cxx_elsa/astgen_parse.ml cxx_elsa/astgen_parse.mli \
1438
cxx_elsa/astgen_lex.ml cxx_elsa/install.ml \
1439
cxx_elsa/cc_ast_visitor.ml cxx_elsa/cc_ast_parse.ml \
1440
src/cxx_types/cc_ast.mli
1443
PLUGIN_UNDOC:=astgen_lex.ml astgen_parse.ml cc_ast_parse.ml
1444
PLUGIN_TESTS_DIRS:=cxx_elsa/tests
1445
PLUGIN_INTRO:=cxx_elsa/doc_intro.txt
1446
PLUGIN_DISTRIBUTED:=no
1447
include Makefile.plugin
1449
ifeq ($(ENABLE_SLICING),yes)
1450
PLUGIN_ENABLE:=$(ENABLE_CXX)
1454
PLUGIN_NAME:=CxxSlicing
1455
PLUGIN_DIR:=cxx_elsa/cxx_slicing
1456
PLUGIN_CMO:= cxx_slice register_slicing
1458
PLUGIN_BFLAGS:= -I cxx_elsa
1459
PLUGIN_OFLAGS:= -I cxx_elsa
1460
PLUGIN_DEPFLAGS:= -I cxx_elsa
1462
PLUGIN_INTRO:=cxx_elsa/cxx_slicing/doc_intro.txt
1464
PLUGIN_DISTRIBUTED:=no
1465
include Makefile.plugin
1471
LCMO = src/logic/fol.cmo src/logic/logic_interp.cmo \
1472
src/logic/infer_annotations.cmo
1473
LCMX = $(LCMO:.cmo=.cmx)
1475
MODULES_TODOC += src/logic/fol.mli src/logic/logic_interp.mli \
1476
src/logic/infer_annotations.mli
1478
PLUGIN_TESTS_LIST += spec
1480
#######################
1481
# Aorai : ltl_to_acsl #
1482
#######################
1484
PLUGIN_ENABLE:=@ENABLE_LTL_TO_ACSL@
1485
PLUGIN_NAME:=Ltl_to_acsl
1486
PLUGIN_DIR:=src/ltl_to_acsl
1487
PLUGIN_GENERATED:= $(addprefix ${PLUGIN_DIR}/, \
1488
promelalexer.ml promelaparser.ml promelaparser.mli \
1489
ltllexer.ml ltlparser.ml ltlparser.mli \
1491
PLUGIN_CMO:= bool3 \
1502
ltl_to_acsl_visitors \
1503
ltl_to_acsl_register
1504
PLUGIN_CMI:= ltlast.mli \
1508
PLUGIN_DISTRIBUTED:=yes
1509
PLUGIN_DISTRIB_BIN:=no
1510
include Makefile.plugin
1512
##########################################################################
1513
# Common startup module #
1514
# All link command should add it as last linked module and depend on it. #
1515
##########################################################################
1517
STARTUPCMO=src/kernel/boot.cmo
1518
STARTUPCMX=$(STARTUPCMO:.cmo=.cmx)
1524
TOPCMO = src/toplevel/main.cmo
1525
TOPCMX = $(TOPCMO:.cmo=.cmx)
1527
ALL_CMO=$(ACMO) $(PLUGIN_TYPES_CMO_LIST) \
1528
$(KERNEL_CMO) $(LCMO) $(LOCCMO) \
1529
$(PLUGIN_CMO_LIST) $(TOPCMO)
1531
bin/toplevel.byte$(EXE): $(ALL_CMO) $(STARTUPCMO) $(GEN_BYTE_LIBS) \
1532
$(PLUGIN_DYN_CMO_LIST)
1533
$(call QUIET,'$(N_LINKING) $@') \
1534
$(OCAMLC) $(BFLAGS) -o $@ $(BYTE_LIBS) $(ALL_CMO) $(STARTUPCMO)
1536
bin/toplevel.prof$(EXE): $(GEN_BYTE_LIBS) $(ALL_CMO) $(STARTUPCMO) \
1537
$(PLUGIN_DYN_CMO_LIST)
1538
ocamlcp $(BFLAGS) -o $@ $(BYTE_LIBS) $(ALL_CMO) $(STARTUPCMO)
1540
ALL_CMX= $(ALL_CMO:.cmo=.cmx)
1542
bin/toplevel.opt$(EXE): $(ALL_CMX) $(STARTUPCMX) $(GEN_OPT_LIBS) \
1543
$(PLUGIN_DYN_CMX_LIST)
1544
$(call QUIET,'$(N_LINKING) $@') \
1545
$(OCAMLOPT) $(OFLAGS) -o $@ $(OPT_LIBS) $(ALL_CMX) $(STARTUPCMX)
1547
bin/toplevel.top$(EXE): $(ALL_CMO) src/toplevel/toplevel_topdirs.cmo \
1548
$(STARTUPCMO) $(GEN_BYTE_LIBS) $(PLUGIN_DYN_CMO_LIST)
1549
$(call QUIET,'$(N_MKTOP) $@') \
1550
$(OCAMLMKTOP) $(BFLAGS) -o $@ $(BYTE_LIBS) $(ALL_CMO) \
1551
src/toplevel/toplevel_topdirs.cmo $(STARTUPCMO)
1557
ifneq (@ENABLE_GUI@,no)
1558
GUI_INCLUDES = -I src/gui -I +lablgtk2
1559
BYTE_GUI_LIBS+= lablgtk.cma
1560
OPT_GUI_LIBS += lablgtk.cmxa
1562
ifeq ($(HAS_VIEWGRAPH),yes)
1563
BYTE_GUI_LIBS += lablgnomecanvas.cma
1564
OPT_GUI_LIBS += lablgnomecanvas.cmxa
1567
ifeq ($(HAS_LABLGTK),yes)
1568
EXTRAS_AFTER_BYTE+= gui
1571
ifeq ($(HAS_GTKSOURCEVIEW),yes)
1572
ifeq ($(HAS_LEGACY_GTKSOURCEVIEW),yes)
1573
GUI_INCLUDES += -I +lablgtksourceview
1575
BYTE_GUI_LIBS += lablgtksourceview.cma
1576
OPT_GUI_LIBS += lablgtksourceview.cmxa
1579
src/gui/filetree.ml: Makefile
1581
ifeq ($(HAS_LABLGTK_CUSTOM_MODEL),yes)
1582
src/gui/filetree.ml: src/gui/filetree_custom.ml
1583
$(call QUIET,'$(N_CP) $@') \
1587
src/gui/filetree.ml: src/gui/filetree_default.ml
1588
$(call QUIET,'$(N_CP) $@') \
1592
GENERATED += src/gui/filetree.ml
1594
GUICMO += gtk_helper source_viewer source_manager warning_manager \
1595
pretty_source filetree design project_manager journal_manager \
1596
about_dialog gui_boot
1597
GUICMO:= $(patsubst %, src/gui/%.cmo, $(GUICMO)) $(PLUGIN_GUI_CMO_LIST)
1599
MODULES_TODOC+= $(addprefix src/gui/,$(addsuffix .mli,\
1600
gtk_helper source_viewer source_manager warning_manager \
1601
pretty_source filetree design project_manager journal_manager))
1603
GUICMI = $(GUICMO:.cmo=.cmi)
1604
GUICMX = $(GUICMO:.cmo=.cmx)
1606
$(GUICMI) $(GUICMO) bin/viewer.byte$(EXE): BFLAGS+= $(GUI_INCLUDES)
1607
$(GUICMX) bin/viewer.opt$(EXE): OFLAGS+= $(GUI_INCLUDES)
1609
$(PLUGIN_DEP_GUI_CMO_LIST) $(PLUGIN_DYN_DEP_GUI_CMO_LIST): BFLAGS+= $(GUI_INCLUDES)
1610
$(PLUGIN_DEP_GUI_CMX_LIST) $(PLUGIN_DYN_DEP_GUI_CMX_LIST): OFLAGS+= $(GUI_INCLUDES)
1614
gui: bin/viewer.byte$(EXE) bin/viewer.$(OCAMLBEST)$(EXE)
1616
bin/viewer.byte$(EXE): BYTE_LIBS+=$(BYTE_GUI_LIBS)
1617
bin/viewer.byte$(EXE): $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO) $(STARTUPCMO) \
1618
$(GEN_BYTE_LIBS) $(PLUGIN_DYN_GUI_CMO_LIST)
1619
$(call QUIET,'$(N_LINKING) $@') \
1620
$(OCAMLC) $(BFLAGS) -o $@ $(BYTE_LIBS) $(ALL_CMO) $(GRAPH_GUICMO) \
1621
$(GUICMO) $(STARTUPCMO)
1623
bin/viewer.opt$(EXE): OPT_LIBS+= $(OPT_GUI_LIBS)
1624
bin/viewer.opt$(EXE): $(ALL_CMX) $(GRAPH_GUICMX) $(GUICMX) $(STARTUPCMX) \
1625
$(GEN_OPT_LIBS) $(PLUGIN_DYN_GUI_CMX_LIST)
1626
$(call QUIET,'$(N_LINKING) $@') \
1627
$(OCAMLOPT) $(OFLAGS) -o $@ $(OPT_LIBS) $(ALL_CMX) $(GRAPH_GUICMX) \
1628
$(GUICMX) $(STARTUPCMX)
1635
JOURNALS = $(patsubst %.ml, %, $(wildcard frama_c_journal*.ml))
1636
JOURNALS_CMO = $(addsuffix .cmo, $(JOURNALS))
1638
ifeq ($(LOWER_THAN_311), no)
1639
JOURNALS_CMXS = $(JOURNALS_CMO:.cmo=.cmxs)
1640
journal: $(JOURNALS_CMO) $(JOURNALS_CMXS)
1642
journal: $(JOURNALS_CMO)
1645
$(JOURNALS_CMO) $(JOURNALS_CMXS): FLAGS+=-w x
1647
#########################
1648
# Standalone Obfuscator #
1649
#########################
1651
obfuscator: bin/obfuscator.$(OCAMLBEST)
1653
bin/obfuscator.byte$(EXE): $(ACMO) $(KERNEL_CMO) $(STARTUPCMO) $(GEN_BYTE_LIBS)
1654
$(call QUIET,'$(N_LINKING) $@') \
1655
$(OCAMLC) $(BFLAGS) -o $@ $(BYTE_LIBS) $^
1657
bin/obfuscator.opt$(EXE): $(ACMX) $(KERNEL_CMX) $(STARTUPCMX) $(GEN_OPT_LIBS)
1658
$(call QUIET,'$(N_LINKING) $@') \
1659
$(OCAMLOPT) $(OFLAGS) -o $@ $(OPT_LIBS) $^
1665
# the following line should be removed when/if miel becomes a plugin
1666
CONFIG_DISTRIB_BIN+="--disable-miel"
1668
ifneq ($(ENABLE_MIEL), no)
1669
MIELCMO = src/miel/miel_spec_parsing_internals.cmo \
1670
src/miel/miel_user.cmo \
1671
src/miel/miel_spec.cmo \
1672
src/miel/miel_spec_compilation_lexer.cmo \
1673
src/miel/miel_spec_compilation_parser.cmo \
1674
src/miel/miel_spec_pointers_lexer.cmo \
1675
src/miel/miel_spec_pointers_parser.cmo \
1676
src/miel/miel_spec_lexer.cmo src/miel/miel_spec_parser.cmo \
1677
src/miel/parallelism.cmo src/miel/proc_names.cmo \
1678
src/miel/build_parallel_model.cmo \
1679
src/miel/alcool.cmo src/miel/miel_ext_pointers.cmo \
1680
src/miel/miel_ext_raw.cmo src/miel/promela.cmo \
1681
src/miel/miel_init.cmo \
1682
src/miel/passerelle.cmo \
1683
src/miel/miel_cg.cmo \
1686
MIELCMX = $(MIELCMO:.cmo=.cmx)
1688
ALL_MIEL_CMO= $(ACMO) $(PLUGIN_TYPES_CMO_LIST) $(KERNEL_CMO) $(KCMO) $(LCMO) $(LOCCMO) $(PLUGIN_CMO_LIST) $(TOPCMO) $(MIELCMO)
1690
ALL_MIEL_CMX = $(ACMX) $(PLUGIN_TYPES_CMX_LIST) $(KERNEL_CMX) $(KCMX) $(LCMX) $(LOCCMX) $(PLUGIN_CMX_LIST) $(TOPCMX) $(MIELCMX)
1692
# The references to MIELO have been removed so far. They will be restored as
1693
# soon as they are needed.
1694
MIELO = src/miel/ocaml_tcl.o
1696
GENERATED += src/miel/miel_spec_lexer.ml src/miel/miel_spec_parser.ml \
1697
src/miel/miel_spec_compilation_lexer.ml \
1698
src/miel/miel_spec_compilation_parser.ml \
1699
src/miel/miel_spec_pointers_lexer.ml \
1700
src/miel/miel_spec_pointers_parser.ml \
1701
src/miel/miel_spec_parser.mli \
1702
src/miel/miel_spec_pointers_parser.mli \
1703
src/miel/miel_spec_compilation_parser.mli
1705
miel: bin/miel.opt$(EXE)
1707
bin/miel.top$(EXE): $(ALL_MIEL_CMO) src/toplevel/toplevel_topdirs.cmo \
1708
src/miel/mieltop_dirs.cmo $(TOPCMO) $(STARTUPCMO) \
1710
$(call QUIET,'$(N_MKTOP) $@') \
1711
$(OCAMLMKTOP) $(BFLAGS) -o $@ $(BYTE_LIBS) \
1712
$(ALL_MIEL_CMO) $(TOPCMO) \
1713
src/toplevel/toplevel_topdirs.cmo src/miel/mieltop_dirs.cmo \
1716
bin/miel.byte$(EXE): $(ALL_MIEL_CMO) $(STARTUPCMO) $(GEN_BYTE_LIBS)
1717
$(call QUIET,'$(N_LINKING) $@') \
1718
$(OCAMLC) $(BFLAGS) -o $@ $(BYTE_LIBS) $(ALL_MIEL_CMO) $(STARTUPCMO)
1720
bin/miel.opt$(EXE): $(ALL_MIEL_CMX) $(STARTUPCMX) $(GEN_OPT_LIBS)
1721
$(call QUIET,'$(N_LINKING) $@') \
1722
$(OCAMLOPT) $(OFLAGS) -o $@ $(OPT_LIBS) $(ALL_MIEL_CMX) $(STARTUPCMX)
1724
miel_tests: bin/miel.byte$(EXE)
1725
$(MAKE) -C src/miel/tests
1727
ifeq ($(HAS_LABLGTK),yes)
1729
GENERATED += src/miel/miel_gui.ml
1730
src/miel/miel_gui.ml : src/miel/gui/miel_gui.glade
1731
$(call QUIET,'$(N_MAKING) $@') \
1732
($(CP) src/miel/gui/miel_gui.glade bin/; \
1733
$(LABLGLADECC) $^ > $@)
1735
bin/miel_gui.glade : src/miel/gui/miel_gui.glade
1736
$(call QUIET,'$(N_CP) $@') \
1739
MIEL_GUI_CMO = src/miel/miel_gui.cmo src/miel/miel_gui_actions.cmo
1740
MIEL_GUI_CMX = $(MIEL_GUI_CMO:.cmo=.cmx)
1741
$(MIEL_GUI_CMO) $(MIEL_GUI_CMX) : INCLUDES+=$(GUI_INCLUDES)
1743
#bin/miel_gui.opt : $(OPT_LIBS)+=lablglade.cmxa lablgtk.cmxa
1744
bin/miel_gui.opt$(EXE) : $(ALL_MIEL_CMX) $(MIEL_GUI_CMX) $(STARTUPCMX) \
1746
$(call QUIET,'$(N_LINKING) $@') \
1747
$(OCAMLOPT) $(OFLAGS) -o $@ $(OPT_LIBS) \
1748
-I +lablgtk2 lablgtk.cmxa lablglade.cmxa \
1749
$(ALL_MIEL_CMX) $(MIEL_GUI_CMX) $(STARTUPCMX)
1751
miel_gui: bin/miel_gui.glade bin/miel_gui.opt$(EXE)
1757
-$(ECHO) "Unsupported extension. Rerun ./configure --enable-miel"
1760
VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
1762
VERSIONDIR=src/kernel
1763
VERSIONFILE=$(VERSIONDIR)/version.ml
1764
VERSIONCMO=$(VERSIONDIR)/version.cmo
1765
GENERATED +=$(VERSIONFILE)
1768
space:=$(empty) $(empty)
1769
$(VERSIONFILE): VERSION Makefile
1770
$(call QUIET,'$(N_MAKING) $@') \
1772
$(ECHO) "(* This file is generated in Makefile.in. Do not modify. *)" \
1774
$(ECHO) "let version = \""$(VERSION)"\"" >> $@; \
1775
$(ECHO) "let date = \""`LC_ALL=C date`"\"" >> $@; \
1776
$(ECHO) "let dataroot = try Sys.getenv \"FRAMAC_SHARE\" with Not_found -> \"$(DESTDIR)$(datadir)\"" >> $@;\
1777
$(ECHO) "let static_plugins = [" \
1778
$(subst $(space),"; ",$(foreach p,$(PLUGIN_LIST),\"$(notdir $p)\")) \
1780
$(ECHO) "let static_gui_plugins = [" \
1781
$(subst $(space),"; ",$(foreach p,$(PLUGIN_GUI_CMO_LIST),\"$(notdir $(patsubst %.cmo,%,$p))\")) \
1791
$(call QUIET,'$(N_DOT) $@') \
1792
$(DOT) -Tpng -o $@ $<
1795
$(call QUIET,'$(N_DOT) $@') \
1796
($(SED) "s/\(digraph .*\)/\1 node [href=\"\\\\N.html\"];/" $< \
1798
$(DOT) -Tsvg -o $@ $<.tmp; \
1802
$(call QUIET,'$(N_DOT) $@') \
1803
$(DOT) -Tps -o $@ $<
1806
@$(ECHO) "dot missing: generation of $@ skipped."
1808
@$(ECHO) "dot missing: generation of $@ skipped."
1810
@$(ECHO) "dot missing: generation of $@ skipped."
1813
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html .cmxs
1816
$(call QUIET,'$(N_OCAMLC) $@') \
1817
$(OCAMLC) -c $(BFLAGS) $<
1820
$(call QUIET,'$(N_OCAMLC) $@') \
1821
if `test -e $<i`; then $(OCAMLC) -c $(BFLAGS) $<i; \
1822
else $(OCAMLC) -c $(BFLAGS) $<; fi
1825
$(call QUIET,'$(N_OCAMLC) $@') \
1826
$(OCAMLC) -c $(BFLAGS) $<
1829
$(call QUIET,'$(N_OCAMLOPT) $@') \
1830
$(OCAMLOPT) -c $(OFLAGS) $<
1833
$(call QUIET,'$(N_OCAMLOPT) $@') \
1834
$(OCAMLOPT) -c $(OFLAGS) $<
1837
$(call QUIET,'$(N_OCAMLOPT) $@') \
1838
$(OCAMLOPT) -shared -o $@ $(OFLAGS) $<
1841
$(call QUIET,'$(N_OCAMLLEX) $@') \
1845
$(call QUIET,'$(N_OCAMLYACC) $@') \
1849
$(call QUIET,'$(N_OCAMLYACC) $@') \
1853
$(call QUIET,'$(N_LATEX) $@') \
1854
latex $< && latex $<
1857
$(call QUIET,'$(N_DVIPS) $@') \
1864
$(call QUIET,'$(N_OCAMLC) $@') \
1865
$(OCAMLC) $(BFLAGS) -ccopt "-o $@" $<
1871
.PHONY: tests oracles btests tests_dist
1872
tests: byte opt top ptests
1873
$(call QUIET,'$(N_EXEC) ptests') \
1874
time -p ./bin/ptests.byte$(EXE) $(PLUGIN_TESTS_LIST)
1876
oracles: opt top ptests
1877
$(call QUIET, '$(N_MAKING) oracles') \
1878
(./bin/ptests.byte$(EXE) $(PLUGIN_TESTS_LIST) > /dev/null 2>&1 ; \
1879
./bin/ptests.byte$(EXE) -update $(PLUGIN_TESTS_LIST))
1881
btests: byte top ptests
1882
$(call QUIET,'$(N_EXEC) ptest') \
1883
time -p ./bin/ptests.byte$(EXE) -byte $(PLUGIN_TESTS_LIST)
1885
tests_dist: dist top ptests
1886
$(call QUIET,'$(N_EXEC) ptests') \
1887
time -p ./bin/ptests.byte$(EXE) $(PLUGIN_TESTS_LIST)
1889
# test only one test suite : make suite_tests
1890
%_tests: opt top ptests
1891
$(call QUIET,'$(N_EXEC) ptests') \
1892
./bin/ptests.byte$(EXE) $($*_TESTS_OPTS) $*
1896
fulltests: tests wp_tests
1899
find doc/speclang -name \*.c -exec bin/toplevel.byte$(EXE) {} \; > /dev/null
1909
# otags gives a better tagging of ocaml files than etags
1912
$(OTAGS) -r external src lib cil
1914
$(OTAGS) -vi -r external src lib cil
1917
find . -name "*.ml[ily]" -o -name "*.ml" | sort -r | xargs \
1918
etags "--regex=/[ \t]*let[ \t]+\([^ \t]+\)/\1/" \
1919
"--regex=/[ \t]*let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
1920
"--regex=/[ \t]*and[ \t]+\([^ \t]+\)/\1/" \
1921
"--regex=/[ \t]*type[ \t]+\([^ \t]+\)/\1/" \
1922
"--regex=/[ \t]*exception[ \t]+\([^ \t]+\)/\1/" \
1923
"--regex=/[ \t]*val[ \t]+\([^ \t]+\)/\1/" \
1924
"--regex=/[ \t]*module[ \t]+\([^ \t]+\)/\1/"
1932
ocamlwc -p src/*/*.ml src/*/*.ml[iyl] cil/ocamlutil/*.ml cil/ocamlutil/*.ml[ily] cil/src/*.ml cil/src/*.ml[ily] cil/src/*.ml cil/src/*.ml[ily] cil/src/logic/*.ml cil/src/logic/*.ml[ily] cil/src/ext/*.ml cil/src/ext/*.ml[ily] cil/src/frontc/*.ml cil/src/frontc/*.ml[ily]
1934
$(DOC_DIR)/plugin.css: $(DOC_DIR)/style.css
1935
$(call QUIET,'$(N_MAKING) $@') \
1937
($(CAT) $<; $(ECHO) "body { background-color : #FFFFEE }") > $@; \
1940
$(DOC_DIR)/docgen.cmo: $(DOC_DIR)/docgen.ml
1941
$(call QUIET,'$(N_OCAMLC) $@') \
1942
$(OCAMLC) -c -I +ocamldoc -I $(VERSIONDIR) $(DOC_DIR)/docgen.ml
1944
$(RM) $(DOC_DIR)/docgen.cm[io]
1946
.PHONY: doc html plugins-doc
1948
plugins-doc: $(PLUGIN_DOC_LIST)
1950
# to make the documentation for one pluggin only,
1951
# the name of the pluggin should begin with a capital letter :
1952
# Example for the pdg doc : make Pdg_DOC
1953
# While working on the documentation of a pluggin, it can also be usefull
1954
# to use : make -o doc/code/kernel-doc.ocamldoc Plugin_DOC
1955
# to avoid redoing the global documentation each time.
1957
DOC_FLAGS:= -colorize-code -stars -inv-merge-ml-mli -m A -hide-warnings \
1958
$(INCLUDES) $(GUI_INCLUDES)
1960
STDLIB_FILES=map set pervasives big_int list array string char marshal \
1961
printf format scanf hashtbl buffer sys
1962
STDLIB_FILES:=$(patsubst %, $(OCAMLLIB)/%.mli, $(STDLIB_FILES))
1964
html $(DOC_DIR)/kernel-doc.ocamldoc: $(MODULES_TODOC) \
1965
byte bin/viewer.byte \
1966
$(DOC_DIR)/docgen.cmo
1967
$(call QUIET,'$(N_DOC) kernel') \
1968
($(MKDIR) $(DOC_DIR)/html; \
1969
$(RM) $(DOC_DIR)/html/*.html; \
1970
$(OCAMLDOC) $(DOC_FLAGS) -I $(OCAMLLIB) \
1971
$(addprefix -stdlib , $(STDLIB_FILES)) \
1972
-sort -css-style ../style.css \
1973
-g $(DOC_DIR)/docgen.cmo \
1974
-d $(DOC_DIR)/html -dump $(DOC_DIR)/kernel-doc.ocamldoc \
1977
doc: html plugins-doc
1979
doc/db/db.tex: src/kernel/db.mli
1980
$(call QUIET,'$(N_DOC) $@') \
1981
($(MKDIR) $(dir $@); \
1982
$(OCAMLDOC) $(INCLUDES) -I $(OCAMLLIB) \
1983
-latex -noindex -latextitle 3,paragraph -notoc -noheader -notrailer \
1986
# Could be optimized
1988
db_doc doc/db/db.pdf: doc/db/main.tex doc/db/main.bib doc/db/db.tex
1989
$(call QUIET,'$(N_MAKING) doc/db/db.pdf') \
1991
pdflatex $(notdir $<); bibtex main; \
1992
pdflatex $(notdir $<); pdflatex $(notdir $<); \
1993
mv main.pdf $(notdir $@)
1995
#find src -name "*.ml[i]" -o -name "*.ml" -maxdepth 3 | sort -r | xargs
1997
$(call QUIET,'$(N_DOC) callgraph') \
1998
$(OCAMLDOC) $(INCLUDES) -o doc/call_graph.dot -dot -dot-include-all -dot-reduce $(MODULES_TODOC)
1999
$(MAKE) doc/call_graph.svg
2000
$(MAKE) doc/call_graph.ps
2002
datatype_dependencies.dot computation_dependencies.dot: ./bin/toplevel.byte$(EXE)
2003
$(call QUIET,'$(N_EXEC) toplevel.byte') \
2004
./bin/toplevel.byte$(EXE) -project-debug -dump > /dev/null 2> /dev/null
2006
.PHONY:display_dependencies
2007
display_dependencies: datatype_dependencies.svg computation_dependencies.svg
2008
inkscape datatype_dependencies.svg computation_dependencies.svg &
2014
FILTER_INTERFACE_DIRS=lib/plugins src/gui
2018
# $(MAKE) -C ocamlgraph install
2019
$(MKDIR) $(DESTDIR)$(BINDIR)
2020
$(MKDIR) $(DESTDIR)$(datadir)
2021
$(MKDIR) $(DESTDIR)$(plugindir)
2022
$(MKDIR) $(DESTDIR)$(libdir)
2023
$(CP) -R share/*.c share/*.h share/Makefile.template share/why share/jessie \
2024
$(DESTDIR)$(datadir)
2025
$(CP) bin/toplevel.$(OCAMLBEST) $(DESTDIR)$(BINDIR)/frama-c$(EXE)
2026
$(CP) bin/toplevel.byte$(EXE) $(DESTDIR)$(BINDIR)/frama-c.byte$(EXE)
2027
if [ -x bin/toplevel.top ] ; then \
2028
$(CP) bin/toplevel.top $(DESTDIR)$(BINDIR)/frama-c.toplevel$(EXE) ; fi
2029
if [ -x bin/viewer.$(OCAMLBEST) ] ; then \
2030
$(CP) bin/viewer.$(OCAMLBEST) $(DESTDIR)$(BINDIR)/frama-c-gui$(EXE) ; fi
2031
if [ -x bin/viewer.byte$(EXE) ] ; then \
2032
$(CP) bin/viewer.byte$(EXE) $(DESTDIR)$(BINDIR)/frama-c-gui.byte$(EXE) ; fi
2033
if [ -d doc/manuals ]; then \
2034
$(CP) -R doc/manuals $(DESTDIR)$(datadir); \
2036
if [ -d lib/plugins -a $(PLUGIN_DYN_EXISTS) = "yes" ]; then \
2037
$(CP) $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
2038
$(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
2039
$(DESTDIR)$(plugindir); \
2041
# line below does not work if INCLUDES contains twice the same directory
2042
# Do not attempt to copy gui interfaces if gui is disabled
2043
$(CP) $(foreach d,$(filter-out $(FILTER_INTERFACE_DIRS),$(INCLUDES:-I%=%)), $(d)/*.cmi) $(DESTDIR)$(libdir)
2044
if [ "$(ENABLE_GUI)" = "yes" ]; then \
2045
$(CP) src/gui/*.cmi $(DESTDIR)$(libdir); \
2047
# remove CVS directories
2048
find $(DESTDIR)$(datadir) -name CVS | xargs $(RM) -r
2049
ifeq (@JESSIE_LOCAL@,yes)
2050
$(MAKE) -C @WHYDISTRIB@ DESTDIR=$(DESTDIR) install
2056
################################
2057
# File headers: license policy #
2058
################################
2060
HEADACHE= headache -c headers/headache_config.txt
2062
MODIFIED_MENHIR=external/ptmap.ml*
2064
CIL = cil/ocamlutil/*.ml* \
2066
cil/src/ext/*.ml* cil/src/ext/pta/*.ml* \
2067
cil/src/frontc/*.ml*
2069
CEA_INRIA_LGPL = Makefile.in configure.in config.h.in \
2071
cil/src/logic/*.ml* \
2072
src/pdg_types/*.ml* src/pdg/*.ml* \
2073
src/slicing_types/*.ml* src/slicing/*.ml* \
2075
src/sparecode/*.ml* \
2078
INRIA_LGPL= src/jessie/*.ml* \
2079
src/ltl_to_acsl/*.ml* \
2082
CEA_LGPL= Makefile.plugin \
2084
src/buckx/*.ml* src/buckx/*.[cS] \
2085
src/constant_propagation/*.ml* \
2086
src/cxx_types/cc_ast.mli.in \
2090
src/journal_loader/*.ml* \
2093
src/memory_state/*.ml* \
2096
src/occurrence/*.ml* \
2097
src/postdominators/*.ml* \
2099
src/semantic_callgraph/*.ml* \
2100
src/syntactic_callgraph/*.ml* \
2101
src/toplevel/*.ml* \
2104
share/*.c share/*.h \
2105
share/Makefile.template \
2108
CEA_PROPRIETARY:= src/modular_dependencies/*.ml* \
2110
src/security/*.ml* \
2112
share/miel-mode.el \
2113
src/cxx_types/predef_cxx_types.mli
2115
ifneq ($(ENABLE_CXX),no)
2119
cxx_elsa/cxx_slicing/*.ml*
2121
ifeq ($(ENABLE_MIEL),yes)
2122
CEA_PROPRIETARY+=src/miel/*.ml*
2125
LICENSES= MODIFIED_MENHIR CEA_LGPL CEA_PROPRIETARY CEA_INRIA_LGPL INRIA_LGPL \
2126
CIL MODIFIED_CAMLLIB
2130
@echo "Applying Headers..."
2131
$(foreach l,$(LICENSES),\
2132
$(foreach f,$($l),$(shell $(HEADACHE) -h headers/$l $f)))
2134
########################################################################
2135
# Makefile is rebuilt whenever Makefile.in or configure.in is modified #
2136
########################################################################
2138
Makefile: Makefile.plugin Makefile.in config.status
2141
config.status: configure
2142
./config.status --recheck
2144
configure: configure.in
2147
$(PERFCOUNT).c: $(PERFCOUNT).c.in
2151
# If 'make clean' have to be performed after 'cvs update':
2152
# change '.make-clean-stamp' before 'cvs commit'
2153
.make-clean: .make-clean-stamp
2159
# force "make clean" to be executed for all users of CVS
2161
expr `$(CAT) .make-clean-stamp` + 1 > .make-clean-stamp
2168
$(call QUIET,'$(N_RM) journal') \
2169
$(RM) frama_c_journal*
2172
$(call QUIET,'$(N_RM) tests') \
2173
($(RM) tests/*/*.byte$(EXE) tests/*/*.opt$(EXE) tests/*/*.cm* \
2174
tests/dynamic/.cm* tests/*/*~ tests/*/#* ; \
2175
$(RM) tests/*/result/*.*)
2177
clean-doc: $(PLUGIN_LIST:=_CLEAN_DOC)
2178
$(call QUIET,'$(N_RM) documentation') \
2179
($(RM) -r $(DOC_DIR)/html; \
2180
$(RM) $(DOC_DIR)/docgen.cm* $(DOC_DIR)/*~; \
2181
$(RM) doc/db/*~ doc/db/ocamldoc.sty doc/db/db.tex; \
2182
if [ -f doc/developer/Makefile ]; then \
2183
$(MAKE) --silent -C doc/developer clean; \
2185
if [ -f doc/architecture/Makefile ]; then \
2186
$(MAKE) --silent -C doc/architecture clean; \
2188
if [ -f doc/speclang/Makefile ]; then \
2189
$(MAKE) --silent -C doc/speclang clean; \
2191
if [ -f doc/www/src/Makefile ]; then \
2192
$(MAKE) --silent -C doc/www/src clean; \
2196
$(call QUIET,'$(N_RM) gui') \
2197
$(RM) src/*/*_gui.cm* src/*/*_gui.o src/gui/*.cm* src/gui/*.o
2200
$(call QUIET,'$(N_RM) why') \
2201
if [ -f why/Makefile ]; then \
2202
$(MAKE) --silent -C why clean; \
2205
clean:: $(PLUGIN_LIST:=_CLEAN) $(PLUGIN_DYN_LIST:=_CLEAN) \
2206
clean-tests clean-journal
2207
$(call QUIET,'$(N_RM) plugins') \
2208
($(RM) $(PLUGIN_GENERATED_LIST); \
2209
$(RM) $(PLUGIN_LIB_DIR)/*.mli $(PLUGIN_LIB_DIR)/*.cm* \
2210
$(PLUGIN_LIB_DIR)/*.p)
2211
$(call QUIET,'$(N_RM) sources') \
2212
for d in . $(SRC_DIRS); do \
2213
$(RM) $$d/*.cm* $$d/*.o $$d/*.a $$d/*.annot $$d/*~ $$d/*.output \
2214
$$d/*.annot $$d/\#*; \
2216
$(call QUIET,'$(N_RM) generated files') \
2218
$(call QUIET,'$(N_RM) binaries') \
2219
$(RM) bin/*.byte$(EXE) bin/*.opt$(EXE) bin/*.top$(EXE)
2221
distclean-ocamlgraph:
2222
$(call QUIET,'$(N_RM) ocamlgraph') \
2223
if [ -f ocamlgraph/Makefile ]; then \
2224
$(MAKE) --silent -C ocamlgraph distclean; \
2228
$(call QUIET,'$(N_RM) why') \
2229
if [ -f why/Makefile ]; then \
2230
$(MAKE) --silent -C why dist-clean; \
2233
dist-clean distclean:: clean clean-doc \
2234
distclean-why distclean-ocamlgraph
2235
$(call QUIET,'$(N_RM) distribution') \
2236
$(RM) Makefile config.cache config.log config.status config.h
2242
PLUGIN_DEP_LIST:=$(PLUGIN_LIST) $(PLUGIN_DYN_LIST)
2245
.depend: $(PLUGIN_DEP_LIST:%=%_DEP)
2246
depend: $(PLUGIN_DEP_LIST:%=%_DEP_REDO)
2248
.depend depend: $(GENERATED) $(PLUGIN_GENERATED_LIST)
2249
$(call QUIET,'$(N_DEP) why/.depend') \
2250
(if [ -f why/Makefile ]; then \
2251
$(MAKE) --silent -C why .depend; \
2253
$(call QUIET,'$(N_DEP) depend') \
2255
if test "$(PLUGIN_DEP_LIST)" != ""; then \
2256
$(CAT) $(foreach d, $(PLUGIN_DEP_LIST), $(dir $d).depend) > .depend; \
2258
$(OCAMLDEP) $(DEP_FLAGS) $(FILES_FOR_OCAMLDEP) >> .depend; \
2259
$(SED) -i -e "s&why/[/A-Za-z_0-9]\+.cm[oxi]&&g" .depend; \
2260
$(SED) -i -e "s&$(OCAMLGRAPH_LOCAL)/view_graph/\([/A-Za-z_0-9]\+.cm[oxi]\)&lib/\1&g" .depend; \
2261
$(CHMOD_RO) .depend)
2265
#####################
2266
# ptest development #
2267
#####################
2271
# Because Ocaml on MacOS X has issues with native threads
2272
ptests: bin/ptests.byte$(EXE)
2274
PTESTS_SRC=ptests/config.ml ptests/ptests.ml
2276
ifeq ($(OCAMLWIN32),yes)
2277
# OCaml on Win32 does not support vmthreads, use native ones.
2278
bin/ptests.byte$(EXE): $(PTESTS_SRC)
2279
$(call QUIET,'$(N_LINKING) $@') \
2280
$(OCAMLC) -I ptests -dtypes -thread -g -o $@ \
2281
unix.cma threads.cma str.cma $^
2283
bin/ptests.byte$(EXE): $(PTESTS_SRC)
2284
$(call QUIET,'$(N_LINKING) $@') \
2285
$(OCAMLC) -I ptests -dtypes -vmthread -g -o $@ \
2286
unix.cma threads.cma str.cma $^
2289
bin/ptests.opt$(EXE): $(PTESTS_SRC)
2290
$(call QUIET,'$(N_LINKING) $@') \
2291
$(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
2292
unix.cmxa threads.cmxa str.cmxa $^
2294
ptests/config.ml: Makefile
2295
$(call QUIET, '$(N_MAKING) $@') \
2298
"let default_suites = [" $(PLUGIN_TESTS_LIST:%='"%";') "]" > $@)
2300
#######################
2301
# source distribution #
2302
#######################
2304
STANDALONE_PLUGINS_FILES = \
2305
$(addprefix src/dummy/hello_world/, hello_world.ml Makefile) \
2306
$(addprefix src/dummy/untyped_metrics/, count_for.ml Makefile)
2308
DISTRIB_FILES+= $(PLUGIN_DISTRIBUTED_LIST) $(PLUGINS_DIST_DOC_LIST) $(STANDALONE_PLUGINS_FILES)
2310
EXPORT=frama-c-$(VERSION)
2312
MANUALS= doc/architecture/archi.pdf doc/developer/developer.pdf \
2313
doc/speclang/acsl-implementation.pdf \
2314
doc/valviewer/doc_valviewer_en.pdf
2317
doc/architecture/archi.pdf:
2318
$(MAKE) -C doc/architecture
2320
doc/developer/developer.pdf:
2321
$(MAKE) -C doc/developer
2323
doc/speclang/acsl-implementation.pdf:
2324
$(MAKE) -C doc/speclang acsl-implementation.pdf
2327
$(MAKE) -C doc/valviewer $(basename $@)
2329
doc-distrib: $(PLUGIN_DIST_DOC_LIST) $(MANUALS)
2330
$(MKDIR) doc/manuals
2331
cp doc/developer/developer.pdf doc/manuals/plug-in_development_guide.pdf
2332
cp doc/speclang/acsl-implementation.pdf doc/manuals/acsl-implementation.pdf
2333
cp doc/valviewer/doc_valviewer_en.pdf doc/manuals/frama-c-manual-en.pdf
2335
clean-distrib: dist-clean
2336
rm -fr $(EXPORT) $(EXPORT).tar.gz
2338
src-distrib: doc-distrib src-distrib-ocamlgraph \
2339
$(PLUGIN_DIST_EXTERNAL_LIST)
2340
$(TAR) cf tmp.tar $(DISTRIB_FILES)
2341
$(MKDIR) $(EXPORT)/bin
2342
$(MKDIR) $(EXPORT)/lib/plugins
2343
$(MKDIR) $(EXPORT)/external
2344
cd $(EXPORT); $(TAR) xf ../tmp.tar;
2346
for dir in $(EXPORT)/tests/*; do \
2347
$(MKDIR) $$dir/result; \
2348
$(MKDIR) $$dir/oracle; \
2350
$(TAR) czf $(EXPORT).tar.gz $(EXPORT)
2351
$(CP) $(EXPORT).tar.gz doc/www/src/download
2353
bin-distrib: clean configure
2354
$(RM) -fr $(VERSION)
2355
./configure --prefix `pwd`/$(VERSION) $(CONFIG_DISTRIB_BIN)
2358
if [ -d why ]; then \
2359
$(MAKE) -C why install; \
2361
$(CP) README $(VERSION)
2363
distrib: src-distrib bin-distrib
2365
ifeq (@OCAMLGRAPH_LOCAL@,"")
2366
src-distrib-ocamlgraph:
2367
@ $(ECHO) "Can not make distrib tar ball without local ocamlgraph installation"
2370
src-distrib-ocamlgraph:
2372
$(CP) ocamlgraph.tar.gz $(EXPORT)
2375
ifeq (@JESSIE_LOCAL@,yes)
2377
$(MAKE) -C @WHYDISTRIB@ tarball-for-framac
2378
# Resulting tarball in @WHYDISTRIB@/export/why-for-framac.tar.gz
2380
cd $(EXPORT); $(TAR) zxf ../@WHYDISTRIB@/export/why-for-framac.tar.gz
2381
mv $(EXPORT)/why-* $(EXPORT)/why
2384
@ $(ECHO) "Can not make distrib tar ball without local why installation"
2389
###############################################################################
2391
# compile-command: "LC_ALL=C make"
added
removed
Makefile.in
