Makefile.in

##########################################################################
#                                                                        #
#  This file is part of the Frama-C's E-ACSL plug-in.                    #
#                                                                        #
#  Copyright (C) 2012-2016                                               #
#    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 license/LGPLv2.1).             #
#                                                                        #
##########################################################################

#######################
# Frama-C Environment #
#######################

# Do not use ?= to initialize both below variables
# (fixed efficiency issue, see GNU Make manual, Section 8.11)
ifndef FRAMAC_SHARE
FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
endif

# OCAMLVERSION and HAS_OCAML312 are defined in Frama-C common Makefile but
# cannot be used at this point. Unfortunatly cannot reuse the same variable name
# here without introducing unexpected interaction with Frama-C compilation when
# compiling it with --enable-external=e-acsl.
EACSL_OCAMLVERSION 	?=@OCAMLVERSION@
ifeq ($(findstring 3.12,$(EACSL_OCAMLVERSION)),)
EACSL_HAS_OCAML312 = no
else
EACSL_HAS_OCAML312 = yes
endif

#########################
# Plug-in configuration #
#########################

PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= local_config \
	options \
	rte \
	error \
	misc \
	gmpz \
	literal_strings \
	mmodel_analysis \
	dup_functions \
	label \
	env \
	interval \
	typing \
	quantif \
	translate \
	loops \
	visit \
	main

PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=no

PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_DISTRIB_BIN:=no

###############
# Local Flags #
###############

# Enable -warn-error in development mode, but not in distribution mode
# Do not edit the line below: it is automatically set by 'make e-acsl-distrib'
IS_DISTRIBUTED:=no
ifneq ($(IS_DISTRIBUTED),yes)
ifeq ($(EACSL_HAS_OCAML312),yes)
EACSL_DEV_FLAGS=-warn-error +a
else
EACSL_DEV_FLAGS=-warn-error A
endif
endif
PLUGIN_BFLAGS:=$(EACSL_DEV_FLAGS)
PLUGIN_OFLAGS:=$(EACSL_DEV_FLAGS)

#######################
# Local configuration #
#######################

PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml

EACSL_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)

$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
	$(PRINT_MAKING) $@
	$(RM) $@
	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
	$(ECHO) "let version = \""$(EACSL_VERSION)"\"" >> $@
	$(CHMOD_RO) $@

###########
# Testing #
###########

ifeq (@MAY_RUN_TESTS@,yes)

$(PLUGIN_DIR)/tests/print.cmxs: OFLAGS=-I $(FRAMAC_LIB)
$(PLUGIN_DIR)/tests/print.cmo: BFLAGS=-I $(FRAMAC_LIB)

PLUGIN_TESTS_DIRS := e-acsl-reject e-acsl-runtime bts gmp no-main
E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config \
	$(PLUGIN_DIR)/tests/print.cmxs \
	$(PLUGIN_DIR)/tests/print.cmo

endif

