Makefile

##########################################################################
#                                                                        #
#  This file is part of Frama-C.                                         #
#                                                                        #
#  Copyright (C) 2007-2022                                               #
#    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).            #
#                                                                        #
##########################################################################

# This file is the main makefile of Frama-C.

FRAMAC_SRC=.
MAKECONFIG_DIR=share

include share/Makefile.common

#Check share/Makefile.config available
ifndef FRAMAC_ROOT_SRCDIR
$(error \
  "You should run ./configure first (or autoconf if there is no configure)")
endif

RELEASE?=no
ifeq ($(RELEASE),yes)
DUNE_BUILD_OPTS=--release
else
DUNE_BUILD_OPTS=
endif

###################
# Frama-C Version #
###################

VERSION:=$(shell $(CAT) VERSION)
VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME)

.PHONY: all

all: config.sed
	dune build $(DUNE_BUILD_OPTS) @install

ifeq ($(HAS_DOT),yes)
OPTDOT=Some \"$(DOT)\"
else
OPTDOT=None
endif

ifeq ($(HAS_OCAML408),yes)
  DYNLINK_INIT=fun () -> ()
  FORMAT_STAG=stag
  FORMAT_STRING_OF_STAG=match s with \
        Format.String_tag str -> str \
      | _ -> raise (Invalid_argument \"unsupported tag extension\")
  FORMAT_STAG_OF_STRING=Format.String_tag s
  FORMAT_PP_OPT=Format.pp_print_option
  HAS_OCAML407_OR_408=yes
else
  DYNLINK_INIT=Dynlink.init
  FORMAT_STAG=tag
  FORMAT_STRING_OF_STAG=s
  FORMAT_STAG_OF_STRING=s
  ifeq ($(HAS_OCAML407),yes)
    HAS_OCAML407_OR_408=yes
  else
    HAS_OCAML407_OR_408=no
  endif
  FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \
    match o with \
    | None -> none fmt () \
    | Some v -> pp fmt v
endif

ifeq ($(HAS_OCAML407_OR_408),yes)
  FLOAT_MAX_FLOAT=Float.max_float
else
  FLOAT_MAX_FLOAT=Pervasives.max_float
endif


MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION)
MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION)
VERSION_CODENAME=$(shell $(CAT) VERSION_CODENAME)

# File used by dune to build src/kernel_internals/runtime/fc_config.ml
config.sed: VERSION share/Makefile.config share/Makefile.common Makefile configure.in
	@echo "# generated file" > $@
	@echo "s|@VERSION@|$(VERSION)|" >> $@
	@echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@
	@echo "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|g" >> $@
	@echo "s|@MINOR_VERSION@|$(MINOR_VERSION)|g" >> $@
	@echo "s|@WARNINGS@|$(WARNINGS)|" >> $@
	@echo "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" >> $@
	@echo "s|@FRAMAC_DEFAULT_CPP_ARGS@|$(FRAMAC_DEFAULT_CPP_ARGS)|" >> $@
	@echo "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" >> $@
	@echo "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" >> $@
	@echo "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" >> $@
	@echo "s|@OPTDOT@|$(OPTDOT)|" >> $@

clean:: purge-tests # to be done before a "dune" command
	dune clean
	dune clean --root ptests
	rm -rf _build .merlin config.sed autom4te.cache

########################################################################
# Makefile.config is rebuilt whenever configure.in is modified         #
########################################################################

share/Makefile.config: share/Makefile.config.in config.status
	$(PRINT_MAKING) $@
	./config.status --file $@

share/Makefile.dynamic_config: share/Makefile.dynamic_config.internal
	$(PRINT_MAKING) $@
	$(RM) $@
	$(CP) $< $@
	$(CHMOD_RO) $@

config.status: configure
	$(PRINT_MAKING) $@
	./config.status --recheck

configure: configure.in .force-reconfigure
	$(PRINT_MAKING) $@
	autoconf -f

# If 'make clean' has to be performed after 'git pull':
# change '.make-clean-stamp' before 'git commit'
.make-clean: .make-clean-stamp
	$(TOUCH) $@
	$(QUIET_MAKE) clean

include .make-clean

# force "make clean" to be executed for all users of GIT
force-clean:
	expr `$(CAT) .make-clean-stamp` + 1 > .make-clean-stamp

# force a reconfiguration for all git users
force-reconfigure:
	expr `$(CAT) .force-reconfigure` + 1 > .force-reconfigure


##############################################################################
# INSTALL/UNINSTALL
################################
.PHONY: install uninstall

FRAMAC_INSTALLDIR?=""

install:
ifeq ($(FRAMAC_INSTALLDIR),"")
	dune install
else
	dune install --prefix ${FRAMAC_INSTALLDIR}
	@echo 'DO NOT FORGET TO EXPAND YOUR OCAMLPATH VARIABLE:'
	@echo '  export OCAMLPATH="${FRAMAC_INSTALLDIR}/lib:$$OCAMLPATH"'
endif

uninstall:
ifeq ($(FRAMAC_INSTALLDIR),"")
	dune uninstall
else
	dune uninstall --prefix ${FRAMAC_INSTALLDIR}
endif

###############################################################################
# HEADER MANAGEMENT
################################

# HDRCK is internal
FRAMAC_HDRCK:=headers/hdrck.exe

# Part that can be shared for external plugins
include share/Makefile.headers

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

# PTESTS is internal
FRAMAC_PTESTS:=ptests/ptests.exe

# WTESTS is internal
FRAMAC_WTESTS:=ptests/wtests.exe

# Part that can be shared for external plugins
include share/Makefile.testing

###############################################################################

# Code prettyfication and lint
include share/Makefile.linting

###############################################################################
# Local Variables:
# compile-command: "make"
# End: