diff --git a/.force-reconfigure b/.force-reconfigure
deleted file mode 100644
index 0cfbf08886fca9a91cb753ec8734c84fcbe52c9f..0000000000000000000000000000000000000000
--- a/.force-reconfigure
+++ /dev/null
@@ -1 +0,0 @@
-2
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0b6741c50f8aebed3ed4b794219eb8f0fc1e1f66..b794a61c233bb7528698c4d43c5718c99cdf192f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -185,7 +185,7 @@ build-distrib-tarball:
CI_LINK: "yes"
HDRCK: "frama-c-hdrck"
script:
- - ./nix/shell-checkers.sh "autoconf && ./dev/make-distrib.sh"
+ - ./nix/shell-checkers.sh "./dev/make-distrib.sh"
artifacts:
paths:
- ./*.tar.gz
diff --git a/Makefile b/Makefile
index cffce70db2e63a54d2af53242990e02e811be05f..6701dccd4cb779ae8a2a1992f6e3eaa25515e5a0 100644
--- a/Makefile
+++ b/Makefile
@@ -58,56 +58,12 @@ clean:: purge-tests # to be done before a "dune" command
dune clean
dune clean --root $(FRAMAC_PTESTS_SRC)
dune clean --root $(FRAMAC_HDRCK_SRC)
- rm -rf _build .merlin autom4te.cache
-
-########################################################################
-# Makefile.config is rebuilt whenever configure.ac 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.ac .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
-
+ rm -rf _build .merlin
##############################################################################
# INSTALL/UNINSTALL
################################
-sinclude config.prefix
-FRAMAC_INSTALLDIR?=
-
-INSTALLDIR:=$(FRAMAC_INSTALLDIR)
-
include share/Makefile.installation
###############################################################################
diff --git a/bin/rebuild.sh b/bin/rebuild.sh
index eb1b290bb010d321b63c84774b18b04e4b6d97cb..d0eaab5d035c2584727b2d777172822b0ed5890a 100755
--- a/bin/rebuild.sh
+++ b/bin/rebuild.sh
@@ -21,4 +21,4 @@
# #
##########################################################################
-autoconf -f && ./configure && make -k clean && make -k
+make -k clean && make -k
diff --git a/configure.ac b/configure.ac
deleted file mode 100644
index b633fdeae71dfc33d9872bc9bb09c04b4d507386..0000000000000000000000000000000000000000
--- a/configure.ac
+++ /dev/null
@@ -1,622 +0,0 @@
-##########################################################################
-# #
-# 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"
-# PLATFORM "Win32", "Cygwin", "MacOS" or "Unix"
-# EXE ".exe" if PLATFORM=Win32 (or Cygwin), "" otherwise
-# DLLEXT ".dll" if PLATFORM=Win32 (or Cygwin), ".so" otherwise
-
-AC_INIT
-AC_CONFIG_SRCDIR([src/init/boot/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(quotes not allowed in --prefix argument: $prefix);;
- NONE )
- # no prefix: remove existing config.prefix if any
- rm -f config.prefix
- ;;
- * )
- echo "FRAMAC_INSTALLDIR?=\"$prefix\"" > config.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.*|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(DUNE,dune,dune,no)
-if test "$DUNE" != no ; then
- true
-else
- AC_MSG_ERROR(Cannot find dune.)
-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
-
-
-# landmarks (profiling tool, for developers)
-########
-
-dnl AC_ARG_ENABLE(
-dnl landmarks,
-dnl [ --enable-landmarks enable landmarks profiling (default: yes if package installed)],
-dnl ENABLE_LANDMARKS=$enableval,
-dnl ENABLE_LANDMARKS=yes)
-
-dnl if test "$ENABLE_LANDMARKS" = yes ; then
-dnl AC_MSG_CHECKING(for Landmarks)
-dnl LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
-dnl LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
-dnl if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
-dnl HAS_LANDMARKS="yes";
-dnl AC_MSG_RESULT(found)
-dnl else
-dnl HAS_LANDMARKS="no";
-dnl AC_MSG_RESULT(not found.)
-dnl fi;
-dnl else
-dnl AC_MSG_RESULT(Landmarks profiling disabled);
-dnl HAS_LANDMARKS="no"
-dnl fi
-
-# Python >=3.7 (for analysis-scripts and 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_PYTHON37="no"
-else
- AC_MSG_RESULT(found)
- AC_MSG_CHECKING(for python3 >= 3.7)
- PYTHON3_VERSION=$(echo "$PYTHON3_VERSION" | cut -d' ' -f2-)
- case $PYTHON3_VERSION in
- 2.*|3.[[0-6]].*)
- AC_MSG_RESULT(found $PYTHON3_VERSION (too old); some non-regression tests will be disabled)
- HAS_PYTHON37="no"
- ;;
- *)
- AC_MSG_RESULT(ok)
- HAS_PYTHON37="yes"
- ;;
- esac
-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
- 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_HEADERS([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+='\"-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)
-
-############################
-# Substitutions to perform #
-############################
-
-AC_SUBST(VERBOSEMAKE)
-AC_SUBST(DEVELOPMENT)
-AC_SUBST(HAS_APRON)
-AC_SUBST(HAS_MPFR)
-AC_SUBST(HAS_LANDMARKS)
-AC_SUBST(HAS_PYTHON37)
-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(LABLGTK_PATH)
-
-# used by some share/Makefile.xxx
-AC_SUBST(PLATFORM)
-
-################################################
-# 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
-
-###########
-# Plugins #
-###########
-
-rm -f src/plugins/.disabled
-rm -f src/plugins/dune
-
-m4_foreach_w([__plugin],m4_esyscmd([ls src/plugins]),
- [
- m4_define([plugin_dir],[src/plugins/__plugin])
- m4_syscmd(test -d plugin_dir)
- m4_define([is_plugin],m4_sysval)
- m4_if(is_plugin,0,[
- AC_ARG_ENABLE(
- __plugin,
- AS_HELP_STRING([--disable-__plugin],[Disable __plugin]),
- [ENABLE___plugin=$enableval],
- [ENABLE___plugin=yes]
- )
- if test "$ENABLE___plugin" = no ; then
- echo "__plugin" >> src/plugins/.disabled
- fi
- ],)
- ])
-
-if test -f src/plugins/.disabled ; then
- echo ";; File generated by ./configure --disable-<PLUGIN>" > src/plugins/dune
- echo "(include_subdirs no)" >> src/plugins/dune
- echo ";; Disabled plugin list:" >> src/plugins/dune
- echo "(data_only_dirs $(cat src/plugins/.disabled))" >> src/plugins/dune
- cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "frama-c-configure") (deps (universe)) (action (echo "Disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
- echo ";; Test" >> src/plugins/dune
- echo "(alias (name ptests) (deps (alias ptests_config)))" >> src/plugins/dune
-# "sed -n" is the posix version of "sed --quiet"
- cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "ptests_config") (deps (universe)) (action (echo "Testing with disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
- chmod a-w src/plugins/dune
- rm src/plugins/.disabled
-fi
-
-###########
-# Summary #
-###########
-
-new_section "summary: plug-ins available"
-
-$DUNE build -j1 --display quiet @frama-c-configure
diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh
index 951e0eda0baa2371bafe43be04e85e098896107f..7e2ea1b03670c8637ab6c0743158d6836f9a9168 100755
--- a/dev/make-distrib.sh
+++ b/dev/make-distrib.sh
@@ -23,11 +23,6 @@
set -euxo pipefail
-if [ ! -f configure ] ; then
- echo "No 'configure' file, you should first run 'autoconf'"
- exit 2
-fi
-
################################################################################
# Configuration
@@ -83,7 +78,6 @@ for plugin in $EXTERNAL_PLUGINS ; do
done
tar --concatenate --file=$TAR_ACC
-tar rf $FRAMAC_TAR configure --transform "s,^,$FRAMAC/,"
################################################################################
# Prepare header options
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 038b9f387e886d4aa739a0beb7c83ec5413ac68e..921c8589c6c172eafa302b33922f1a80ce5f7064 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -43,7 +43,9 @@ DEPENDENCIES= $(FRAMAC_MODERN) $(GENERATED) frama-c-book.cls
all: developer.pdf # check << restore check later
-FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
+# This variable does not exist anymore.
+# FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
+# Thus TODO: use `dune exec -- frama-c` for the following commands
.PHONY: clean-tuto
clean-tuto:
diff --git a/ivette/INSTALL.md b/ivette/INSTALL.md
index db3201e0c7c338f327ed8b9001bb608663a7a2ca..3935c806cd5b7f79bcfdd371636d3f683c0fc77d 100644
--- a/ivette/INSTALL.md
+++ b/ivette/INSTALL.md
@@ -43,8 +43,6 @@ command to run the server.
From the `Frama-C` main directory, simply type:
```
-$ autoconf -f
-$ ./configure
$ make -C ivette dist
$ [sudo] make -C ivette install
```
diff --git a/ivette/Makefile b/ivette/Makefile
index b8e494cc10d9ae58881c7d4da2bbdd188f9f1493..b9f07f68e9113757c6607bde8ad46d871707405e 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -159,7 +159,9 @@ include $(DOME)/template/makefile
# --- Ivette Installation
# --------------------------------------------------------------------------
-sinclude ../share/Makefile.config
+INSTALLDIR?=/usr/local
+BINDIR=$(INSTALLDIR)/bin
+LIBDIR=$(INSTALLDIR)/lib
dist-dir:
@echo "Cleaning dist"
diff --git a/nix/api-doc.nix b/nix/api-doc.nix
index d83dd85c02edf0cbc41bfa5d34d1e9b674c2d8aa..d16814551514ad5def3e9b56d4dca0148845e3db 100644
--- a/nix/api-doc.nix
+++ b/nix/api-doc.nix
@@ -20,7 +20,6 @@ stdenv.mkDerivation rec {
preConfigure = frama-c.preConfigure;
buildPhase = ''
- make config.sed
dune build -j1 @doc
cp -r _build/default/_doc/_html frama-c-api
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
index a9716f262e3ca2358d850ac87a35e836ed6fc34b..9ccc398534f01b7848d92fdb420313ba38e8ffc8 100644
--- a/nix/frama-c-checkers-shell.nix
+++ b/nix/frama-c-checkers-shell.nix
@@ -1,6 +1,5 @@
{ lib
, stdenv
-, autoconf
, clang_10
, frama-c-hdrck
, git
@@ -11,7 +10,6 @@
stdenv.mkDerivation rec {
name = "frama-c-checkers-shell";
buildInputs = [
- autoconf
clang_10
frama-c-hdrck
git
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index c82520a4ecf76061f94948c40f3f895795abb009..849a47a825bebbda49835a972ac8b3ce1726f33e 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -8,12 +8,12 @@
, wrapGAppsHook
, writeText
# Generic
-, autoconf
, findlib
# Frama-C build
, apron
, camlzip
, dune_3
+, dune-configurator
, dune-site
, gcc9
, graphviz
@@ -56,7 +56,6 @@ stdenvNoCC.mkDerivation rec {
else gitignoreSource ./.. ;
nativeBuildInputs = [
- autoconf
which
wrapGAppsHook
];
@@ -65,6 +64,7 @@ stdenvNoCC.mkDerivation rec {
apron
camlzip
dune_3
+ dune-configurator
dune-site
findlib
gcc9
@@ -93,9 +93,10 @@ stdenvNoCC.mkDerivation rec {
outputs = [ "out" "build_dir" ];
- preConfigure = (if release_mode then "" else "autoconf \n") + ''
+ preConfigure = ''
patchShebangs src/plugins/eva/gen-api.sh
chmod +x src/plugins/eva/gen-api.sh
+ dune build @frama-c-configure
'';
# Do not use default parallel building, but allow 2 cores for Frama-C build
@@ -103,14 +104,13 @@ stdenvNoCC.mkDerivation rec {
dune_opt = if release_mode then "--release" else "" ;
buildPhase = ''
- make config.sed
dune build -j2 --display short $release_mode @install
make tools/ptests/ptests.exe
make tools/ptests/wtests.exe
'';
installFlags = [
- "FRAMAC_INSTALLDIR=$(out)"
+ "INSTALLDIR=$(out)"
];
# Simpler for our test target
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 46f974137fc5bf1bb35de1fa2129e98979376e2e..7b7da8d89acc3962ecf4a7e2bbb02683fe6d1b00 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -10,12 +10,12 @@
, wrapGAppsHook
, writeText
# Generic
-, autoconf
, findlib
# Frama-C build
, apron
, camlzip
, dune_3
+, dune-configurator
, dune-site
, gcc9
, graphviz
@@ -58,7 +58,6 @@ stdenvNoCC.mkDerivation rec {
src = gitignoreSource ./..;
nativeBuildInputs = [
- autoconf
which
wrapGAppsHook
];
@@ -68,6 +67,7 @@ stdenvNoCC.mkDerivation rec {
alt-ergo
camlzip
dune_3
+ dune-configurator
dune-site
findlib
gcc9
@@ -101,15 +101,14 @@ stdenvNoCC.mkDerivation rec {
outputs = [ "out" ];
preConfigure = ''
- autoconf
patchShebangs src/plugins/eva/gen-api.sh
chmod +x src/plugins/eva/gen-api.sh
+ dune build @frama-c-configure
'';
# Do not use default parallel building, but allow 2 cores for Frama-C build
enableParallelBuilding = false;
buildPhase = ''
- make config.sed
dune build -j2 --display short @install
make tools/ptests/ptests.exe
make tools/ptests/wtests.exe
@@ -134,7 +133,7 @@ stdenvNoCC.mkDerivation rec {
'';
installFlags = [
- "FRAMAC_INSTALLDIR=$(out)"
+ "INSTALLDIR=$(out)"
];
meta = {
diff --git a/nix/src-distrib.nix b/nix/src-distrib.nix
index e675ec74b3f48c42a189464809bf51e65cba1170..053764b047c9969dca16a2dd0b715c3bd300399b 100644
--- a/nix/src-distrib.nix
+++ b/nix/src-distrib.nix
@@ -19,10 +19,6 @@ stdenv.mkDerivation rec {
git
];
- configurePhase = ''
- autoconf
- '';
-
preBuild = ''
patchShebangs ./devel_tools/make-distrib.sh
'';
diff --git a/opam/opam b/opam/opam
index 6d3db50de31befab490b0cc6e95720ab688dfbea..6f16116da6577c2d378aaa2c52a49d4f791eb384 100644
--- a/opam/opam
+++ b/opam/opam
@@ -87,15 +87,12 @@ tags: [
]
build: [
- ["autoconf"] {dev}
- ["./configure" "--prefix" prefix]
- [make "config.sed"]
["dune" "build" "-j%{jobs}%" "--release" "@install"]
[make "-C" "doc" "download"] {with-doc}
]
install: [
- [make "install"]
+ [make "INSTALLDIR=%{prefix}%" "install"]
[make "-C" "doc" "install"] {with-doc}
]
@@ -112,7 +109,6 @@ depends: [
"dune-configurator"
"dune-private-libs"
"dune-site"
- "conf-autoconf" { build }
( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
& ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
| ( "lablgtk3" { >= "3.1.0" & os!="macos" }
diff --git a/share/Makefile.common b/share/Makefile.common
index 604c069a2d101c5e3b26d63abf92927a062fa098..fed4267889d3444317af1daff6330da7f1891d90 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -26,36 +26,18 @@
# #
##########################################################################
-#################
-# Make commands #
-#################
-
-define assert_defined
-ifndef $(1)
-$$(error Undefined variable $(1) please report.)
-endif
-endef
-
-##################################
-# Configure & required variables #
-##################################
-
-$(eval $(call assert_defined,MAKECONFIG_DIR))
-
-include $(MAKECONFIG_DIR)/Makefile.config
-
-#Check share/Makefile.config available
-ifndef FRAMAC_ROOT_SRCDIR
-$(error \
- "You should run ./configure first (or autoconf if there is no configure)")
-endif
+#############
+# Platform #
+#############
-$(eval $(call assert_defined,PLATFORM))
+PLATFORM:=$(shell uname -s)
#############
# Verbosing #
#############
+VERBOSEMAKE?=no
+
ifneq ($(VERBOSEMAKE),no) # Do not change to ifeq ($(VERBOSEMAKE),yes), as this
# version makes it easier for the user to set the
# option on the command-line to investigate
@@ -115,7 +97,7 @@ RM = rm -f
TOUCH = touch
GIT = git
-ifeq ($(PLATFORM),MacOS)
+ifeq ($(PLATFORM),Darwin)
TAR = gtar
else
# Unix, Cygwin, Win32
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
deleted file mode 100644
index e3a8475d0da5176db1dea649cda72fb051e7f28a..0000000000000000000000000000000000000000
--- a/share/Makefile.config.in
+++ /dev/null
@@ -1,89 +0,0 @@
-##########################################################################
-# #
-# 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). #
-# #
-##########################################################################
-
-##########################################################################
-# #
-# Define variables from configure. #
-# These variables may be redefined later. #
-# #
-##########################################################################
-
-######################
-# Installation paths #
-######################
-
-CYGPATH ?=@CYGPATH@
-
-DESTDIR ?=
-prefix ?=@prefix@
-exec_prefix ?=@exec_prefix@
-datarootdir ?=@datarootdir@
-datadir ?=@datadir@
-BINDIR ?=$(DESTDIR)@bindir@
-LIBDIR ?=$(DESTDIR)@libdir@
-DATADIR ?=$(DESTDIR)@datarootdir@
-MANDIR ?=$(DESTDIR)@mandir@
-BASHCOMPDIR ?=$(DESTDIR)@datarootdir@/bash-completion/completions
-
-FRAMAC_LIBDIR ?=$(LIBDIR)/frama-c
-FRAMAC_PLUGINDIR ?=$(FRAMAC_LIBDIR)/plugins
-FRAMAC_DATADIR ?=$(DATADIR)/frama-c
-EMACS_DATADIR ?=$(DATADIR)/emacs/site-lisp
-
-FRAMAC_DEFAULT_CPP ?=@FRAMAC_DEFAULT_CPP@
-FRAMAC_DEFAULT_CPP_ARGS ?= @FRAMAC_DEFAULT_CPP_ARGS@
-FRAMAC_GNU_CPP ?=@FRAMAC_GNU_CPP@
-DEFAULT_CPP_KEEP_COMMENTS?=@DEFAULT_CPP_KEEP_COMMENTS@
-DEFAULT_CPP_SUPPORTED_ARCH_OPTS?=@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@
-
-###########################
-# Miscellaneous variables #
-###########################
-
-# Used by Makefile.common
-PLATFORM ?=@PLATFORM@
-
-# Used by Makefile.common
-VERBOSEMAKE ?=@VERBOSEMAKE@
-
-#######################
-# Working directories #
-#######################
-
-ifeq ($(OCAMLWIN32),yes)
-ifneq ($(CYGPATH),no)
-# Note: using quotes in the line below leads to weird garbled characters
-# in some versions of Cygwin.
-winpath=$(shell $(CYGPATH) -m $(1))
-else
-winpath=$(1)
-endif #CYGPATH
-else
-winpath=$(1)
-endif #OCAMLWIN32
-
-FRAMAC_ROOT_SRCDIR ?= $(call winpath,@abs_top_srcdir@)
-
-##########################################################################
-# Local Variables:
-# mode: makefile
-# End:
diff --git a/share/Makefile.linting b/share/Makefile.linting
index 700afae655885924d84ba20208a9b2aa3b70e1b9..1e987ccaf432d369f153ae209b0a2bc49921bffa 100644
--- a/share/Makefile.linting
+++ b/share/Makefile.linting
@@ -98,7 +98,7 @@ RMDIR ?= rm -rf
TOUCH ?= touch
WC ?= wc
-ifeq ($(PLATFORM),MacOS)
+ifeq ($(PLATFORM),Darwin)
XARGS ?= xargs
else
# Unix, Cygwin
diff --git a/share/Makefile.testing b/share/Makefile.testing
index 2d494fa071655af48c038568e636260ade9b40cb..3569f03d45e3eb5819b961344a60ee4dff7efeac 100644
--- a/share/Makefile.testing
+++ b/share/Makefile.testing
@@ -54,7 +54,7 @@ GREP ?= grep
RM ?= rm -f
RMDIR ?= rm -rf
-ifeq ($(PLATFORM),MacOS)
+ifeq ($(PLATFORM),Darwin)
XARGS ?= xargs
else
# Unix, Cygwin
diff --git a/share/configure.ac b/share/configure.ac
deleted file mode 100644
index 50d76dbe695febe951155ae05840026d98ce4dd2..0000000000000000000000000000000000000000
--- a/share/configure.ac
+++ /dev/null
@@ -1,703 +0,0 @@
-##########################################################################
-# #
-# 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). #
-# #
-##########################################################################
-
-# AC_ARG_WITH(frama-c,
-# AC_HELP_STRING([Frama-C executable name (default is 'frama-c')]),
-# [FRAMA_C=$withval],
-# [FRAMA_C=frama-c])
-
-# AC_ARG_WITH(frama-c-gui,
-# AC_HELP_STRING([Frama-C executable name (default is 'frama-c')]),
-# [FRAMA_C_GUI=$withval],
-# [FRAMA_C_GUI=frama-c-gui])
-
-m4_ifdef([FRAMAC_MAIN_AUTOCONF],,
- [m4_ifdef([plugin_file],
- [AC_INIT(plugin_file)],
- [AC_INIT(aclocal.m4)])
- [KNOWN_PLUGINS=$(frama-c -plugins | \
- sed -e '/\[kernel\]/d' -e 's/\([^ ][^ ]*\( [^ ][^ ]*\)*\) .*/\1/' \
- -e '/^ /d' -e '/^$/d' | \
- tr "a-z- " "A-Z__")
- for plugin in ${KNOWN_PLUGINS}; do
- export $(echo ENABLE_$plugin)=yes
- done
- ]
- AC_SUBST([FRAMAC_VERSION],[`frama-c -version`])
- AC_CHECK_PROG(ENABLE_GUI,[frama-c-gui],[yes],[no])
- ])
-
-m4_define([PLUGIN_RELATIVE_PATH],
- [m4_ifdef([plugin_prefix],plugin_prefix/$1,$1)])
-
-upper() {
- echo "$1" | tr "a-z-" "A-Z_"
-}
-
-lower() {
- echo "$1" | tr "A-Z" "a-z"
-}
-
-m4_define([tovarname],[m4_esyscmd(printf "%s" $1 | tr "a-z-." "A-Z__")])
-
-new_section() {
- banner=`echo "* $1 *" | sed -e 's/./*/g'`
- title=`echo "* $1 *" | tr "a-z" "A-Z"`
- AC_MSG_NOTICE($banner)
- AC_MSG_NOTICE($title)
- AC_MSG_NOTICE($banner)
-}
-
-define([FRAMAC_M4_MACROS])
-
-# sadly, there's no way to define a new diversion beside the internal ones.
-# hoping for the best here...
-m4_define([frama_c_configure_tool],m4_incr(m4_divnum))
-
-m4_define([PLUGINS_LIST],[])
-
-# to distinguish internal plugins, known by the main configure, from
-# purely external plugins living in src/ and compiled together with the main
-# frama-c
-
-define([KNOWN_SRC_DIRS],[])
-
-define([check_plugin],
-[
-define([PLUGIN_NAME],$1)
-define([PLUGIN_FILE],$2)
-define([PLUGIN_MSG],$3)
-define([PLUGIN_DEFAULT],$4)
-define([PLUGIN_ADDITIONAL_DIR],$5)
-AC_CHECK_FILE(PLUGIN_FILE,
- default=PLUGIN_DEFAULT;plugin_present=yes,
- plugin_present=no;default=no)
-
-FORCE=no
-define([PLUGIN_HELP],
- AC_HELP_STRING([--enable-PLUGIN_NAME],
- [PLUGIN_MSG (default: PLUGIN_DEFAULT)]))
-AC_ARG_ENABLE(
- [PLUGIN_NAME],
- PLUGIN_HELP,
- ENABLE=$enableval;FORCE=$enableval,
- ENABLE=$default
-)
-
-if test "$ONLY_KERNEL" = "yes" -a "$FORCE" = "no"; then
- ENABLE=no
-fi
-
-define([KNOWN_SRC_DIRS],KNOWN_SRC_DIRS PLUGIN_FILE PLUGIN_ADDITIONAL_DIR)
-
-if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
- AC_MSG_ERROR([PLUGIN_NAME is not available])
-fi
-define([UP],[tovarname(PLUGIN_NAME)])
-[FORCE_]UP=$FORCE
-PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}" "[FORCE_]UP
-define([PLUGINS_LIST],PLUGINS_LIST UP)
-[ENABLE_]UP=$ENABLE
-[NAME_]UP=PLUGIN_NAME
-if test "$default" = "no" -a "$FORCE" = "no"; then
- [INFO_]UP=" (not available by default)"
-fi
-
-AC_SUBST([ENABLE_]UP)
-echo "PLUGIN_NAME... $ENABLE"
-# kept defined for write_plugin_config. A bit ugly, but not more than
-# usual autoconf stuff.
-# m4_undefine([PLUGIN_NAME])
-m4_undefine([PLUGIN_FILE])
-m4_undefine([PLUGIN_MSG])
-m4_undefine([PLUGIN_DEFAULT])
-m4_undefine([PLUGIN_ADDITIONAL_DIR])
-m4_undefine([UP])
-]) # end of check_plugin
-
-# 1st param: uppercase name of the library
-# 2nd param: file which must exist. This parameter can be a list of files.
-# In this case, they will be tried in turn until one of them exists. The
-# name of the file found will be put in the variable SELECTED_$1
-# 3d param: warning to display if problem
-# 4th param: yes iff checking the library must always to be done
-# (even if there is no plug-in using it)
-m4_define([configure_library],
-[
-# No need to check the same thing multiple times.
- m4_ifdef(SELECTED_$1,,
- [
- m4_define([VAR],[$1])
- m4_define([SELECTED_VAR],[SELECTED_$1])
- m4_define([PROG],[$2])
- m4_define([require],[$REQUIRE_$1])
- m4_define([use],[$USE_$1])
- m4_define([msg],[$3])
- m4_define([has],[HAS_$1])
- m4_define([file],[FILE_$1])
-# [JS 2009/06/02] sh tests and m4 variables do not mix well together.
-# It works by chance but it is not robust enough.
-# Should be rewritten
- has=no
- m4_foreach(file,[PROG],
- [if test "$has" != "yes"; then
- AC_CHECK_FILE(file,has=yes,has=no)
- if test "$has" = "yes"; then SELECTED_VAR=file
- fi
- fi]
- )
- VAR=$SELECTED_VAR
- m4_divert_push(frama_c_configure_tool)
- if test -n "require" -o -n "use" -o "$force_check" = "yes"; then
- if test "$has" = "no"; then
- AC_MSG_WARN([msg])
- reason="PROG missing"
- $5
- for p in require; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval enable_p=\$$ep
- if test "$enable_p" != "no"; then
- fp=FORCE_`upper "$p"`
- if eval test "\$$fp" = "yes"; then
- AC_MSG_ERROR([$p requested but $reason.])
- fi
- eval $ep="no\ \(see\ warning\ about\ PROG\)"
- AC_MSG_WARN([$p disabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- for p in use; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval eep="\$$ep"
- if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
- eval $ep="partial\ \(see\ warning\ about\ PROG\)"
- AC_MSG_WARN([$p partially enabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- fi
- fi
- m4_divert_pop(frama_c_configure_tool)
- AC_SUBST(VAR)
- AC_SUBST(has)
- undefine([SELECTED_VAR])
- undefine([VAR])
- undefine([PROG])
- undefine([require])
- undefine([use])
- undefine([msg])
- undefine([has])
- undefine([file])
- ])
-])
-
-# 1st param: actual name of the ocamlfind package (often lowercase)
-# 2nd param: warning to display if problem
-m4_define([configure_pkg],
-[
-define([PKG_UP],[tovarname($1)])
-m4_ifdef([HAS_OCAML_]PKG_UP,,
- [
- define([VAR],[[OCAML_]PKG_UP])
- define([require],[$[REQUIRE_OCAML_]PKG_UP])
- define([use],[$[USE_OCAML_]PKG_UP])
- define([msg],[$2])
- define([has],[[HAS_OCAML_]PKG_UP])
-
- has=
- AC_MSG_CHECKING(for OCaml package $1)
- VAR=$(ocamlfind query $1 -format %v 2>/dev/null)
- if test -z "$VAR" ; then
- AC_MSG_RESULT(not found via ocamlfind.)
- has=no
- else
- AC_MSG_RESULT(found.)
- has=yes
- fi
- m4_divert_push(frama_c_configure_tool)
- if test -n "require" -o -n "use" -o "$force_check" = "yes"; then
- if test "$has" = "no"; then
- AC_MSG_WARN([msg])
- reason="$1 missing"
- for p in require; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval enable_p=\$$ep
- if test "$enable_p" != "no"; then
- fp=FORCE_`upper "$p"`
- if eval test "\$$fp" = "yes"; then
- AC_MSG_ERROR([$p requested but $reason.])
- fi
- eval $ep="no\ \(see\ warning\ about\ $1\)"
- AC_MSG_WARN([$p disabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- for p in use; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval eep="\$$ep"
- if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
- eval $ep="partial\ \(see\ warning\ about\ $1\)"
- AC_MSG_WARN([$p partially enabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- else
- VAR=PKG_UP
- fi
- fi
- m4_divert_pop(frama_c_configure_tool)
- AC_SUBST(VAR)
- AC_SUBST(has)
- undefine([PKG_UP])
- undefine([VAR])
- undefine([require])
- undefine([use])
- undefine([msg])
- undefine([has])
-])
-])
-
-# 1st param: uppercase name of the program
-# 2nd param: program which must exist. See comment on configure_library()
-# on how to deal with multiple choices for a given program.
-# 3d param: warning to display if problem
-# 4th param: yes iff checking the tool must always to be done
-# (even if there is no plug-in using it)
-m4_define([configure_tool],
-[
-m4_ifdef(HAS_$1,,
- [
- define([VAR],[$1])
- define([PROG],[$2])
- define([require],[$REQUIRE_$1])
- define([use],[$USE_$1])
- define([msg],[$3])
- define([has],[HAS_$1])
- define([force_check],[$4])
-
- for file in PROG; do
- has=
-AC_CHECK_PROG(has,$file,yes,no)
- if test "$has" = "yes"; then SELECTED_VAR=$file break; fi
- done
- m4_divert_push(frama_c_configure_tool)
- if test -n "require" -o -n "use" -o "$force_check" = "yes"; then
- if test "$has" = "no"; then
- AC_MSG_WARN([msg])
- reason="PROG missing"
- for p in require; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval enable_p=\$$ep
- if test "$enable_p" != "no"; then
- fp=FORCE_`upper "$p"`
- if eval test "\$$fp" = "yes"; then
- AC_MSG_ERROR([$p requested but $reason.])
- fi
- eval $ep="no\ \(see\ warning\ about\ PROG\)"
- AC_MSG_WARN([$p disabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- for p in use; do
- up=`upper "$p"`
- ep=ENABLE_$up
- eval eep="\$$ep"
- if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
- eval $ep="partial\ \(see\ warning\ about\ PROG\)"
- AC_MSG_WARN([$p partially enabled because $reason.])
- eval INFO_$up=\", $reason\"
- fi
- done
- else
- VAR=PROG
- fi
- fi
- m4_divert_pop(frama_c_configure_tool)
- AC_SUBST(VAR)
- AC_SUBST(has)
- undefine([VAR])
- undefine([PROG])
- undefine([require])
- undefine([use])
- undefine([msg])
- undefine([has])
-])
-])
-
-
-EXTERNAL_PLUGINS=
-
-define([plugin_require_external],
- [m4_define([UPORIG],tovarname($2))
- m4_define([REQUIRE],[REQUIRE_]UPORIG)
- REQUIRE=$REQUIRE" "$1
- m4_undefine([REQUIRE])
- m4_undefine([UPORIG])])
-
-define([plugin_use_external],
- [m4_define([UPORIG],tovarname($2))
- m4_define([USE],[USE_]UPORIG)
- USE=$USE" "$1
- m4_undefine([USE])
- m4_undefine([UPORIG])])
-
-define([plugin_require_pkg],
- [m4_define([UPORIG],[OCAML_]tovarname($2))
- m4_define([REQUIRE],[REQUIRE_]UPORIG)
- REQUIRE=$REQUIRE" "$1
- m4_undefine([REQUIRE])
- m4_undefine([UPORIG])])
-
-define([plugin_use_pkg],
- [m4_define([UPORIG],[OCAML_]tovarname($2))
- m4_define([USE],[USE_]UPORIG)
- USE=$USE" "$1
- m4_undefine([USE])
- m4_undefine([UPORIG])])
-
-define([plugin_require],
- [m4_define([UPTARGET],tovarname($1))
- m4_define([UPORIG],tovarname($2))
- m4_define([REQUIRE],[REQUIRE_]UPORIG)
- m4_define([REQUIRED],[REQUIRED_]UPTARGET)
- REQUIRE=$REQUIRE" "$1
- REQUIRED=$REQUIRED" "$2
- m4_undefine([UPTARGET])
- m4_undefine([UPORIG])
- m4_undefine([REQUIRE])
- m4_undefine([REQUIRED])
- ])
-
-define([plugin_use],
- [m4_define([UPTARGET],tovarname($1))
- m4_define([UPORIG],tovarname($2))
- m4_define([USE],[USE_]UPORIG)
- m4_define([USED],[USED_]UPTARGET)
- USE=$USE" "$1
- USED=$USED" "$2
- m4_undefine([UPTARGET])
- m4_undefine([UPORIG])
- m4_undefine([USE])
- m4_undefine([USED])
- ])
-
-# Usage: plugin_disable([plugin],[reason])
-define([plugin_disable],
- [m4_define([PLUGIN_NAME],$1)
- m4_define([MSG],$2)
- m4_define([UP],[tovarname(PLUGIN_NAME)])
- if test "[FORCE_]UP" = "yes"; then
- AC_MSG_ERROR([PLUGIN_NAME requested but MSG]);
- else
- AC_MSG_WARN([PLUGIN_NAME disabled because MSG]);
- [ENABLE_]UP=no;
- [INFO_]UP=", MSG"
- fi])
-
-define([has_pushed],0)
-define([after_plugin_dependencies],[
- define([has_pushed],1)
- m4_divert_push(frama_c_configure_tool)])
-define([end_after_plugin_dependencies],[
- m4_if(has_pushed,1,
- [m4_divert_pop(frama_c_configure_tool)]
- m4_define([has_pushed],0)
- )])
-# Implementation of an ordering $1 < $2: "" < yes < partial < no
-lt_mark () {
- first=`echo "$1" | sed -e 's/ .*//' `
- second=`echo "$2" | sed -e 's/ .*//' `
- case $first in
- "") echo "true";;
- "yes"*)
- case $second in
- "yes") echo "";;
- "partial" | "no") echo "true";;
- esac;;
- "partial"*)
- case $second in
- "yes" | "partial") echo "";;
- "no") echo "true";;
- esac;;
- "no"*) echo "";;
- esac
-}
-
-# Check and propagate marks to requires and users.
-# $1: parent plugin
-# $2: mark to propagate to requires
-# $3: mark to propagate to users
-check_and_propagate () {
- # for each requires
- r=REQUIRE_$1
- eval require="\$$r"
- for p in $require; do
- up=`upper "$p"`
- m=MARK_"$up"
- eval mark="\$$m"
- if test -z "$mark"; then
- m=ENABLE_"$up"
- eval mark="\$$m"
- fi
- if test `lt_mark "$mark" "$2" `; then
- # update marks
- eval MARK_$up=\"$2\";
- TODOLIST=$TODOLIST" "$p
- # display a warning or an error if required
- short_mark=`echo $2 | sed -e 's/ .*//'`
- lp=`lower $p`
- reason=`echo $2 | sed -e 's/no (\(.*\))/\1/' `
- if test "$short_mark" = "no"; then
- fp=FORCE_"$up"
- if eval test "\$$fp" = "yes"; then
- AC_MSG_ERROR([$lp requested but $reason.])
- else
- AC_MSG_WARN([$lp disabled because $reason.])
- fi
- else
- if test "$short_mark" = "partial"; then
- reason=`echo $2 | sed -e 's/partial (\(.*\))/\1/' `
- AC_MSG_WARN([$lp only partially enable because $reason.])
- fi
- fi
- eval INFO_$up=\", $reason\"
- fi
- done
- # for each users
- u=USE_$1
- eval use="\$$u"
- for p in $use; do
- up=`upper "$p"`
- m=MARK_$up
- eval mark="\$$m"
- if test -z "$mark"; then
- m=ENABLE_"$up"
- eval mark="\$$m"
- fi
- if test `lt_mark "$mark" "$3" `; then
- # update marks
- eval MARK_$up=\"$3\";
- TODOLIST=$TODOLIST" "$p
- # display a warning if required
- lp=`lower $p`
- reason=`echo $3 | sed -e 's/partial (\(.*\))/\1/' `
- if test "$reason" != "$3"; then
- AC_MSG_WARN([$lp only partially enabled because $reason.])
- fi
- eval INFO_$up=\", $reason\"
- fi
- done
-}
-
-# checks direct dependencies of a plugin. Useful for dynamic plugins which
-# have a dependency toward already installed (or not) plug-ins, since the old
-# plugins are not in the TODO list from the beginning (and need not their
-# mutual dependencies be rechecked anyway
-check_required_used () {
- ep=ENABLE_$1
- eval enabled=\$$ep
-
- if test "$enabled" != "no"; then
-
- r=REQUIRED_$1
- u=USED_$1
- m=MARK_$1
- eval required=\$$r
- eval used=\$$u
- eval $m=yes
-
- reason=
-
- for p in $required; do
- up=`upper $p`
- ec=ENABLE_$up
- eval enabled=\$$ec
- case `echo "$enabled" | sed -e 's/ .*//'` in
- "") reason="$p unknown";;
- "yes" | "partial");;
- "no") reason="$p not enabled";;
- esac
- done
- if test -n "$reason"; then
- eval $m=\"no\ \($reason\)\"
- p_name=`lower $1`
- AC_MSG_WARN([$p_name disabled because $reason.])
- eval INFO_$1=\", $reason\"
- else
- for p in $used; do
- up=`upper $p`
- ec=ENABLE_$up
- eval enabled=\$$ec
- case `echo "$enabled" | sed -e 's/ .*//'` in
- "") reason="$p unknown";;
- "yes" | "partial");;
- "no") reason="$p not enabled";;
- esac
- done
- if test -n "$reason"; then
- eval $m=\"partial\ \($reason\)\"
- p_name=`lower $1`
- AC_MSG_WARN([$p_name partially enabled because $reason.])
- eval INFO_$1=\", $reason\"
- fi
- fi
-
- else # $enabled = "no"
- eval $m=\"no\"
- fi
-}
-
-# Recursively check the plug-in dependencies using the plug-in dependency graph
-compute_dependency () {
- plugin=`echo $TODOLIST | sed -e 's/ .*//' `
- TODOLIST=`echo $TODOLIST | sed -e 's/[[^ ]]* *\(.*\)/\1/' `
-
- lplugin=`lower "$plugin"`
- uplugin=`upper "$plugin"`
- # new mark to consider
- m=MARK_$uplugin
- eval mark="\$$m"
- # old mark to consider
- r=REMEMBER_$uplugin
- eval remember="\$$r"
- # the exact mark (final result),
- # also the old mark if plugin already visited
- e=ENABLE_$uplugin
- eval enable="\$$e"
- #first visit. Performs additional checks over requirements.
- if test -z "$mark"; then
- check_required_used "$uplugin";
- eval mark=\$$m
- fi
-
-# echo "plug-in $lplugin (mark=$mark, remember=$remember, enable=$enable)"
- if test `lt_mark "$remember" "$mark"`; then
- # visit the current plugin:
- # mark <- max(mark, enable)
- case `echo "$mark" | sed -e 's/ .*//' ` in
- "") echo "problem?"; exit 3;;
- "yes")
- if test -n "$enable"; then mark="$enable"; else mark="yes"; fi;;
- "partial") if test "$enable" = "no"; then mark="no"; fi;;
- "no") ;;
- esac
- # update plug-in attributes with the new mark
-# echo "update attributes with $mark"
- eval $m=\"$mark\"
- eval $e=\"`echo "$mark" | sed -e 's/ .*//' `\"
- enable="$mark"
- eval $r=\"$mark\"
- # compute and propagate a new mark to requires and users
- case `echo "$enable" | sed -e 's/ .*//' ` in
- "") echo "problem?"; exit 3;;
- "yes") check_and_propagate $uplugin "yes" "yes";;
- "partial")
-# if a plug-in is partial, does not consider its dependencies as partial
-# so the second argument is "yes" and not "partial"
- check_and_propagate \
- "$uplugin" \
- "yes" \
- "yes";;
- "no")
- check_and_propagate \
- "$uplugin" \
- "no ($lplugin not enabled)" \
- "partial ($lplugin not enabled)";;
- esac
- fi
- # recursively consider the next plugins
- if test -n "$TODOLIST"; then
- compute_dependency;
- fi
-}
-
-define([compute_plugin_dependencies],
-[
-# First, initialize some variables
-for fp in ${PLUGINS_FORCE_LIST}; do
- if test "$fp" != "FORCE_GTKSOURCEVIEW"; then
- plugin=`echo $fp | sed -e "s/FORCE_\(.*\)/\1/" `
- TODOLIST=$TODOLIST" "$plugin
- eval MARK_$plugin=
- eval REMEMBER_$plugin=
- fi
-done
-# main call
-compute_dependency
-])
-
-define([check_frama_c_dependencies],
- [m4_undivert(frama_c_configure_tool)
- compute_plugin_dependencies])
-
-define([check_plugin_dependencies],
- [m4_ifdef([FRAMAC_MAIN_AUTOCONF],
- [after_plugin_dependencies],
- [m4_undivert(frama_c_configure_tool)
- compute_plugin_dependencies])])
-
-define([write_plugin_summary],
-[
- m4_ifdef([FRAMAC_MAIN_AUTOCONF],,
- [
-# Compute INFO_* and exported ENABLE_* from previously computed ENABLE_*
- for fp in ${PLUGINS_FORCE_LIST}; do
- if test "$fp" != "FORCE_GTKSOURCEVIEW"; then
- plugin=`echo $fp | sed -e "s/FORCE_\(.*\)/\1/" `
- ep=ENABLE_$plugin
- eval v=\$$ep
- eval ep_v=`echo $v | sed -e 's/ .*//' `
- eval ENABLE_$plugin=$ep_v
- reason=`echo $v | sed -e 's/[[a-z]]*\( .*\)/\1/' `
- n=NAME_$plugin
- eval name=\$$n
- info=
- if test "$reason" != "$ep_v"; then
- info=$reason
- fi
- AC_MSG_NOTICE([$name: $ep_v$info])
- fi
- done])])
-
-define([write_plugin_config],
- [m4_ifndef([plugin_prefix],[define([plugin_prefix],[.])])
- m4_define([plugin_files],
- AC_FOREACH([plugin_file],$1,[plugin_prefix/plugin_file ]))
- m4_define([files_chmod],
- AC_FOREACH([plugin_file],plugin_files,[chmod -w plugin_file]))
- AC_CONFIG_FILES(plugin_files,files_chmod)
- m4_ifdef(
- [FRAMAC_MAIN_AUTOCONF],
- [end_after_plugin_dependencies]
- if test "$[ENABLE_]tovarname(PLUGIN_NAME)" != "no"; then
- [EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} plugin_prefix"];
- fi,
- [
- write_plugin_summary
- AC_OUTPUT()
- ])
- ])