-
François Bobot authored
because always true now
François Bobot authoredbecause always true now
configure.in 31.08 KiB
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2019 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# INRIA (Institut National de Recherche en Informatique et en #
# Automatique) #
# #
# 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). #
# #
##########################################################################
# autoconf input for Objective Caml programs
# Copyright (C) 2001 Jean-Christophe Filliâtre
# from a first script by Georges Mariano
# the script generated by autoconf from this input will set the following
# variables:
# OCAMLC "ocamlc" if present in the path, or a failure
# or "ocamlc.opt" if present with same version number as ocamlc
# OCAMLOPT "ocamlopt" (or "ocamlopt.opt" if present), or "no"
# OCAMLBEST either "byte" if no native compiler was found,
# or "opt" otherwise
# OCAMLDEP "ocamldep"
# OCAMLLEX "ocamllex" (or "ocamllex.opt" if present)
# OCAMLYACC "ocamlyacc"
# OCAMLLIB the path to the ocaml standard library
# OCAMLVERSION the ocaml version number
# OCAMLWIN32 "yes"/"no" depending on Sys.os_type = "Win32"
# EXE ".exe" if OCAMLWIN32=yes, "" otherwise
AC_INIT(src/kernel_internals/runtime/boot.ml)
define([FRAMAC_MAIN_AUTOCONF])
m4_include(share/configure.ac)
AC_SUBST([FRAMAC_VERSION],[`cat VERSION`])
# export CYGWIN=nobinmode
##########################
# Check for Make version #
##########################
new_section "configure make"
AC_CHECK_PROGS(MAKE,gmake make,make,)
AC_MSG_CHECKING([version of make])
MAKE_DISTRIB=`sh -c "$MAKE -v | sed -n -e 's/\(.*\) Make.*$/\1/p'"`
MAKE_MAJOR=`sh -c "$MAKE -v | sed -n -f bin/sed_get_make_major"`
MAKE_MINOR=`sh -c "$MAKE -v | sed -n -f bin/sed_get_make_minor"`
AC_MSG_RESULT($MAKE_MAJOR.$MAKE_MINOR)
if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 \
-o "$MAKE_MAJOR" = 3 -a "$MAKE_MINOR" -lt 81
then
AC_MSG_ERROR([unsupported version; GNU Make version 3.81
or higher is required.]);
fi
# verbosemake feature
AC_ARG_ENABLE(
verbosemake,
[ --enable-verbosemake verbose makefile commands],
VERBOSEMAKE=$enableval,
VERBOSEMAKE=no
)
if test "$VERBOSEMAKE" = yes ; then
AC_MSG_RESULT(Make will be verbose.)
fi
##########################################
# Check for invalid command-line options #
##########################################
case $prefix in
*\ * ) AC_MSG_ERROR(spaces not allowed in --prefix argument "$prefix");;
* ) ;;
esac
#############################
# Check for Ocaml compilers #
#############################
new_section "configure ocaml compilers"
# we first look for ocamlc in the path; if not present, we fail
AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
if test "$OCAMLC" = no ; then
AC_MSG_ERROR(Cannot find ocamlc.)
fi
# we extract Ocaml version number and library path
# "sed -n" is the posix version of "sed --quiet"
AC_MSG_CHECKING(version of OCaml)
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
AC_MSG_RESULT($OCAMLVERSION)
case $OCAMLVERSION in
0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*)
AC_MSG_ERROR(Incompatible OCaml version; use 4.05+.);;
*)
OCAML_ANNOT_OPTION="-bin-annot";;
esac
AC_SUBST(OCAMLMAJORNB)
AC_SUBST(OCAMLMINORNB)
AC_SUBST(OCAMLPATCHNB)
AC_SUBST(HAS_OCAML407)
AC_SUBST(HAS_OCAML408)
OCAMLMAJORNB=$(echo $OCAMLVERSION | cut -f 1 -d .)
OCAMLMINORNB=$(echo $OCAMLVERSION | cut -f 2 -d .)
OCAMLPATCHNB=$(echo $OCAMLVERSION | cut -f 3 -d .)
if test $OCAMLMAJORNB -gt 4; then
HAS_OCAML407=yes;
HAS_OCAML408=yes;
else
HAS_OCAML407=no;
HAS_OCAML408=no;
if test $OCAMLMINORNB -ge 7; then
HAS_OCAML407=yes;
fi;
if test $OCAMLMINORNB -ge 8; then
HAS_OCAML408=yes;
fi;
fi; # MAJORNB -gt 4
# Ocaml library path
AC_MSG_CHECKING(OCaml library path)
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
AC_MSG_RESULT($OCAMLLIB)
# then we look for ocamlopt; if not present, we issue a warning
# if the version or the stdlib directory is not the same, we also discard it
# we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not
AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no)
OCAMLBEST=byte
if test "$OCAMLOPT" = no ; then
AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
else
AC_MSG_CHECKING(ocamlopt version and standard library)
TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
if test "$TMPVERSION" != "$OCAMLVERSION" \
-o `$OCAMLOPT -where | tr -d '\\r'` != "$OCAMLLIB"; then
AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
OCAMLOPT=no
else
AC_MSG_RESULT(ok)
OCAMLBEST=opt
fi
fi
# In case we have a native compiler, check that native dynlink works.
# Otherwise, fall back to bytecode-only compilation
if test "$OCAMLBEST" = opt; then
echo "let f x y =" > test_dynlink.ml
echo " Dynlink.loadfile \"foo\"; " >> test_dynlink.ml
echo " ignore (Dynlink.is_native);" >> test_dynlink.ml
echo " abs_float (x -. y)" >> test_dynlink.ml
if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
2> /dev/null ; \
then
AC_MSG_RESULT([native dynlink works fine. Great.])
else
AC_MSG_WARN([Native dynlink does not work, disabling native compilation.])
OCAMLBEST=byte
fi
rm -f test_dynlink.*
fi
if test "$OCAMLBEST" = "opt"; then
LIB_SUFFIX=cmxa
DYN_SUFFIX=cmxs
OBJ_SUFFIX=cmx;
else
LIB_SUFFIX=cma
DYN_SUFFIX=cma
OBJ_SUFFIX=cmo;
fi
# checking for ocamlfind
AC_CHECK_PROG(OCAMLFIND,ocamlfind,ocamlfind,no)
if test "$OCAMLFIND" != no ; then
OCAMLC="$OCAMLFIND ocamlc"
OCAMLOPT="$OCAMLFIND ocamlopt"
else
AC_MSG_ERROR(Cannot find ocamlfind.)
fi
###################################################
# Select devel compilation (warnings, warn-error) #
###################################################
# It is inherited by the plugins
if test -e ".for_devel"; then
DEFAULT_DEVEL_MODE=yes
else
DEFAULT_DEVEL_MODE=no
fi
AC_ARG_ENABLE(
devel-mode,
[ --enable-devel-mode force the devel mode (warnings and warn-error).
--disable-devel-mode force the distrib mode (no warnings and no warn-error).
],
DEVELOPMENT=$enableval,
DEVELOPMENT=$DEFAULT_DEVEL_MODE, # default value
)
if test "$DEVELOPMENT" = "yes" ; then
AC_MSG_NOTICE(Development mode: warnings and warn-errors are activated)
else
AC_MSG_NOTICE(Distribution mode: all warnings are deactivated)
fi
##############################################
# Check for other mandatory tools/libraries #
##############################################
new_section "configure mandatory tools and libraries"
# ocamldep
AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no)
if test "$OCAMLDEP" = no ; then
AC_MSG_ERROR(Cannot find ocamldep.)
else
OCAMLDEP="$OCAMLFIND ocamldep"
fi
# ocamllex
AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no)
if test "$OCAMLLEX" = no ; then
AC_MSG_ERROR(Cannot find ocamllex.)
else
AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no)
if test "$OCAMLLEXDOTOPT" != no ; then
OCAMLLEX=$OCAMLLEXDOTOPT
fi
fi
# ocamlyacc
AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
if test "$OCAMLYACC" = no ; then
AC_MSG_ERROR(Cannot find ocamlyacc.)
fi
# ocamlcp
AC_CHECK_PROG(OCAMLCP,ocamlcp,ocamlcp,no)
if test "$OCAMLCP" = no ; then
AC_MSG_ERROR(Cannot find ocamlcp.)
else
OCAMLCP="$OCAMLFIND ocamlcp"
fi
# ocamlgraph
############
AC_MSG_CHECKING(for ocamlgraph)
OCAMLGRAPH=$($OCAMLFIND query ocamlgraph -format %v)
if test -z "$OCAMLGRAPH" ; then
AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \
(requires ocamlgraph 1.8.5 or higher).)
ficase $OCAMLGRAPH in
0.* | 1.[[01234567]].* \
| 1.8.0 | 1.8.0+dev \
| 1.8.1 | 1.8.1+dev \
| 1.8.2 | 1.8.2+dev \
| 1.8.3 | 1.8.3+dev \
| 1.8.4 | 1.8.4+dev)
AC_MSG_ERROR(found $OCAMLGRAPH: requires 1.8.5 or higher.);;
1.8.5 | 1.8.6 | 1.8.7)
AC_MSG_RESULT(found);;
*)
AC_MSG_RESULT(found $OCAMLGRAPH: should work);;
esac
# zarith
########
AC_MSG_CHECKING(for zarith)
ZARITH=$($OCAMLFIND query zarith -format %v)
if test -z "$ZARITH" ; then
AC_MSG_ERROR(Cannot find zarith via ocamlfind.)
else
AC_MSG_RESULT(found $ZARITH)
fi
# yojson
########
AC_MSG_CHECKING(for Yojson)
YOJSON=$($OCAMLFIND query yojson -format %v)
if test -z "$YOJSON" ; then
AC_MSG_ERROR(Cannot find yojson via ocamlfind \
(requires yojson 1.4.1 or higher).)
else
AC_MSG_RESULT(found $YOJSON)
fi
#################################################
# Check for other (optional) tools/libraries #
#################################################
new_section "configure optional tools and libraries"
AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,no)
if test "$OCAMLDOC" = no ; then
AC_MSG_RESULT(ocamldoc discarded not present)
else
OCAMLDOC="$OCAMLFIND ocamldoc"
fi
AC_CHECK_PROG(OCAMLMKTOP,ocamlmktop,ocamlmktop,no)
if test "$OCAMLMKTOP" = no ; then
AC_MSG_RESULT(Cannot find ocamlmktop: toplevels cannot be built.)
else
OCAMLMKTOP="$OCAMLFIND ocamlmktop"
fi
AC_CHECK_PROG(OTAGS,otags,otags,)
# apron
########
AC_MSG_CHECKING(for Apron)
APRON_PATH=$($OCAMLFIND query apron 2>/dev/null | tr -d '\r\n')
if test -f "$APRON_PATH/apron.$DYN_SUFFIX"; then
HAS_APRON="yes";
AC_MSG_RESULT(found)else
HAS_APRON="no";
AC_MSG_RESULT(not found. The corresponding domains won't be available in Eva)
fi;
# mpfr
#######
AC_MSG_CHECKING(for MPFR)
MPFR_PATH=$($OCAMLFIND query gmp 2>/dev/null | tr -d '\r\n')
if test -f "$MPFR_PATH/gmp.$DYN_SUFFIX" -a -f "$MPFR_PATH/mpfr.cmx" ; then
HAS_MPFR="yes";
AC_MSG_RESULT(found)
else
HAS_MPFR="no";
AC_MSG_RESULT(not found. The numerors domain won't be available in Eva)
fi;
# landmarks (profiling tool, for developers)
########
AC_ARG_ENABLE(
landmarks,
[ --enable-landmarks enable landmarks profiling (default: yes if package installed)],
ENABLE_LANDMARKS=$enableval,
ENABLE_LANDMARKS=yes)
if test "$ENABLE_LANDMARKS" = yes ; then
AC_MSG_CHECKING(for Landmarks)
LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
HAS_LANDMARKS="yes";
AC_MSG_RESULT(found)
else
HAS_LANDMARKS="no";
AC_MSG_RESULT(not found.)
fi;
else
AC_MSG_RESULT(Landmarks profiling disabled);
HAS_LANDMARKS="no"
fi
############
# Platform #
############
new_section "configure platform"
AC_MSG_CHECKING(platform)
# get Sys.os_type as OCAML_OS_TYPE
echo "let () = print_string Sys.os_type;;" > test_os_type.ml
$OCAMLC -o test_os_type test_os_type.ml
OCAML_OS_TYPE=$(./test_os_type)
rm -f test_os_type.cmi test_os_type.cmo test_os_type.ml test_os_type
if test "$OCAML_OS_TYPE" = "Win32"; then
AC_MSG_RESULT(Win32)
AC_CHECK_PROG(CYGPATH,cygpath,cygpath,no)
PLATFORM=Win32
OCAMLWIN32=yes
EXE=.exe
# OCaml on Win32 does not support vmthreads, use native ones.
HAS_NATIVE_THREADS=yes
else
OCAMLWIN32=no
if test "$OCAML_OS_TYPE" = "Cygwin"; then
AC_MSG_RESULT(Cygwin)
PLATFORM=Cygwin EXE=.exe
else
if test $(uname -s) = "Darwin"; then
AC_MSG_RESULT(MacOS)
PLATFORM=MacOS
else
AC_MSG_RESULT(Unix)
PLATFORM=Unix
fi
EXE=
fi
if test "$OCAMLBEST" = opt; then
# OCaml native threads
AC_MSG_CHECKING([OCaml native threads])
echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
test_native_threads.ml) 2> /dev/null ;
then
HAS_NATIVE_THREADS=yes
AC_MSG_RESULT([ok.]);
else
HAS_NATIVE_THREADS=no
AC_MSG_WARN([unsupported.]);
fi
rm -f test_native_threads*;
else
HAS_NATIVE_THREADS=no; # no native compilation anyway
fi
fi
# C and POSIX standard headers used by C bindings.
AC_LANG([C])
AC_ARG_WITH(cc,[specifies a custom C compiler and pre-processor],[CC=$withval])
AC_PROG_CC
AC_CHECK_HEADERS(stdlib.h)
AC_CHECK_HEADERS(assert.h)
AC_CHECK_HEADERS(float.h)
AC_CHECK_HEADERS(math.h)
AC_CHECK_HEADERS(signal.h)
AC_CHECK_HEADERS(unistd.h)
# Local machdep feature (to generate new platforms)
AC_ARG_ENABLE(
localmachdep,
[ --enable-localmachdep enable local machdep configuration],
LOCAL_MACHDEP=$enableval,
LOCAL_MACHDEP=no)
if test "$LOCAL_MACHDEP" = yes ; then
AC_CONFIG_HEADER(config.h)
AC_CHECK_HEADERS(wchar.h)
# Find out the true definitions of some integer types
# checkIntegerype(size_t) will echo "int" or "long"
checkIntegerType() {
fn="testtype.c"
fo="testtype.o"
for t in "int" "unsigned int" "long" "unsigned long" "short" "unsigned short" "char" "unsigned char" ;do
echo "#include <stddef.h>" >$fn
echo "#include <wchar.h>" >>$fn
# We define a prototype with one type and the function with
# another type. This will result in compilation error
# unless the types are really identical echo "$t foo($t x);" >>$fn
echo "$1 foo($1 x) { return x;}" >>$fn
if gcc -c $fn 2>/dev/null ;then
# Found it
echo $t
rm -f $fn $fo
return
fi
done
rm -f $fn $fo
}
AC_MSG_CHECKING([definition of size_t])
TYPE_SIZE_T=`checkIntegerType "size_t"`
if test "x$TYPE_SIZE_T" = "x" ;then
AC_MSG_ERROR([Cannot find definition of size_t])
fi
AC_DEFINE_UNQUOTED(TYPE_SIZE_T, "$TYPE_SIZE_T")
AC_MSG_RESULT([$TYPE_SIZE_T])
AC_MSG_CHECKING([definition of wchar_t])
TYPE_WCHAR_T=`checkIntegerType "wchar_t"`
if test "x$TYPE_WCHAR_T" = "x" ;then
AC_MSG_ERROR([Cannot find definition of wchar_t])
fi
AC_DEFINE_UNQUOTED(TYPE_WCHAR_T, "$TYPE_WCHAR_T")
AC_MSG_RESULT([$TYPE_WCHAR_T])
AC_MSG_CHECKING([definition of ptrdiff_t])
TYPE_PTRDIFF_T=`checkIntegerType "ptrdiff_t"`
if test "x$TYPE_PTRDIFF_T" = "x" ;then
AC_MSG_ERROR([Cannot find definition of ptrdiff_t])
fi
AC_DEFINE_UNQUOTED(TYPE_PTRDIFF_T, "$TYPE_PTRDIFF_T")
AC_MSG_RESULT([$TYPE_PTRDIFF_T])
AC_MSG_CHECKING([for gcc version])
AC_CHECK_TYPE(__builtin_va_list,
HAVE_BUILTIN_VA_LIST=true,
HAVE_BUILTIN_VA_LIST=false)
if test "$HAVE_BUILTIN_VA_LIST" = "true" ;then
AC_DEFINE_UNQUOTED(HAVE_BUILTIN_VA_LIST, 1)
fi
AC_MSG_CHECKING([if __thread is a keyword])
AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main(int __thread) { return 0; }])],
THREAD_IS_KEYWORD=false,
THREAD_IS_KEYWORD=true)
AC_MSG_RESULT($THREAD_IS_KEYWORD)
if test "$THREAD_IS_KEYWORD" = "true" ;then
AC_DEFINE_UNQUOTED(THREAD_IS_KEYWORD, 1)
fi
# Does gcc add underscores to identifiers to make assembly labels?
# (I think MSVC always does)
AC_MSG_CHECKING([if gcc adds underscores to assembly labels.])
AC_LINK_IFELSE([AC_LANG_SOURCE([int main() { __asm__("jmp _main"); }])],
UNDERSCORE_NAME=true,
UNDERSCORE_NAME=false)
AC_MSG_RESULT($UNDERSCORE_NAME)
if test "$UNDERSCORE_NAME" = "true" ;then
AC_DEFINE_UNQUOTED(UNDERSCORE_NAME, 1)
fi
fi # local machdep configuration
###################################
# Frama-C's pre-processor support #
###################################
# Specific preprocessor support
AC_ARG_WITH(
cpp,
[ --with-cpp customize default preprocessor for Frama-C],
[FRAMAC_DEFAULT_CPP=$withval],
[FRAMAC_DEFAULT_CPP=])
# if no specific pre-processor has been given, check whether we can use
# $CC. Note that we want to keep comments in the output, so that AC_PROG_CPP
# alone is not sufficient.
if test -z "$FRAMAC_DEFAULT_CPP"; then
AC_PROG_CPP
CPPFLAGS="-C -I.";
if test -n "$GCC"; then FRAMAC_GNU_CPP=true; else FRAMAC_GNU_CPP=false; fi
else
CPP=$FRAMAC_DEFAULT_CPP;
FRAMAC_GNU_CPP=true;
CPPFLAGS="-dD -nostdinc"
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([#define foo 0
/* foo */
])],
FRAMAC_GNU_CPP=true,
FRAMAC_GNU_CPP=false)
CPPFLAGS=
fi
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([/* Check whether comments are kept in output */])],
[if test -e conftest.i; then
if grep -e kept conftest.i; then
FRAMAC_DEFAULT_CPP="$CPP $CPPFLAGS";
DEFAULT_CPP_KEEP_COMMENTS=true;
else
AC_MSG_WARN([Default pre-processing command '$CPP' do not preserve
comments. Please define an appropriate pre-processor
with --with-cpp, or you will only be able to use ACSL
annotations in already pre-processed files])
FRAMAC_DEFAULT_CPP=$CPP;
DEFAULT_CPP_KEEP_COMMENTS=false;
fi;
else # handling old version of autoconf (<2.67) that does not keep
# preprocessor result in conftest.i
AC_MSG_WARN([Unable to check whether $CPP preserves comments.
Assuming everything is fine])
FRAMAC_DEFAULT_CPP="$CPP $CPPFLAGS";
DEFAULT_CPP_KEEP_COMMENTS=true;
fi
],
[AC_MSG_WARN([Unable to find a working pre-processor.
Please define one with --with-cpp, or you will be able
to launch Frama-C only on pre-processed files])];
FRAMAC_DEFAULT_CPP="";
DEFAULT_CPP_KEEP_COMMENTS=false;
)
AC_MSG_RESULT(Default preprocessor is '$FRAMAC_DEFAULT_CPP'.)
FRAMAC_DEFAULT_CPP_ARGS=$CPPFLAGS
# Test if preprocessor supports options such as -m16/-m32/-m64
DEFAULT_CPP_SUPPORTED_ARCH_OPTS=
# Store original value of CPPFLAGS before doing tests
OLD_CPPFLAGS=$CPPFLAGS
rm -f conftest.i
CPPFLAGS="$OLD_CPPFLAGS -m32"
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([/* Check if preprocessor supports option -m32 */])], [if test -e conftest.i; then
DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m32\"; ';
fi], [])
rm -f conftest.i
CPPFLAGS="$OLD_CPPFLAGS -m64"
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([/* Check if preprocessor supports option -m64 */])],
[if test -e conftest.i; then
DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m64\"; ';
fi], [])
rm -f conftest.i
CPPFLAGS="$OLD_CPPFLAGS -m16"
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([/* Check if preprocessor supports option -m16 */])],
[if test -e conftest.i; then
DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m16\"; ';
fi], [])
# revert CPPFLAGS to original value
CPPFLAGS=$OLD_CPPFLAGS
AC_MSG_RESULT(Default preprocessor supported architecture-related options: $DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
#################
# Plugin wished #
#################
new_section "wished frama-c plug-ins"
# Option -with-no-plugin
#######################
define([NO_PLUGIN_HELP],
AC_HELP_STRING([--with-no-plugin],
[disable all plug-ins (default: no)]))
AC_ARG_WITH(no-plugin,NO_PLUGIN_HELP,[ONLY_KERNEL=$withval],[ONLY_KERNEL=no])
# library declarations
######################
# REQUIRE_LIBRARY: library *must* be present in order to build plugins
# USE_LIBRARY: better for plugins if library is present, but not required
# HAS_LIBRARY: is the library available?
REQUIRE_LABLGTK=
USE_LABLGTK=
HAS_LABLGTK=
# Tool declarations
####################
DOT=
REQUIRE_DOT=
USE_DOT=
HAS_DOT=
### Now plugin declarations
PLUGINS_FORCE_LIST=
###############################################################################
# #
#################### #
# Plug-in sections # #
#################### #
# ## For 'internal' developers: #
# Add your own plug-in here #
# #
###############################################################################
# callgraph
###########
check_plugin(callgraph, src/plugins/callgraph,
[support for callgraph plugin], yes)
plugin_use_external(callgraph,dot)
plugin_use(callgraph,gui)
plugin_use(callgraph,eva)
# constant propagation
######################
check_plugin(semantic_constant_folding, src/plugins/constant_propagation,
[support for constant propagation plugin],yes)
plugin_require(semantic_constant_folding,eva)
# from
######
check_plugin(from_analysis,src/plugins/from,[support for from analysis],yes)
plugin_require(from_analysis,eva)
plugin_require(from_analysis,callgraph)
# gui
#####
check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk)
plugin_use_external(gui,gnomecanvas)
plugin_require_external(gui,gtksourceview)
plugin_use_external(gui,dot)
# impact
########
check_plugin(impact,src/plugins/impact,[support for impact plugin],yes)
plugin_use(impact,gui)
plugin_use(impact,slicing)
plugin_require(impact,pdg)
plugin_require(impact,eva)
plugin_require(impact,inout)
# inout
#######
check_plugin(inout,src/plugins/inout,[support for inout analysis],yes)
plugin_require(inout,from_analysis)
plugin_require(inout,eva)
plugin_require(inout,callgraph)
# metrics
#########
check_plugin(metrics,src/plugins/metrics,[support for metrics analysis],yes)
plugin_require(metrics,eva)
plugin_use(metrics,gui)
# occurrence
############
check_plugin(occurrence,src/plugins/occurrence,
[support for occurrence analysis],yes)
plugin_use(occurrence,gui)
plugin_require(occurrence,eva)
# pdg
#####
check_plugin(pdg,src/plugins/pdg,[support for pdg plugin],yes,pdg_types)
plugin_require(pdg,from_analysis)
plugin_require(pdg,eva)
plugin_require(pdg,callgraph)
# postdominators
################
check_plugin(postdominators,src/plugins/postdominators,
[support for postdominators plugin],yes)
# rte
#####
check_plugin(rtegen,src/plugins/rte,
[support for runtime error annotation],yes)
# scope
############
check_plugin(scope,src/plugins/scope,[support for scope plugin],yes)
plugin_require(scope,postdominators)
plugin_require(scope,eva)
plugin_require(scope,from_analysis)
plugin_require(scope,pdg)
plugin_use(scope,gui)
# slicing
#########
check_plugin(slicing,src/plugins/slicing,[support for slicing plugin],yes)
plugin_require(slicing,from_analysis)
plugin_require(slicing,pdg)
plugin_require(slicing,eva)
plugin_require(slicing,callgraph)
plugin_use(slicing,gui)
# spare code
############
check_plugin(sparecode,src/plugins/sparecode,
[support for sparecode plugin],yes)
plugin_require(sparecode,pdg)
plugin_require(sparecode,eva)
# users
#######
check_plugin(users,src/plugins/users,[support for users analysis],yes)
plugin_require(users,eva)
plugin_use(users,callgraph)
# value
#######
check_plugin(eva,src/plugins/value,
[support for value analysis],yes)
plugin_use(eva,gui)
plugin_use(eva,scope)
plugin_use(eva,callgraph)
##################### External plugins #
####################
EXTRA_EXTERNAL_PLUGINS=
AC_ARG_ENABLE(external,
[[ --enable-external=plugin
allows to compile directly from Frama-C kernel
some external plug-ins.]],
[
for dir in $enableval; do
if test -d $dir; then
AC_MSG_NOTICE([external plug-in $dir found.])
EXTRA_EXTERNAL_PLUGINS="$EXTRA_EXTERNAL_PLUGINS $dir"
olddir=$(pwd)
cd $dir;
if test -x ./configure; then
new_section "configure plug-in $dir"
./configure --prefix=$prefix --datarootdir=$datarootdir \
--exec_prefix=$exec_prefix --bindir=$bindir --libdir=$datadir/frama-c \
--host=$host --build=$build --mandir=$mandir \
|| \
AC_MSG_ERROR([cannot configure requested external plugin in $dir])
fi;
cd $olddir
else
AC_MSG_ERROR([--enable-external expects an existing directory as argument.])
fi;
done
])
AC_FOREACH([__plugin],m4_esyscmd([ls src/plugins]),
[ m4_if(m4_index(KNOWN_SRC_DIRS,__plugin),[-1],
[
m4_define([plugin_dir],[src/plugins/__plugin])
m4_syscmd(test -r plugin_dir/configure.in)
m4_define([is_configure_in],m4_sysval)
m4_syscmd(test -r plugin_dir/configure.ac)
m4_define([is_configure_ac],m4_sysval)
m4_define([config_file],
[m4_if(is_configure_in,0,plugin_dir/configure.in,
m4_if(is_configure_ac,0,plugin_dir/configure.ac,no))])
m4_if(config_file,[no],
[ m4_syscmd(test -r plugin_dir/Makefile)
m4_if(m4_sysval,[0],
[ m4_syscmd(test "$DISTRIB_CONF" = "yes" && \
grep -q -e "PLUGIN_DISTRIBUTED *:= *no" \
plugin_dir/Makefile
)
m4_if(m4_sysval,[0],,
[ check_plugin(__plugin,plugin_dir,
[support for __plugin plug-in],yes)
if test "$[ENABLE_]tovarname(__plugin)" != "no"; then
EXTERNAL_PLUGINS="$EXTERNAL_PLUGINS plugin_dir";
fi])])],
[ m4_syscmd(test "$DISTRIB_CONF" = "yes" && \
grep -q -e "PLUGIN_DISTRIBUTED:=no" \
plugin_dir/Makefile.in)
m4_if(m4_sysval,[0],,
[ m4_define([plugin_prefix],plugin_dir)
m4_include(config_file)
m4_syscmd(cd plugin_dir && \
[FRAMAC_SHARE]=../../../share autoconf)])
])
m4_undefine([plugin_dir])
])
])
#####################################################
# Check for tools/libraries requirements of plugins ######################################################
new_section "configure tools and libraries used by some plug-ins"
# lablgtk2
##########
define([ENABLE_LABLGTK3_HELP],
AC_HELP_STRING([--disable-lablgtk3],
[in case lablgtk2 and lablgtk3 are available, the default is to compile
against lablgtk3. Use this option to force compiling against lablgtk2]))
AC_ARG_ENABLE(
lablgtk3,[ENABLE_LABLGTK3_HELP],
[ENABLE_LABLGTK3=$enableval],[ENABLE_LABLGTK3=yes])
REQUIRE_LABLGTK="$REQUIRE_LABLGTK$REQUIRE_GNOMECANVAS"
USE_LABLGTK="$USE_LABLGTK$USE_GNOMECANVAS"
LABLGTK_PATH=""
SOURCEVIEW_PATH=""
if test "$PLATFORM" != "MacOS"; then
if test "$ENABLE_LABLGTK3" = "yes"; then
LABLGTK_PATH=`ocamlfind query lablgtk3 | tr -d '\\r\\n'`;
fi
if test "$LABLGTK_PATH" != ""; then
SOURCEVIEW_PATH=`ocamlfind query lablgtk3-sourceview3 | tr -d '\\r\\n'`;
fi
fi
if test "$SOURCEVIEW_PATH" = ""; then
LABLGTK_VERSION=2
LABLGTK_PATH=`ocamlfind query lablgtk2 | tr -d '\\r\\n'`
if test "$LABLGTK_PATH" = "" -o \
"$LABLGTK_PATH" -ef "$OCAMLLIB/lablgtk2" ; then
echo "Ocamlfind -> using +lablgtk2.($LABLGTK_PATH,$OCAMLLIB/lablgtk2)"
LABLGTK_PATH=+lablgtk2
LABLGTKPATH_FOR_CONFIGURE=$OCAMLLIB/lablgtk2
else
echo "Ocamlfind -> using $LABLGTK_PATH"
LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH
fi;
SOURCEVIEW_PATH=$LABLGTKPATH_FOR_CONFIGURE;
else
LABLGTK_VERSION=3
echo "ocamlfind -> using $LABLGTK_PATH"
LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH;
fi
configure_library([GTKSOURCEVIEW],
[$SOURCEVIEW_PATH/lablgtksourceview2.$LIB_SUFFIX,
$SOURCEVIEW_PATH/lablgtk3_sourceview3.$LIB_SUFFIX],
[lablgtksourceview not found],
no)
configure_library([GNOMECANVAS],
[$LABLGTKPATH_FOR_CONFIGURE/lablgnomecanvas.$LIB_SUFFIX],
[lablgnomecanvas.$LIB_SUFFIX not found],
no)
configure_library([LABLGTK],
[$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX,
$LABLGTKPATH_FOR_CONFIGURE/lablgtk3.$LIB_SUFFIX],
[$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.],
no)
# dot and xdot tools
####################
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
# Checking some other things which cannot be done too early
###########################################################
# Native version of ptests can be used only if
# - a native compiler exists
# - native threads are usable
PTESTSBEST=byte
if test \
"$OCAMLBEST" = "opt" -a \
"$HAS_NATIVE_THREADS" = "yes"; \
then
PTESTSBEST=opt;
fi
########################
# Plug-in dependencies #
########################
new_section "checking for plug-in dependencies"
check_frama_c_dependencies
############################
# Substitutions to perform #
############################
EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(DOT)
AC_SUBST(HAS_DOT)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
AC_SUBST(LABLGTK_VERSION)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
AC_SUBST(OCAMLWIN32)
AC_SUBST(OCAML_ANNOT_OPTION)
AC_SUBST(EXE)
AC_SUBST(HAVE_STDLIB_H)
AC_SUBST(HAVE_WCHAR_H)
AC_SUBST(HAVE_PTRDIFF_H)
AC_SUBST(HAVE_BUILTIN_VA_LIST)
AC_SUBST(THREAD_IS_KEYWORD)
AC_SUBST(UNDERSCORE_NAME)
AC_SUBST(CYCLES_PER_USEC)
AC_SUBST(LOCAL_MACHDEP)
AC_SUBST(datarootdir)
AC_SUBST(FRAMAC_DEFAULT_CPP)
AC_SUBST(FRAMAC_DEFAULT_CPP_ARGS)
AC_SUBST(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
AC_SUBST(FRAMAC_GNU_CPP)
AC_SUBST(DEFAULT_CPP_KEEP_COMMENTS)
AC_SUBST(CC)
AC_SUBST(EXTERNAL_PLUGINS)
AC_SUBST(HAS_NATIVE_THREADS)
AC_SUBST(PTESTSBEST)
AC_SUBST(LABLGTK_PATH)
# m4_foreach_w is not supported in some old autoconf versions.# Sadly AC_FOREACH is deprecated now...
AC_FOREACH([p],PLUGINS_LIST,
[AC_SUBST([ENABLE_]p)
])
################################################
# Finally create the Makefile from Makefile.in #
################################################
new_section "creating makefile"
AC_CONFIG_FILES([share/Makefile.config], [chmod a-w share/Makefile.config])
AC_OUTPUT()
###########
# Summary #
###########
new_section "summary: plug-ins available"
for plugin in m4_flatten(PLUGINS_LIST); do
n=NAME_$plugin
e=ENABLE_$plugin
i=INFO_$plugin
eval nv=\$$n
eval ev=\$$e
eval iv=\$$i
AC_MSG_NOTICE([$nv: $ev$iv])
done
if test "$EXTRA_EXTERNAL_PLUGINS" != ""; then
new_section "summary: requested external plugins"
fi
for plugin in $EXTRA_EXTERNAL_PLUGINS; do
AC_MSG_NOTICE([$plugin])
done