frama-c-base 20111001+nitrogen+dfsg-3 / usr / share / frama-c / Makefile.common

##########################################################################
#                                                                        #
#  This file is part of Frama-C.                                         #
#                                                                        #
#  Copyright (C) 2007-2011                                               #
#    CEA (Commissariat à l'énergie atomique et aux énergies              #
#         alternatives)                                                  #
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the GNU   #
#  Lesser General Public License as published by the Free Software       #
#  Foundation, version 2.1.                                              #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
#  GNU Lesser General Public License for more details.                   #
#                                                                        #
#  See the GNU Lesser General Public License version 2.1                 #
#  for more details (enclosed in the file licenses/LGPLv2.1).            #
#                                                                        #
##########################################################################

##########################################################################
#                                                                        #
# Define common stuff shared by makefiles.                               #
#                                                                        #
##########################################################################

include $(MAKECONFIG_DIR)/Makefile.config

#######################
# Working directories #
#######################

# Frama-C kernel directories
UNPACKED_DIRS= misc ai memory_state toplevel slicing_types pdg_types \
	       kernel logic lib type project buckx gui
UNPACKED_DIRS:= $(addprefix src/, $(UNPACKED_DIRS))
UNPACKED_DIRS+= external

CIL_PATH= cil/src
CIL_DIRS= $(CIL_PATH) $(CIL_PATH)/ext $(CIL_PATH)/frontc $(CIL_PATH)/logic \
	cil/ocamlutil

FRAMAC_SRC_DIRS=$(UNPACKED_DIRS) $(CIL_DIRS)

##################
# Flags          #
##################

ifeq ($(findstring 3.10,$(OCAMLVERSION)),)
HAS_OCAML311 = yes
else
HAS_OCAML311 = no
endif

ifeq ($(HAS_OCAML311),yes)
ifeq ($(findstring 3.12,$(OCAMLVERSION)),)
HAS_OCAML312 = no
else
HAS_OCAML312 = yes
endif
else
HAS_OCAML312 = no
endif

# All warnings are activated by default: this could grow up the chance of
# compatibility breaks with future versions of the caml compilers.
# BUT that is only the case of the SVN version
# since the distrib is not compiled with -warn-error.
# See BTS #310 and #638.
ifeq ($(HAS_OCAML312),yes)
WARNINGS= -w +a-4-6-7-9 # add warning 7 and 9 whenever 3.12 will be mandatory
else
WARNINGS= -w Ael
endif

FLAGS	= $(WARNINGS) $(OCAML_ANNOT_OPTION) $(OPTIM)
DEBUG	= -g

#############
# Verbosing #
#############

ifneq ($(VERBOSEMAKE),no) # Do not change to ifeq ($(VERBOSEMAKE),yes), as this
                          # version makes it easier for the user to set the
			  # option on the command-line to investigate
			  # Makefile-related problems
# ignore the PRINT_* materials but print all the other commands
  PRINT = @true
# prevent the warning "jobserver unavailable: using -j1".
# see GNU make manual (section 5.7.1 and appendix B)
  QUIET_MAKE:= + $(MAKE)
# prevent the warning: "-jN forced in submake: disabling jobserver mode".
# see GNU make manual (appendix B)
  MAKE := MAKEFLAGS="$(patsubst j,,$(MAKEFLAGS))" $(MAKE)
else
# print the PRINT_* materials
  PRINT = @echo
# but silently execute all the other commands
# fixed bug #637: do not write spaces between flags
  OLDFLAGS:=r$(MAKEFLAGS)
  MAKEFLAGS:=rs$(MAKEFLAGS)
# do not silently execute other makefiles (e.g the one of why):
# the redefinition of MAKE below is for this purpose
# but use QUIET_MAKE in order to call silently the initial Makefile
  QUIET_MAKE:= + $(MAKE)
  MAKE := MAKEFLAGS="$(OLDFLAGS)" $(MAKE)
endif

################
# Calling Make #
################

# Function to be called to call make on a given plugin (first argument) and
# a given rule (second argument)
external_make = \
  $(MAKE) FRAMAC_INTERNAL=yes \
          PLUGIN_LIB_DIR="\
             $(if $(filter /%,$(PLUGIN_LIB_DIR)),$(PLUGIN_LIB_DIR),\
                    $(FRAMAC_TOP_SRCDIR)/$(PLUGIN_LIB_DIR))" \
          PLUGIN_GUI_LIB_DIR="\
            $(if $(filter /%,$(PLUGIN_GUI_LIB_DIR)),$(PLUGIN_GUI_LIB_DIR),\
                   $(FRAMAC_TOP_SRCDIR)/$(PLUGIN_GUI_LIB_DIR))" \
          FRAMAC_LIBDIR="$(FRAMAC_TOP_SRCDIR)/lib/fc" \
          FRAMAC_SHARE="$(FRAMAC_TOP_SRCDIR)/share" -C $(1) $(2)