######################
# Benchmarking tools #
######################
BM_TOOLS_SOURCES = $(wildcard $(PLUGIN_DIR)/benchmarking/tools/*.c)
BM_TOOLS_BINARIES = $(patsubst %.c,%, $(BM_TOOLS_SOURCES))

CFLAGS = -g3 -O2 -std=c11 -pedantic -Wall -Wno-unused-result

$(BM_TOOLS_BINARIES): % : %.c
	$(PRINT_CC) $@
	$(CC) $(CFLAGS) -o $@ $^

all:: $(BM_TOOLS_BINARIES)

clean::
	$(PRINT_RM) benchmarking tools
	$(RM) $(BM_TOOLS_BINARIES)

################################################
# E-ACSL C Libs: libjemalloc, libgmp					 #
################################################
LOCAL_LIB := $(PLUGIN_DIR)/lib
JEMALLOC_DIR := $(PLUGIN_DIR)/contrib/libjemalloc
JEMALLOC_LIBNAME = libjemalloc-e-acsl.a
JEMALLOC_LIB = $(LOCAL_LIB)/$(JEMALLOC_LIBNAME)

$(JEMALLOC_LIB):
	cd $(JEMALLOC_DIR) && \
		./autogen.sh \
  		--with-jemalloc-prefix="__e_acsl_native_" \
  		--with-private-namespace="__e_acsl_hidden_" \
  		--with-install-suffix="-e-acsl" && \
		$(MAKE) $(MAKEOPTS) lib/$(JEMALLOC_LIBNAME)
	$(CP) $(JEMALLOC_DIR)/lib/$(JEMALLOC_LIBNAME) $@

GMP_DIR := $(PLUGIN_DIR)/contrib/libgmp
GMP_LIBNAME = libgmp-e-acsl.a
GMP_LIB = $(LOCAL_LIB)/$(GMP_LIBNAME)

$(GMP_LIB):
	cd $(GMP_DIR) && ./configure && $(MAKE) $(MAKEOPTS)
	$(CP) $(GMP_DIR)/.libs/libgmp.a $@

all:: $(JEMALLOC_LIB) $(GMP_LIB)

clean::
	$(PRINT_RM) e-acsl contrib libraries
	$(RM) $(JEMALLOC_LIB) $(GMP_LIB)
	if test -f $(JEMALLOC_DIR)/Makefile; \
		then $(MAKE) -C$(JEMALLOC_DIR) relclean; \
	fi
	if test -f $(GMP_DIR)/Makefile; \
		then $(MAKE) -C$(GMP_DIR) distclean; \
	fi

############
# Cleaning #
############

clean::
	$(PRINT_RM) cleaning generated test and doc files
	$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
	$(RM) $(E_ACSL_DIR)/tests/test_config
	$(RM) $(foreach dir, $(PLUGIN_TESTS_DIRS), tests/$(dir)/result/*)
	$(RM) $(E_ACSL_DIR)/doc/doxygen/html/*
	$(RM) $(E_ACSL_DIR)/doc/doxygen/warn.log
	$(RM) $(E_ACSL_DIR)/doc/code/*

DISTCLEANFILES = $(wildcard \
	Makefile config.log config.status configure .depend autom4te.cache/* \
	doc/doxygen/doxygen.cfg \
	META.frama-c-e_acsl Makefile.plugin.generated local_config.ml top/*)

distclean:
	$(MAKE) -s clean
	$(PRINT_RM) generated files
	$(RM) $(addprefix $(E_ACSL_DIR)/, $(DISTCLEANFILES))

################################
# Building source distribution #
################################

EXPORT = e-acsl-$(EACSL_VERSION)

OCAML_FILES = \
	$(filter-out $(wildcard *local_config.ml), $(wildcard *.ml)) \
	$(wildcard *.mli)

DOC_FILES = \
	doc/manuals/e-acsl-manual.pdf  \
	doc/manuals/e-acsl.pdf \
	doc/manuals/e-acsl-implementation.pdf \
	doc/doxygen/doxygen.cfg.in \
	doc/Changelog \
	man/e-acsl-gcc.sh.1

TEST_FILES = \
	tests/test_config.in \
	tests/print.ml \
	$(foreach dir, $(TESTDIRS), $(wildcard $(dir)/* $(dir)/*/*))

RTL_FILES = $(wildcard share/e-acsl/*.[ch] share/e-acsl/*/*.[ch])

SCRIPT_FILES = scripts/e-acsl-gcc.sh scripts/testrun.sh

LICENSE_FILES = \
	license/CEA_LGPL license/SPARETIMELABS \
	license/headache_config.txt license/LGPLv2.1

EACSL_DISTRIB_FILES = \
	configure.ac Makefile.in \
	INSTALL README VERSION .depend \
	$(OCAML_FILES) \
	$(DOC_FILES) \
	$(TEST_FILES) \
	$(RTL_FILES) \
	$(SCRIPT_FILES) \
	$(LICENSE_FILES)

