-
Julien Signoles authored[e-acsl] fix unexpected interaction with Frama-C compilation when compiling it with --enable-external
Julien Signoles authored[e-acsl] fix unexpected interaction with Frama-C compilation when compiling it with --enable-external
Makefile.in 6.34 KiB
##########################################################################
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2012 #
# 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). #
# #
##########################################################################
#######################
# 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 -journal-disable -print-path)
endif
ifndef FRAMAC_LIBDIR
FRAMAC_LIBDIR :=$(shell frama-c -journal-disable -print-libpath)
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 \
read_header \
error \
misc \
mpz \
env \
typing \
quantif \
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 src-distrib'
IS_DISTRIBUTED:=no
ifneq ($(IS_DISTRIBUTED),yes)
ifeq ($(EACSL_HAS_OCAML312),yes)
DEV_FLAGS=-warn-error +a
else
DEV_FLAGS=-warn-error A
endif
endif
PLUGIN_BFLAGS:=$(DEV_FLAGS)
PLUGIN_OFLAGS:=$(DEV_FLAGS)
#######################
# Local configuration #
#######################
PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
$(PRINT_MAKING) $@
$(RM) $@
$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
$(ECHO) "let version = \""$(VERSION)"\"" >> $@
$(CHMOD_RO) $@
###########
# Testing #
###########
ifeq (@MAY_RUN_TESTS@,yes)
PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime
PLUGIN_NO_DEFAULT_TEST:=yes
tests/test_config: tests/test_config.in Makefile
$(PRINT_MAKING) $@
$(SED) -e "s|${FRAMAC_SHARE}|$(FRAMAC_SHARE)|g" \
-e "s|@SEDCMD@|`which sed `|g" $< > $@
tests:: tests/test_config
endif
###########
# Install #
###########
install::
$(PRINT_CP) E-ACSL share files
$(MKDIR) $(FRAMAC_SHARE)/e-acsl
$(CP) $(E_ACSL_DIR)/share/e-acsl/* $(FRAMAC_SHARE)/e-acsl
$(MKDIR) $(FRAMAC_SHARE)/manuals
$(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
$(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
$(FRAMAC_SHARE)/manuals
uninstall::
$(PRINT_RM) E-ACSL share files
$(RM) -r $(FRAMAC_SHARE)/e-acsl
$(RM) $(FRAMAC_SHARE)/manuals/e-acsl.pdf \
$(FRAMAC_SHARE)/manuals/e-acsl-implementation.pdf
################################
# Building source distribution #
################################
EXPORT =e-acsl-$(VERSION)
DISTRIB_FILES= $(filter-out $(wildcard *local_config.ml), $(wildcard *.ml)) \
$(wildcard *.mli) \
configure.ac Makefile.in \
doc/Changelog \
doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf \
share/e-acsl/*.h \
tests/test_config.in \
tests/e-acsl-reject/test_config tests/e-acsl-reject/*.i \
tests/e-acsl-runtime/test_config tests/e-acsl-runtime/*.i \
license/CEA_LGPL license/headache_config.txt license/LGPLv2.1 \
INSTALL README VERSION .depend
e-acsl-distrib: .depend
$(PRINT_TAR) tmp-distrib
$(TAR) cf tmp.tar $(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
$(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)
WWW = /localhome/julien/frama-c/doc/www
install-distrib: e-acsl-distrib
$(PRINT) Copying to website
$(CP) $(EXPORT).tar.gz $(WWW)/distrib/download/e-acsl
##########
# Header #
##########
headers::
@echo "Applying Headers..."
headache -c license/headache_config.txt -h license/CEA_LGPL \
*.ml *.mli \
Makefile.in configure.ac \
share/e-acsl/*.h
################
# Generic part #
################
include $(FRAMAC_SHARE)/Makefile.dynamic
#####################################
# Regenerating the Makefile on need #
#####################################
ifeq ("$(FRAMAC_INTERNAL)","yes")
CONFIG_STATUS_DIR=$(FRAMAC_SRC)
elseCONFIG_STATUS_DIR=$(E_ACSL_DIR)
endif
$(E_ACSL_DIR)/Makefile: $(E_ACSL_DIR)/Makefile.in \
$(CONFIG_STATUS_DIR)/config.status
cd $(CONFIG_STATUS_DIR) && ./config.status