##################
# Shell commands #
##################

# prefer to use these commands and not directly "cp" or others

CAT	= cat
CHMOD	= chmod
CHMOD_RO= true
CHMOD_RW= sh -c \
'for f in "$$@"; do \
  if test -e $$f; then chmod u+w $$f; fi \
done' chmod_rw
CP      = /bin/cp
ECHO	= echo
MKDIR   = mkdir -p
MV	= mv
ISED	= sh -c \
'new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1; \
sed "$$@" > $$new_temp; \
eval last=\$${$$\#}; \
mv $$new_temp $$last' sed_inplace
SED	= sed
RM	= rm -f
TAR	= tar
TOUCH	= touch

###########################
# Command pretty printing #
###########################

PRINT_OCAMLC   	=$(PRINT) 'Ocamlc      '#
PRINT_OCAMLOPT 	=$(PRINT) 'Ocamlopt    '#
PRINT_DEP      	=$(PRINT) 'Ocamldep    '#
PRINT_OCAMLLEX 	=$(PRINT) 'Ocamllex    '#
PRINT_OCAMLYACC	=$(PRINT) 'Ocamlyacc   '#
PRINT_OCAMLMKTOP=$(PRINT) 'Ocamlmktop  '#
PRINT_DOC	=$(PRINT) 'Ocamldoc    '#
PRINT_OCAMLCP  	=$(PRINT) 'Profiling   '#
PRINT_CAMLP4   	=$(PRINT) 'Camlp4      '#
PRINT_PACKING  	=$(PRINT) 'Packing     '#
PRINT_LINKING  	=$(PRINT) 'Linking     '#

PRINT_MAKING   	=$(PRINT) 'Generating  '#
PRINT_MV       	=$(PRINT) 'Moving to   '#
PRINT_CP       	=$(PRINT) 'Copying to  '#
PRINT_RM       	=$(PRINT) 'Cleaning    '#
PRINT_EXEC	=$(PRINT) 'Running     '#
PRINT_TAR    	=$(PRINT) 'Archiving   '#
PRINT_UNTAR    	=$(PRINT) 'Unarchiving '#
PRINT_CONFIG   	=$(PRINT) 'Configuring '#
PRINT_BUILD   	=$(PRINT) 'Building    '#
PRINT_INSTALL  	=$(PRINT) 'Installing  '#
PRINT_UPDATE  	=$(PRINT) 'Updating    '#

PRINT_DOT	=$(PRINT) 'Dot         '#
PRINT_LATEX	=$(PRINT) 'Latex       '#
PRINT_DVIPS	=$(PRINT) 'Dvips       '#
PRINT_HEVEA	=$(PRINT) 'Hevea       '#

#########
# Tests #
#########

define COMPILE_TESTS_ML_FILES
# Function with two arguments:
#  - $(1) is the test directory under consideration.
#  - $(2) is the name of Frama-C component under test (plugin or some core part)
ML_TESTS:=$(wildcard tests/$(1)/*.ml)
.PRECIOUS: $(patsubst %.ml, %.cmo, $(ML_TESTS)) \
	$(patsubst %.ml, %.cmx, $(ML_TESTS)) \
	$(patsubst %.ml, %.cmxs, $(ML_TESTS)) \
	$(patsubst %.ml, %.opt, $(ML_TESTS)) \
	$(patsubst %.ml, %.byte, $(ML_TESTS))

# [JS 2009/03/18] in the 5 rules below, don't print anything while VERBOSEMAKE
# is not set (otherwise "make tests" is too much verbose)

$(1)_TESTS_INCLUDES=$$(addprefix -I tests/, $$($(2)_TESTS_DIRS))

tests/$(1)/%.cmo: tests/$(1)/%.ml $$(CMO) $$(GEN_BYTE_LIBS)
	$$(OCAMLC) -c $$(BFLAGS) $$($(1)_TESTS_INCLUDES) $$<

tests/$(1)/%.byte: tests/$(1)/%.cmo $(3:.cmx=.cmo) bin/toplevel.byte$$(EXE)
	$$(OCAMLC) $$(BLINKFLAGS) $$($(1)_TESTS_INCLUDES) -o $$@ \
	  $$(BYTE_LIBS) $$(filter-out $$(STARTUP_CMO),$$(ALL_BATCH_CMO)) $(3:.cmx=.cmo) \
	  $$< $$(STARTUP_CMO)

# [JS 2009/05/29] don't use $$(CMX)
# [VP 2010/04/22] don't call directly ocamlopt, just refine flags of generic
# rule, which is chosen by make anyway
tests/$(1)/%.cmx: OFLAGS+=$$($(1)_TESTS_INCLUDES)

$(patsubst %.ml,%.cmx,$(wildcard tests/$(1)/*.ml tests/$(1)/*/*.ml)): \
           $$(CMO:.cmo=.cmx) $$(GEN_OPT_LIBS)