# BE CAREFUL: manually remove all *.ml* files which should not be released!
e-acsl-distrib: .depend
	$(PRINT_TAR) tmp-distrib
	$(TAR) cf tmp.tar $(EACSL_DISTRIB_FILES)
	$(PRINT_MAKING) export directories
	$(MKDIR) $(EXPORT)
	$(PRINT_UNTAR) tmp-distrib
	cd $(EXPORT); \
	  $(TAR) xf ../tmp.tar; autoconf; \
	  $(SED) -i \
	    -e 's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/' Makefile.in; \
	  $(RM) -rf autom4te.cache
	$(PRINT_RM) tmp-distrib
	$(RM) tmp.tar
	$(PRINT_MAKING) test directories
	for dir in $(EXPORT)/tests/*; do \
	  if test -d $$dir; then \
	    $(MKDIR) $$dir/result; \
	    $(MKDIR) $$dir/oracle; \
          fi \
	done
	$(PRINT_MAKING) archive
	$(TAR) czf $(EXPORT).tar.gz $(EXPORT)
	$(PRINT) Cleaning
	$(RM) -fr $(EXPORT)

dist: e-acsl-distrib

WWW	?= /localhome/julien/frama-c/doc/www
e-acsl-install-distrib: e-acsl-distrib
	$(PRINT) Copying to website
	$(CP) $(EXPORT).tar.gz $(WWW)/distrib/download/e-acsl
	$(CP) $(DOC_FILES) $(WWW)/distrib/download/e-acsl
	$(CP) doc/manuals/e-acsl-manual.pdf \
	      $(WWW)/distrib/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
	$(CP) doc/manuals/e-acsl.pdf \
	      $(WWW)/distrib/download/e-acsl/e-acsl-1.7.pdf
	$(CP) doc/manuals/e-acsl-implementation.pdf \
	      $(WWW)/distrib/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf

##############################
# Check source distribution  #
##############################
distcheck:
	$(RM) -rf $(EXPORT)*
	$(MAKE) e-acsl-distrib
	$(TAR) -xvf $(EXPORT).tar.gz
	cd $(EXPORT)
	autoconf
	./configure
	$(MAKE)
	$(MAKE) tests
	$(MAKE) doc
	cd ../
	$(RM) -rf $(EXPORT)*

##########
# Header #
##########

headers::
	@echo "Applying Headers..."
	headache -c license/headache_config.txt -h license/CEA_LGPL \
		*.ml *.mli \
		Makefile.in configure.ac \
		share/e-acsl/*.[ch] share/e-acsl/*/*.[ch] scripts/*.sh
	headache -c license/headache_config.txt -h license/SPARETIMELABS \
		share/e-acsl/e_acsl_printf.h

################
# Generic part #
################

include $(FRAMAC_SHARE)/Makefile.dynamic

###########
# Install #
###########

install::
	$(PRINT_INSTALL) E-ACSL share files
	$(MKDIR) $(FRAMAC_DATADIR)/e-acsl
	$(CP) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl
	$(MKDIR) $(FRAMAC_DATADIR)/e-acsl/bittree_model \
		 $(FRAMAC_DATADIR)/e-acsl/glibc
	$(CP) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \
		$(FRAMAC_DATADIR)/e-acsl/bittree_model
	$(CP) $(E_ACSL_DIR)/share/e-acsl/glibc/* $(FRAMAC_DATADIR)/e-acsl/glibc
	$(PRINT_INSTALL) E-ACSL manuals
	$(MKDIR) $(FRAMAC_DATADIR)/manuals
	$(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
	      $(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
	      $(E_ACSL_DIR)/doc/manuals/e-acsl-manual.pdf \
		$(FRAMAC_DATADIR)/manuals
	$(PRINT_INSTALL) E-ACSL libraries
	$(MKDIR) $(LIBDIR)
	$(CP) $(JEMALLOC_LIB) $(LIBDIR)
	$(CP) $(GMP_LIB) $(LIBDIR)
	$(PRINT_INSTALL) E-ACSL scripts
	$(MKDIR) $(BINDIR)
	$(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/
	$(PRINT_INSTALL) E-ACSL man pages
	$(MKDIR) $(MANDIR)/man1
	$(CP) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/

uninstall::
	$(PRINT_RM) E-ACSL share files
	$(RM) -r $(FRAMAC_DATADIR)/e-acsl
	$(PRINT_RM) E-ACSL manuals
	$(RM) $(FRAMAC_DATADIR)/manuals/e-acsl.pdf \
	      $(FRAMAC_DATADIR)/manuals/e-acsl-implementation.pdf \
	      $(FRAMAC_DATADIR)/manuals/e-acsl-manual.pdf
	$(PRINT_RM) E-ACSL libraries
	$(PRINT_INSTALL) E-ACSL share files
	$(MKDIR) $(FRAMAC_DATADIR)/e-acsl
	$(RM) $(LIBDIR)/$(JEMALLOC_LIBNAME)
	$(RM) $(LIBDIR)/$(GMP_LIBNAME)
	$(PRINT_RM) E-ACSL scripts
	$(RM) $(BINDIR)/e-acsl-gcc.sh
	$(PRINT_RM) man pages
	$(RM) $(MANDIR)/man1/e-acsl-gcc.sh.1

####################
# Testing (part 2) #
####################

ifeq (@MAY_RUN_TESTS@,yes)

$(E_ACSL_DIR)/tests/test_config: $(E_ACSL_DIR)/tests/test_config.in \
				$(E_ACSL_DIR)/Makefile
	$(PRINT_MAKING) $@
	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@

endif

#####################################
# Regenerating the Makefile on need #
#####################################

ifeq ("$(FRAMAC_INTERNAL)","yes")
CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
CONFIG_STATUS_DIR_DEP:=
else
CONFIG_STATUS_DIR:=$(E_ACSL_DIR)
CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
endif

$(E_ACSL_DIR)/Makefile: $(E_ACSL_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
	cd $(CONFIG_STATUS_DIR) && ./config.status

#####################################
# Doxygen                           #
#####################################

DOXYGEN = @DOXYGEN@
doxygen:
	if ! test $(DOXYGEN) = "no"; then \
		$(DOXYGEN) $(E_ACSL_DIR)/doc/doxygen/doxygen.cfg ; \
	else \
	  echo "Warning: Skip doxygen documentation: \
Doxygen executable not found."; \
	fi

doc:: doxygen

clean::
	$(PRINT_RM) generated documentation
	$(RM) $(E_ACSL_DIR)/doc/doxygen/html/*
	$(RM) $(E_ACSL_DIR)/doc/code/*