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..4604ae0ffc7bffba26ec3a103e671ac72c2047e8 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
@@ -279,6 +279,7 @@ ocaml-versions-nightly:
stage: compatibility
image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
script:
+ - sudo apt update
- opam pin . -n
- opam depext frama-c --with-test
- opam install --jobs 2 frama-c --with-test
@@ -295,7 +296,6 @@ opam-pin-nightly:
<<: *opam_template
only:
- schedules
- allow_failure: true
# TODO: Enable this rule later:
#
diff --git a/Makefile b/Makefile
index 85eb31106625444dffc3080f24e2d7df7ef2d61e..fbfcdce80f735d1a3daedccb8e986ec0e4778a98 100644
--- a/Makefile
+++ b/Makefile
@@ -26,6 +26,10 @@ MAKECONFIG_DIR=share
include share/Makefile.common
+##############################################################################
+# DUNE OPTIONS
+################################
+
DUNE_BUILD_OPTS?=
RELEASE?=no
@@ -39,95 +43,53 @@ endif
DUNE_DISPLAY?=progress
DUNE_BUILD_OPTS+=--display $(DUNE_DISPLAY)
+##############################################################################
# PTESTS SRC
+################################
+
FRAMAC_PTESTS_SRC:=tools/ptests
+##############################################################################
# HDRCK SRC
-FRAMAC_HDRCK_SRC:=tools/hdrck
+################################
-###################
-# Frama-C Version #
-###################
+FRAMAC_HDRCK_SRC:=tools/hdrck
-VERSION:=$(shell $(CAT) VERSION)
-VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME)
+##############################################################################
+# Frama-C
+################################
.PHONY: all
-all: config.sed
+all:
+ifneq ($(DISABLED_PLUGINS),)
+ dune clean
+ rm -rf _build .merlin
+ ./dev/disable-plugins.sh ${DISABLED_PLUGINS}
+endif
dune build $(DUNE_BUILD_OPTS) @install
-MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION)
-MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION)
-VERSION_CODENAME=$(shell $(CAT) VERSION_CODENAME)
-
-# File used by dune to build src/kernel_internals/runtime/fc_config.ml
-config.sed: VERSION share/Makefile.config share/Makefile.common Makefile configure.ac
- @echo "# generated file" > $@
- @echo "s|@VERSION@|$(VERSION)|" >> $@
- @echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@
- @echo "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|g" >> $@
- @echo "s|@MINOR_VERSION@|$(MINOR_VERSION)|g" >> $@
- @echo "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" >> $@
- @echo "s|@FRAMAC_DEFAULT_CPP_ARGS@|$(FRAMAC_DEFAULT_CPP_ARGS)|" >> $@
- @echo "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" >> $@
- @echo "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" >> $@
- @echo "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" >> $@
-
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 config.sed 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
+ rm -rf _build .merlin
-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
+##############################################################################
+# HELP
+################################
+help::
+ @echo "Build configuration variables"
+ @echo " - RELEASE: compile in release mode if set to 'yes'"
+ @echo " - DUNE_DISPLAY: parameter transmitted to dune --display option"
+ @echo " - DISABLED_PLUGINS: disable these plugins before (re)building"
+ @echo " (none for enabling all plugins)"
##############################################################################
# INSTALL/UNINSTALL
################################
-sinclude config.prefix
-FRAMAC_INSTALLDIR?=
-
-INSTALLDIR:=$(FRAMAC_INSTALLDIR)
-
include share/Makefile.installation
###############################################################################
@@ -153,12 +115,9 @@ FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
# Frama-C also have ptest directories in plugins, so we do not use default
PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests)
-# Test aliasing definition allowing ./configure --disable-<plugin>
+# Test aliasing definition allowing ./configure --disable-<plugin>
PTEST_ALIASES:=@tests/ptests @src/plugins/ptests
-# Ptests needs config.sed so that dune can build Frama-C (if it is not built)
-PTEST_DEPS:=config.sed
-
# WP tests need WP cache
PTEST_USE_WP_CACHE:=yes
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/configurator.ml b/configurator.ml
new file mode 100644
index 0000000000000000000000000000000000000000..69511aec6c76b662162cb8890094a81437852223
--- /dev/null
+++ b/configurator.ml
@@ -0,0 +1,268 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module C = Configurator.V1
+
+module Temp = struct (* Almost copied from configurator *)
+ let (^/) a b = a ^ "/" ^ b
+
+ let rec rm_rf dir =
+ Array.iter (fun fn ->
+ let fn = dir ^/ fn in
+ if Sys.is_directory fn then rm_rf fn else Unix.unlink fn)
+ (Sys.readdir dir);
+ Unix.rmdir dir
+
+ let prng = lazy (Random.State.make_self_init ())
+
+ let gen_name ~dir ~prefix ~suffix =
+ let rnd = Random.State.bits (Lazy.force prng) land 0xFFFFFF in
+ dir ^/ Printf.sprintf "%s%06x%s" prefix rnd suffix
+
+ let create_dir () =
+ let dir =
+ gen_name ~dir:(Filename.get_temp_dir_name ()) ~prefix:"" ~suffix:"" in
+ Unix.mkdir dir 0o700 ;
+ at_exit (fun () -> rm_rf dir) ;
+ dir
+
+ let create ?(dir=create_dir ()) ?(prefix="") ?(suffix="") mk =
+ let rec try_name counter =
+ let name = gen_name ~dir ~prefix ~suffix in
+ match mk name with
+ | () -> name
+ | exception Unix.Unix_error _ when counter < 1000 -> try_name (counter + 1)
+ in
+ try_name 0
+end
+
+module C_compiler = struct (* This could be put in Dune? *)
+ type t =
+ { compiler: string
+ ; is_gnu: bool
+ }
+
+ let find_compiler configurator =
+ let cc_env = try Sys.getenv "CC" with Not_found -> "" in
+ if cc_env <> "" then cc_env
+ else
+ let finder compiler = C.which configurator compiler |> Option.is_some in
+ try List.find finder [ "gcc"; "cc"; "cl.exe" ]
+ with Not_found -> C.die "Could not find a C compiler"
+
+ let write_file name code =
+ let out = open_out name in
+ Printf.fprintf out "%s" code ;
+ close_out out
+
+ let call configurator compiler options code =
+ let dir = Temp.create_dir () in
+ let file =
+ Temp.create ~dir ~suffix:".c" (fun name -> write_file name code) in
+ C.Process.run configurator ~dir compiler (options @ [ file ])
+
+
+ let preprocess_flag = "-E"
+
+ let is_gnu configurator compiler =
+ let code = {|#ifndef __GNUC__
+ this is not a gnuc compiler
+#endif
+|}
+ in
+ (call configurator compiler ["-c"] code).exit_code = 0
+
+ let get configurator =
+ let compiler = find_compiler configurator in
+ let is_gnu = is_gnu configurator compiler in
+ { compiler ; is_gnu }
+
+ let preprocess configurator t options =
+ call configurator t.compiler (preprocess_flag :: options)
+
+ let _compile configurator t options =
+ call configurator t.compiler ("-c" :: options)
+end
+
+(* Frama-C specific part *)
+
+module Cpp = struct
+ module GnuLike = struct
+ let code = {|
+#define foo 0
+/* foo */
+int main(){}
+|}
+
+ let check configurator compiler =
+ let options = ["-dD" ; "-nostdinc"] in
+ (C_compiler.preprocess configurator compiler options code).exit_code = 0
+ end
+
+ module KeepComments = struct
+ let code =
+ {|/* Check whether comments are kept in output */|}
+
+ let check configurator compiler options =
+ let result = C_compiler.preprocess configurator compiler options code in
+ result.exit_code = 0 &&
+ let re = Str.regexp_string "kept" in
+ try ignore (Str.search_forward re result.stdout 0); true
+ with Not_found -> false
+ end
+
+ module Archs = struct
+ let opt_m_code value =
+ Format.asprintf {|/* Check if preprocessor supports option -m%s */|} value
+
+ let check configurator compiler arch =
+ let code = opt_m_code arch in
+ let options = [ Format.asprintf "-m%s" arch ] in
+ if (C_compiler.preprocess configurator compiler options code).exit_code = 0
+ then Some arch else None
+
+ let supported_archs configurator compiler archs =
+ let check = check configurator compiler in
+ List.map (fun s -> "-m" ^ s) @@ List.filter_map check archs
+ end
+
+ type t =
+ { compiler : C_compiler.t
+ ; default_args : string list
+ ; is_gnu_like : bool
+ ; keep_comments : bool
+ ; supported_archs_opts : string list
+ }
+
+ let get configurator =
+ let compiler = C_compiler.get configurator in
+ let default_args = [ "-C" ; "-I." ] in
+ let is_gnu_like = GnuLike.check configurator compiler in
+ let keep_comments = KeepComments.check configurator compiler [ "-C" ] in
+ let supported_archs_opts =
+ Archs.supported_archs configurator compiler [ "16" ; "32" ; "64" ] in
+ { compiler; default_args; is_gnu_like; keep_comments; supported_archs_opts }
+
+ let pp_flags fmt =
+ let pp_sep fmt () = Format.fprintf fmt " " in
+ Format.pp_print_list ~pp_sep Format.pp_print_string fmt
+
+ let pp_default_cpp fmt cpp =
+ Format.fprintf fmt "%s %a"
+ cpp.compiler.compiler
+ pp_flags (C_compiler.preprocess_flag :: cpp.default_args)
+
+ let pp_archs fmt cpp =
+ let pp_arch fmt arch = Format.fprintf fmt "\"%s\"" arch in
+ let pp_sep fmt () = Format.fprintf fmt "; " in
+ Format.fprintf fmt
+ "%a" (Format.pp_print_list ~pp_sep pp_arch) cpp.supported_archs_opts
+
+ let pp_sed fmt cpp =
+ Format.fprintf fmt
+ "s|@FRAMAC_DEFAULT_CPP@|%a|\n" pp_default_cpp cpp ;
+ Format.fprintf fmt
+ "s|@FRAMAC_DEFAULT_CPP_ARGS@|%a|\n" pp_flags cpp.default_args ;
+ Format.fprintf fmt
+ "s|@FRAMAC_GNU_CPP@|%b|\n" cpp.is_gnu_like ;
+ Format.fprintf fmt
+ "s|@DEFAULT_CPP_KEEP_COMMENTS@|%b|\n" cpp.keep_comments ;
+ Format.fprintf fmt
+ "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|%a|" pp_archs cpp
+end
+
+module Fc_version = struct
+ type t =
+ { major: string
+ ; minor: string
+ ; ext: string
+ ; name: string
+ }
+
+ let get configurator =
+ let out_VERSION =
+ let out = C.Process.run configurator "cat" ["VERSION"] in
+ if out.exit_code <> 0 then C.die "Can't read VERSION." ;
+ out.stdout
+ in
+ let re_version =
+ Str.regexp {|\([1-9][0-9]\)\.\([0-9]\)\(.*\)|}
+ in
+ let major, minor, ext =
+ if Str.string_match re_version out_VERSION 0 then
+ Str.matched_group 1 out_VERSION,
+ Str.matched_group 2 out_VERSION,
+ try Str.matched_group 3 out_VERSION with Not_found -> ""
+ else
+ C.die "Can't read VERSION."
+ in
+ let name =
+ let out = C.Process.run configurator "cat" ["VERSION_CODENAME"] in
+ if out.exit_code <> 0 then
+ C.die "Can't read VERSION_CODENAME." ;
+ String.sub out.stdout 0 (String.length out.stdout - 1)
+ in
+ { major; minor; ext; name }
+
+ let pp_sed fmt version =
+ Format.fprintf fmt
+ "s|@VERSION@|%s.%s%s|\n" version.major version.minor version.ext ;
+ Format.fprintf fmt
+ "s|@VERSION_CODENAME@|%s|\n" version.name ;
+ Format.fprintf fmt
+ "s|@MAJOR_VERSION@|%s|\n" version.major ;
+ Format.fprintf fmt
+ "s|@MINOR_VERSION@|%s|" version.minor
+end
+
+let python_available configurator =
+ let result = C.Process.run configurator "python3" ["--version"] in
+ if result.exit_code <> 0 then false
+ else
+ let out = result.stdout in
+ let re_version =
+ Str.regexp {|.* \([0-9]\)\.\([0-9]+\).[0-9]+|}
+ in
+ try
+ let maj, med =
+ if Str.string_match re_version out 0 then
+ int_of_string @@ Str.matched_group 1 out,
+ int_of_string @@ Str.matched_group 2 out
+ else raise Not_found
+ in
+ if maj <> 3 || med < 7 then raise Not_found ;
+ true
+ with Not_found | Failure _ -> false
+
+let configure configurator =
+ let version = Fc_version.get configurator in
+ let cpp = Cpp.get configurator in
+ let config_sed = open_out "config.sed" in
+ let fmt = Format.formatter_of_out_channel config_sed in
+ Format.fprintf fmt "%a\n%a\n" Fc_version.pp_sed version Cpp.pp_sed cpp ;
+ close_out config_sed ;
+ let python = open_out "python-3.7-available" in
+ Printf.fprintf python "%b" (python_available configurator) ;
+ close_out python
+
+let () =
+ C.main ~name:"frama_c_config" configure
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/disable-plugins.sh b/dev/disable-plugins.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f8dd83fbe2d89f4b1877da393d9dd3fe135dc678
--- /dev/null
+++ b/dev/disable-plugins.sh
@@ -0,0 +1,88 @@
+#!/usr/bin/env bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
+case "$1" in
+ "-h"|"--help")
+ echo "Usage: $0 <plugin directories>"
+ echo " - directories are given without prefix src/plugins"
+ echo " - if no directory is given all plugins are enabled (alternative: none)"
+ exit 0
+esac
+
+if [ ! -f VERSION ]; then
+ echo "This script is meant to be run from the root directory of Frama-C"
+ exit 2
+fi
+
+if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
+ rm -f src/plugins/dune
+ echo "All plugins enabled"
+ echo "Make sure to \"dune clean\" the Frama-C directory before rebuilding"
+ exit 0
+fi
+
+IFS='\, ' read -a DISABLED_PLUGINS <<< "$@"
+
+PLUGINS=
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+ if [ -d "src/plugins/$PLUGIN" ]; then
+ PLUGINS="$PLUGINS $PLUGIN"
+ else
+ echo "Error: src/plugins/$PLUGIN is not a directory"
+ exit 2
+ fi
+done
+
+cat > src/plugins/dune <<EOL
+;; File generated by ./dev/disable-plugins.sh <PLUGINS>
+(include_subdirs no)
+;; Disabled plugin list:
+(data_only_dirs ${PLUGINS})
+(rule
+ (alias "frama-c-configure")
+ (deps (universe))
+ (action (progn
+ (echo "Disabled plug-in(s):\n")
+EOL
+
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+ echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
+done
+
+cat >> src/plugins/dune <<EOL
+)))
+;; Test
+(alias (name ptests) (deps (alias ptests_config)))
+(rule
+ (alias "ptests_config")
+ (deps (universe))
+ (action (progn
+ (echo "Testing with disabled plug-in(s):\n")
+EOL
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+ echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
+done
+echo ")))" >> src/plugins/dune
+
+echo "Disabled plug-ins: $PLUGINS"
+echo "Make sure to clean the current directory before rebuilding"
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/Makefile b/doc/Makefile
index bf7e70ab044e1e97c9a21f73ccb85e4ae9530e4c..584d88aec76d842370af34c38b77519793add281 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -28,12 +28,10 @@ MAKECONFIG_DIR=$(FRAMAC_SRC)/share
include $(FRAMAC_SRC)/share/Makefile.common
-DOCDIR ?= "$(DESTDIR)${prefix}/share/doc"
FRAMAC_DOCDIR ?= $(DOCDIR)/frama-c
.PHONY: .force
-
###################
# Frama-C Version #
###################
@@ -201,3 +199,13 @@ acsl/acsl-implementation.pdf: | acsl/acsl.pdf
$(EACSL_DOC)/refman/e-acsl-implementation.pdf: | $(EACSL_DOC)/refman/e-acsl.pdf
endif
+
+##############################################################################
+# HELP
+################################
+
+help::
+ @echo "Documentation installation configuration variable"
+ @echo " - PREFIX: documentation will be in PREFIX/share/doc/frama-c"
+ @echo " - DOCDIR: (overrides previous variable) documentation will be in DOCDIR/frama-c"
+ @echo " - FRAMAC_DOCDIR: (overrides previous variable) documentation will be in FRAMAC_DOCDIR"
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/dune b/dune
index 0f46950b014e5b34ab7e22cf65d6c459a42162c5..390a079328f3156ed3700979649108cbd4005052 100644
--- a/dune
+++ b/dune
@@ -21,4 +21,13 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(alias (name default) (deps (alias install)))
-(dirs src tools tests headers share bin)
+(dirs bin headers man share src tools tests)
+
+(executable
+ (name configurator)
+ (libraries dune-configurator str))
+
+(rule
+ (deps VERSION VERSION_CODENAME)
+ (targets config.sed python-3.7-available)
+ (action (run ./configurator.exe)))
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..afa38a1d866bac637f8d39398370954904399c02 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -60,6 +60,14 @@ tsc: dome-pkg dome-templ
yarn run typecheck
yarn run lint --fix --cache --cache-location .eslint-cache
+# --------------------------------------------------------------------------
+# --- Help
+# --------------------------------------------------------------------------
+
+help::
+ @echo "Ivette installation configuration variables"
+ @echo " - PREFIX: used to customize installation path"
+
# --------------------------------------------------------------------------
# --- Ivette Package Loader
# --------------------------------------------------------------------------
@@ -159,7 +167,8 @@ include $(DOME)/template/makefile
# --- Ivette Installation
# --------------------------------------------------------------------------
-sinclude ../share/Makefile.config
+BINDIR=$(PREFIX)/bin
+LIBDIR=$(PREFIX)/lib
dist-dir:
@echo "Cleaning dist"
diff --git a/man/dune b/man/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d1ff77d3e0b0cf8d4ce12b54430218a9b15a8582
--- /dev/null
+++ b/man/dune
@@ -0,0 +1,40 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (target frama-c.1.generated)
+ (deps frama-c.1.md)
+ (enabled_if %{bin-available:pandoc})
+ (action (run pandoc -s -t man %{deps} -o %{target}))
+)
+
+(rule
+ (alias check-man)
+ (deps frama-c.1 frama-c.1.generated)
+ (action (diff frama-c.1 frama-c.1.generated))
+)
+
+(install
+ (package frama-c)
+ (section man)
+ (files frama-c.1)
+)
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..457a9d9c82027a6f191172efa31d0de1706996e3 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
@@ -121,9 +121,14 @@ stdenvNoCC.mkDerivation rec {
tar -cf $build_dir/dir.tar .
'';
- # Required so that tests of external plugins can be excuted
+ # Nix moves these directories after they have been installed by Dune and
+ # compress manuals ...
+ # Note: Required so that tests of external plugins can be executed. Don't know
+ # why tests fail without them.
postFixup = ''
cp -r $out/share/doc $out/doc
+ cp -r $out/share/man $out/man
+ gzip -d $out/man/man1/*
'';
# Allow loading of external Frama-C plugins
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..b47f790431761100c1f9fd604a1a8dab930b96d2 100644
--- a/opam/opam
+++ b/opam/opam
@@ -87,16 +87,13 @@ 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 "-C" "doc" "install"] {with-doc}
+ [make "INSTALLDIR=%{prefix}%" "MANDIR=%{mandir}%" "install"]
+ [make "PREFIX=%{prefix}%" "-C" "doc" "install"] {with-doc}
]
run-test: [
@@ -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..8ce54338620771a0d474d640821cda807259d3c5 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -26,36 +26,30 @@
# #
##########################################################################
-#################
-# Make commands #
-#################
-
-define assert_defined
-ifndef $(1)
-$$(error Undefined variable $(1) please report.)
-endif
-endef
-
-##################################
-# Configure & required variables #
-##################################
+#############
+# Platform #
+#############
-$(eval $(call assert_defined,MAKECONFIG_DIR))
+PLATFORM:=$(shell uname -s)
-include $(MAKECONFIG_DIR)/Makefile.config
+#############
+# Locations #
+#############
-#Check share/Makefile.config available
-ifndef FRAMAC_ROOT_SRCDIR
-$(error \
- "You should run ./configure first (or autoconf if there is no configure)")
-endif
+# Note that Dune rules do NOT use these variables.
+# They are used by other Makefiles
+# - Ivette (PREFIX)
+# - Manuals (DOCDIR)
-$(eval $(call assert_defined,PLATFORM))
+PREFIX ?= /usr/local
+DOCDIR ?= $(PREFIX)/share/doc
#############
# 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 +109,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.installation b/share/Makefile.installation
index 535654377a202e058e18620fadb88e2900bb78cb..544db518ed7639961ac7944fb2ec81f6303c366b 100644
--- a/share/Makefile.installation
+++ b/share/Makefile.installation
@@ -24,6 +24,14 @@
# INSTALLATION #
################
+################################
+## Help
+
+help::
+ @echo "Installation configuration variables"
+ @echo " - INSTALLDIR: used to customize installation path"
+ @echo " - MANDIR: used to customize man files installation path"
+
################################
## Default variables
@@ -31,6 +39,17 @@
# Default: Dune installs in the Opam directory
INSTALLDIR?=
+# Set this variable to request a specific man installation directory
+# Default: the manuals are installed in the installation directory transmitted
+# to Dune (so either in Opam or in INSTALLDIR)
+MANDIR?=
+
+ifeq (${MANDIR},)
+MANDIR_OPT=
+else
+MANDIR_OPT=--mandir ${MANDIR}
+endif
+
################################
## Install and uninstall
@@ -38,18 +57,18 @@ INSTALLDIR?=
install:
ifeq ($(INSTALLDIR),)
- dune install
+ dune install ${MANDIR_OPT}
else
@echo "Installing to prefix: ${INSTALLDIR}"
- dune install --prefix ${INSTALLDIR}
+ dune install --prefix ${INSTALLDIR} ${MANDIR_OPT}
@echo 'DO NOT FORGET TO EXPAND YOUR OCAMLPATH VARIABLE:'
@echo ' export OCAMLPATH="${INSTALLDIR}/lib:$$OCAMLPATH"'
endif
uninstall:
ifeq ($(INSTALLDIR),)
- dune uninstall
+ dune uninstall ${MANDIR_OPT}
else
@echo "Uninstalling from prefix: ${INSTALLDIR}"
- dune uninstall --prefix ${INSTALLDIR}
+ dune uninstall --prefix ${INSTALLDIR} ${MANDIR_OPT}
endif
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()
- ])
- ])
diff --git a/src/plugins/e-acsl/man/dune b/src/plugins/e-acsl/man/dune
new file mode 100644
index 0000000000000000000000000000000000000000..44b5571eb4ecee0716eb921c9ad31e3b79380f1a
--- /dev/null
+++ b/src/plugins/e-acsl/man/dune
@@ -0,0 +1,27 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of the Frama-C's E-ACSL plug-in. ;;
+;; ;;
+;; Copyright (C) 2012-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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(install
+ (package frama-c-e-acsl)
+ (section man)
+ (files e-acsl-gcc.sh.1)
+)
diff --git a/tests/compliance/test_config b/tests/compliance/test_config
index 2454128362a6b8b71db649b6d45f3baf2b6df496..7b1cc18c311b1d70b15ed4c6e958070b3a4f257f 100644
--- a/tests/compliance/test_config
+++ b/tests/compliance/test_config
@@ -1 +1,2 @@
PLUGIN:
+ENABLED_IF: %{read:../../../python-3.7-available}
diff --git a/tests/fc_script/estimate_difficulty.i b/tests/fc_script/estimate_difficulty.i
index 23b63dd6c5250076eb5eb8e74f0197b0bd9a12cc..68ee456b3a5a8850ca1b6dd8073e1c09a9a0cada 100644
--- a/tests/fc_script/estimate_difficulty.i
+++ b/tests/fc_script/estimate_difficulty.i
@@ -1,6 +1,7 @@
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
- EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
+ COMMENT: Disabled for now, when tests are executed in parallel, this test often fails
+ DONTRUN: EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
*/
// these includes are not actually used by the compiler
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 1428c373f694cfce0c1f97140f921fa4199319da..7a490e293ff63380fa3ee3e017ccd74713fa4aeb 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -3,7 +3,7 @@
COMMENT: the 'build' command cannot be tested because it requires 'glub'.
DEPS: main2.c main3.c main.c
EXECNOW: LOG list_files.res LOG list_files.err PTESTS_TESTING=1 %{bin:frama-c-script} list-files %{dep:./list_files.json} > ./list_files.res 2> ./list_files.err
- DEPS: for-find-fun2.c for-find-fun.c for-list-functions.c for-list-functions.h for-list-functions2.h main2.c main3.c main.c make-wrapper2.c make-wrapper3.c make-wrapper.c
+ DEPS: build-callgraph.i estimate_difficulty.i for-find-fun2.c for-find-fun.c for-list-functions.c for-list-functions.h for-list-functions2.h list_functions.i main2.c main3.c main.c make-wrapper2.c make-wrapper3.c make-wrapper.c recursions.i
EXECNOW: LOG find_fun1.res LOG find_fun1.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main2 ./ > ./find_fun1.res 2> ./find_fun1.err
EXECNOW: LOG find_fun2.res LOG find_fun2.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main3 ./ > ./find_fun2.res 2> ./find_fun2.err
EXECNOW: LOG find_fun3.res LOG find_fun3.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun false_positive ./ > ./find_fun3.res 2> ./find_fun3.err
diff --git a/tests/fc_script/test_config b/tests/fc_script/test_config
index ff1c5e31628a610eb768e563368ecec4c4cfdad3..11c2e8173b5b072f0e234344a289457747b7cb36 100644
--- a/tests/fc_script/test_config
+++ b/tests/fc_script/test_config
@@ -3,4 +3,5 @@ COMMENT: Explicits the dependencies of {bin:frama-c-script} execution:
PLUGIN: variadic,instantiate
COMMENT: The library frama-c.analysis_scripts is part of the package frama-c
COMMENT: and this dependency is implicit as the one to the needed python files.
+ENABLED_IF: %{read:../../../python-3.7-available}
*/
diff --git a/tests/jcdb/test_config b/tests/jcdb/test_config
index 2454128362a6b8b71db649b6d45f3baf2b6df496..7b1cc18c311b1d70b15ed4c6e958070b3a4f257f 100644
--- a/tests/jcdb/test_config
+++ b/tests/jcdb/test_config
@@ -1 +1,2 @@
PLUGIN:
+ENABLED_IF: %{read:../../../python-3.7-available}