tests/$(1)/%.cmxs: tests/$(1)/%.ml $$(CMO:.cmo=.cmx) $$(GEN_OPT_LIBS)
	$$(OCAMLOPT) $$(OFLAGS) $$($(1)_TESTS_INCLUDES) -shared -o $$@ $$<

tests/$(1)/%.opt: tests/$(1)/%.cmx $(3) bin/toplevel.opt$$(EXE)
	$$(OCAMLOPT) $$(OLINKFLAGS) $$($(1)_TESTS_INCLUDES) -o $$@ \
	  $$(OPT_LIBS) $$(filter-out $$(STARTUP_CMX),$$(ALL_BATCH_CMX)) $(3) $$< $$(STARTUP_CMX)

$(filter-out $(3),$(patsubst %.ml,%.cmx,$(wildcard tests/$(1)/*.ml))): $(3)
$(filter-out $(3:.cmx=.cmo), \
    $(patsubst %.ml,%.cmo,$(wildcard tests/$(1)/*.ml))): \
     $(3:.cmx=.cmo)

endef #COMPILE_TESTS_ML_FILES

#################
# Documentation #
#################

ifeq ("$(OCAMLDOC)","ocamldoc.opt")
DOC_PLUGIN=$(DOC_DIR)/docgen.cmxs
else
DOC_PLUGIN=$(DOC_DIR)/docgen.cmo
endif

#################
# Generic rules #
#################

.DEFAULT_GOAL=all

ifndef SUFFIXES_ARE_SET

SUFFIXES_ARE_SET:=true

# The former .SUFFIXES delete all predefined implicit rules
# The latter .SUFFIXES defines our suffix list
# See GNU Make manual, section 10.7
# This way of declaring implicit rules is deprecated,
# but that is the only way for removing **all** predefined implicit rules
# The only other way is to remove each predefined implicit rule, one by one.
.SUFFIXES:
.SUFFIXES: .c .o .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html .cmxs \
	.png .svg .ps

ifdef DOT
%.png: %.dot
	$(PRINT_DOT) $@
	$(DOT) -Tpng -o $@ $<

%.svg: %.dot
	$(PRINT_DOT) $@
	$(ISED) -e "s/\(digraph .*\)/\1 node [href=\"\\N.html\"];/" $<
	$(DOT) -Tsvg -o $@ $<

%.ps: %.dot
	$(PRINT_DOT) $@
	$(DOT) -Tps -o $@ $<
else
%.png: %.dot
	@$(ECHO) "dot missing: generation of $@ skipped."
%.svg: %.dot
	@$(ECHO) "dot missing: generation of $@ skipped."
%.ps: %.dot
	@$(ECHO) "dot missing: generation of $@ skipped."
endif

.mli.cmi:
	$(PRINT_OCAMLC) $@
	$(OCAMLC) -c $(BFLAGS) $<

.ml.cmi:
	$(PRINT_OCAMLC) $@
	if `test -e $<i`; then $(OCAMLC) -c $(BFLAGS) $<i; \
	else $(MAKE) $(patsubst %.ml,%.cmo,$<); fi

.ml.cmo:
	$(PRINT_OCAMLC) $@
	$(OCAMLC) -c $(BFLAGS) $<

%.cmx: %.ml
	$(PRINT_OCAMLOPT) $@
	$(OCAMLOPT) -c $(OFLAGS) $<

# .o are generated together with .cmx, but %.o %.cmx: %.ml only confuses
# make when computing dependencies...
%.o: %.cmx
	:

.ml.cmxs:
	$(PRINT_PACKING) $@
	$(OCAMLOPT) -shared -o $@ $(OFLAGS) $<

.mll.ml:
	$(PRINT_OCAMLLEX) $@
	$(CHMOD_RW) $@
	$(OCAMLLEX) $<
	$(CHMOD_RO) $@

%.mli %.ml: %.mly
	$(PRINT_OCAMLYACC) $@
	$(CHMOD_RW) $(<:.mly=.ml) $(<:.mly=.mli)
	$(OCAMLYACC) -v $<
	$(CHMOD_RO) $(<:.mly=.ml) $(<:.mly=.mli)

.tex.dvi:
	$(PRINT_LATEX) $@
	latex $< && latex $<

.dvi.ps:
	$(PRINT_DVIPS) $@
	dvips $< -o $@

.tex.html:
	$(PRINT_HEVEA) $@
	hevea $<

.c.o:
	$(PRINT_OCAMLC) $@
	$(OCAMLC) $(BFLAGS) -ccopt "-o $@" $<

endif