-
Patrick Baudin authoredPatrick Baudin authored
configure.in 32.24 KiB
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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
# DLLEXT ".dll" if OCAMLWIN32=yes, ".so" 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 4
then
AC_MSG_ERROR([unsupported version; GNU Make version 4.0
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 and build directory #
##############################################################
case $prefix in
*\ * ) AC_MSG_ERROR(spaces not allowed in --prefix argument "$prefix");;
* ) ;;
esac
case $(pwd) in
*\ * ) AC_MSG_ERROR(spaces not allowed in build directory "$(pwd)");;
*\'* ) AC_MSG_ERROR(single quotes not allowed in build directory "$(pwd)");;
*\"* ) AC_MSG_ERROR(double quotes not allowed in build directory "$(pwd)");;
* ) ;;
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.*|4.05.*|4.06.*|4.07.*|4.08.0)
AC_MSG_ERROR(Incompatible OCaml version; use 4.08.1+.);;
*)
OCAML_ANNOT_OPTION="-bin-annot";;
esac
AC_SUBST(OCAMLMAJORNB)
AC_SUBST(OCAMLMINORNB)
AC_SUBST(OCAMLPATCHNB)
AC_SUBST(HAS_OCAML409)
AC_SUBST(HAS_OCAML410)
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_OCAML409=yes;
HAS_OCAML410=yes;
else
HAS_OCAML409=no;
HAS_OCAML410=no;
if test $OCAMLMINORNB -ge 9; then HAS_OCAML409=yes;
fi;
if test $OCAMLMINORNB -ge 10; then
HAS_OCAML410=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).)
fi
AC_SUBST(HAS_OCAMLGRAPH_2)
HAS_OCAMLGRAPH_2=no
case $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|1.8.8)
AC_MSG_RESULT(found);;
2.0.*)
HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found);;
*)
HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found $OCAMLGRAPH: should work, but is not tested);;
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 (requires zarith 1.5 or higher).)
fi
case ZARITH in
1.[[01234]].*)
AC_MSG_ERROR(found $ZARITH: requires 1.5 or higher.);;
*)
AC_MSG_RESULT(found $ZARITH);;
esac
# 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 and Landmarks-ppx)
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
# Python 3 (for analysis-scripts, and for several tests: compliance, jcdb, ...)
########
AC_MSG_CHECKING(for python3)
PYTHON3_VERSION=$(python3 --version 2>/dev/null || echo "")
if test -z "$PYTHON3_VERSION" ; then AC_MSG_RESULT(not found. Some non-regression tests will be disabled.)
HAS_PYTHON36="no"
else
AC_MSG_RESULT(found)
AC_MSG_CHECKING(for python3 >= 3.6)
PYTHON3_VERSION=$(echo "$PYTHON3_VERSION" | cut -d' ' -f2-)
case $PYTHON3_VERSION in
2.*|3.[[0-5]].*)
AC_MSG_RESULT(found $PYTHON3_VERSION (too old); some non-regression tests will be disabled)
HAS_PYTHON36="no"
;;
*)
AC_MSG_RESULT(ok)
HAS_PYTHON36="yes"
;;
esac
fi
plugin_use_external(tests,python3)
############
# 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
DLLEXT=.dll
else
OCAMLWIN32=no
if test "$OCAML_OS_TYPE" = "Cygwin"; then
AC_MSG_WARN([Compilation using Cygwin is unsupported;
consider using a MinGW-based compiler.])
AC_MSG_RESULT(Cygwin)
PLATFORM=Cygwin
EXE=.exe
DLLEXT=.dll
else
if test $(uname -s) = "Darwin"; then
AC_MSG_RESULT(MacOS)
PLATFORM=MacOS
else
AC_MSG_RESULT(Unix)
PLATFORM=Unix
fi
EXE=
DLLEXT=.so
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
# 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="$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="$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="$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=
### 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)
plugin_require(from_analysis,postdominators)
# gui
#####
check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk)
# in ocamlgraph 2, the gtk part is separated. Hence if we found it,
# there's no need to check specifically for gnomecanvas
if test "$HAS_OCAMLGRAPH_2" = "yes"; then
plugin_use_external(gui,ocaml_ocamlgraph_gtk)
else
plugin_use_external(gui,gnomecanvas)
fi
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_require(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,server)
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)
# reduc
############
check_plugin(reduc,src/plugins/reduc,[support for reduc plugin],yes)
plugin_require(reduc,eva)
plugin_require(reduc,inout)
# 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_require(slicing,sparecode)
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)
plugin_require(sparecode,users)
# users
#######
check_plugin(users,src/plugins/users,[support for users analysis],yes)
plugin_require(users,eva)
plugin_require(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,inout)
plugin_use(eva,callgraph)
plugin_require(eva,server)
####################
# 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_bregexp(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)
if test "$HAS_OCAMLGRAPH_2" = yes; then
configure_pkg([ocamlgraph_gtk],[package ocamlgraph_gtk not found])
fi
# dot and xdot tools
####################
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
configure_tool([UNIX2DOS],[unix2dos],
[unix2dos not found: you should install dos2unix],no)
plugin_use_external(tests,unix2dos)
########################
# Plug-in dependencies #
########################
new_section "checking for plug-in dependencies"
check_frama_c_dependencies
AC_SUBST(HAS_DGRAPH)
if test "$HAS_OCAMLGRAPH_2" = "yes"; then
HAS_DGRAPH=$HAS_OCAML_OCAMLGRAPH_GTK;
else
HAS_DGRAPH=$HAS_GNOMECANVAS
fi
############################
# Substitutions to perform #
############################
EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)AC_SUBST(HAS_LANDMARKS)
AC_SUBST(HAS_PYTHON36)
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(DLLEXT)
AC_SUBST(HAVE_STDLIB_H)
AC_SUBST(HAVE_WCHAR_H)
AC_SUBST(HAVE_PTRDIFF_H)
AC_SUBST(HAVE_BUILTIN_VA_LIST)
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(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