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