Merge branch 'feature/dune/configure-simplification' into 'feature/bobot/jbuilder'

[Configure] simplification related to config.sed

See merge request frama-c/frama-c!3832

.gitignore

@@ -201,7 +201,6 @@ Makefile.plugin.generated
 /src/kernel_internals/parsing/clexer.ml
 /src/kernel_internals/parsing/cparser.ml
 /src/kernel_internals/parsing/cparser.mli
-/src/libraries/stdlib/transitioning.ml
 # /src/plugins/callgraph/cg_viewer.ml
 /src/plugins/gui/debug_manager.ml
 /src/plugins/gui/dgraph_helper.ml

Makefile

@@ -22,17 +22,10 @@
 
 # This file is the main makefile of Frama-C.
 
-FRAMAC_SRC=.
 MAKECONFIG_DIR=share
 
 include share/Makefile.common
 
-#Check share/Makefile.config available
-ifndef FRAMAC_ROOT_SRCDIR
-$(error \
-  "You should run ./configure first (or autoconf if there is no configure)")
-endif
-
 RELEASE?=no
 ifeq ($(RELEASE),yes)
 DUNE_BUILD_OPTS=--release
@@ -58,81 +51,28 @@ else
 OPTDOT=None
 endif
 
-ifeq ($(HAS_OCAML408),yes)
-  DYNLINK_INIT=fun () -> ()
-  FORMAT_STAG=stag
-  FORMAT_STRING_OF_STAG=match s with \
-        Format.String_tag str -> str \
-      | _ -> raise (Invalid_argument \"unsupported tag extension\")
-  FORMAT_STAG_OF_STRING=Format.String_tag s
-  FORMAT_PP_OPT=Format.pp_print_option
-  HAS_OCAML407_OR_408=yes
-else
-  DYNLINK_INIT=Dynlink.init
-  FORMAT_STAG=tag
-  FORMAT_STRING_OF_STAG=s
-  FORMAT_STAG_OF_STRING=s
-  ifeq ($(HAS_OCAML407),yes)
-    HAS_OCAML407_OR_408=yes
-  else
-    HAS_OCAML407_OR_408=no
-  endif
-  FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \
-    match o with \
-    | None -> none fmt () \
-    | Some v -> pp fmt v
-endif
-
-ifeq ($(HAS_OCAML407_OR_408),yes)
-  FLOAT_MAX_FLOAT=Float.max_float
-else
-  FLOAT_MAX_FLOAT=Pervasives.max_float
-endif
-
-
 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.in
 	@echo "# generated file" > $@
-	@echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@
 	@echo "s|@VERSION@|$(VERSION)|" >> $@
-	@echo "s|@CURR_DATE@|$$(LC_ALL=C date)|" >> $@
-	@echo "s|@OCAMLC@|$(OCAMLC)|" >> $@
-	@echo "s|@OCAMLOPT@|$(OCAMLOPT)|" >> $@
-	@echo "s|@WARNINGS@|$(WARNINGS)|" >> $@
-	@echo "s|@FRAMAC_DATADIR@|$(FRAMAC_DATADIR)|" >> $@
-	@echo "s|@FRAMAC_LIBDIR@|$(FRAMAC_LIBDIR)|" >> $@
-	@echo "s|@FRAMAC_ROOT_SRCDIR@|$(FRAMAC_ROOT_SRCDIR)|" >> $@
-	@echo "s|@FRAMAC_PLUGINDIR@|$(FRAMAC_PLUGINDIR)|" >> $@
+	@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)|" >> $@
 	@echo "s|@OPTDOT@|$(OPTDOT)|" >> $@
-	@echo "s|@EXE@|$(EXE)|" >> $@
-	@echo "s/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g" >> $@
-	@echo "s/@STACK_FOLD@/$(STACK_FOLD)/g" >> $@
-	@echo "s/@NTH_OPT@/$(NTH_OPT)/g" >> $@
-	@echo "s/@FIND_OPT@/$(FIND_OPT)/g" >> $@
-	@echo "s/@ASSOC_OPT@/$(ASSOC_OPT)/g" >> $@
-	@echo "s/@ASSQ_OPT@/$(ASSQ_OPT)/g" >> $@
-	@echo "s/@HAS_YOJSON@/$(HAS_YOJSON)/g" >> $@
-	@echo "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|g" >> $@
-	@echo "s|@MINOR_VERSION@|$(MINOR_VERSION)|g" >> $@
-	@echo "s/@DYNLINK_INIT@/$(DYNLINK_INIT)/g" >> $@
-	@echo "s/@FORMAT_STAG@/$(FORMAT_STAG)/g" >> $@
-	@echo "s/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g" >> $@
-	@echo "s/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g" >> $@
-	@echo "s/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/g" >> $@
-	@echo "s/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g" >> $@
 
 clean:: purge-tests # to be done before a "dune" command
 	dune clean
 	dune clean --root ptests
-	rm -rf _build .merlin config.sed
+	rm -rf _build .merlin config.sed autom4te.cache
 
 ########################################################################
 # Makefile.config is rebuilt whenever configure.in is modified         #

share/Makefile.common

@@ -26,65 +26,31 @@
 #                                                                        #
 ##########################################################################
 
-include $(MAKECONFIG_DIR)/Makefile.config
-
-##################
-# Flags          #
-##################
+#################
+# Make commands #
+#################
 
-# Flags to be used by ocamlc and ocamlopt when compiling Frama-C
-# itself. For development versions, we add -warn-error for most
-# warnings -warn-error has effect only for warnings that are
-# explicitly set using '-w'.
-ifeq ($(DEVELOPMENT),yes)
-# Most warnings are activated by default. Those settings are inherited
-# in the compilation of external plugins.
-# - 4 (fragile pattern-matching) only make sense when adding a node to a type.
-#   OCaml GPR #1071 will make it usable
-# - 6 (omit label in application) would make code clearer, but requires
-#   refactoring before being enabled.
-# - 9 (missing field in record pattern) is much too heavy. Most of the time
-#   not all fields are relevant in pattern-matching Frama-C's AST.
-# - 40 (constructor or label name used out of scope)
-# - 41 (ambiguous constructor or label name)
-# - 42 (Disambiguated constructor or label name)
-#   these three warnings prevents type-based disambiguation,
-#   a feature which is seen as a good thing by many developers
-# - 44 (open shadows an identifier)
-# - 45 (open shadows a label or constructor): While the use of open directives
-#   is supposed to stay small, it should still be possible to open modules
-#   that share common names, barring some mechanism to open only parts of a
-#   module.
-# - 48 (implicit elimination of optional arguments): makes use of functions
-#   with optional arguments heavier in higher-order context
-# - 67 (unused module parameter in functor signature): naming all parameters
-#   in functor signatures is a common practice that seems harmless. Warning 60
-#   ensures that named functor parameters are indeed used in the implementation.
-WARNINGS ?= +a-4-9-40-41-42-44-45-48-67
+define assert_defined
+ifndef $(1)
+$$(error Undefined variable $(1) please report.)
+endif
+endef
 
-# - 3 (deprecated feature) cannot always be avoided for OCaml stdlib when
-#   supporting several OCaml versions
-# - 4 (fragile pattern matching) will be activated when adding a node (see
-#   above), in order to let the developer decide whether a case should be
-#   added on relevant fragile pattern or not: a matching might very well stay
-#   fragile without triggering an error.
-# - 3x (various categories of unused identifiers) it is sometimes useful to
-#   let code compile despite such warnings when in the middle of a development.
-#   On the other hand, a completed feature should not trigger such warnings.
-# - 58 (missing cmx) is triggered by some versions of external libraries.
-#   Situation should probably improve as these libraries get updated, leading
-#   to treat this warning as error.
-WARN_ERROR ?= -warn-error +a-3-4-32-33-34-35-36-37-38-39-58
+##################################
+# Configure & required variables #
+##################################
 
-else
+$(eval $(call assert_defined,MAKECONFIG_DIR))
 
-WARNINGS ?= -a
+include $(MAKECONFIG_DIR)/Makefile.config
 
-endif #DEVELOPMENT
+#Check share/Makefile.config available
+ifndef FRAMAC_ROOT_SRCDIR
+$(error \
+  "You should run ./configure first (or autoconf if there is no configure)")
+endif
 
-FLAGS	= $(WARNINGS) $(WARN_ERROR) $(OCAML_ANNOT_OPTION) -strict-sequence \
-          -safe-string
-DEBUG	= -g
+$(eval $(call assert_defined,PLATFORM))
 
 #############
 # Verbosing #
@@ -116,7 +82,6 @@ else
   MAKE := MAKEFLAGS="$(OLDFLAGS)" $(MAKE)
 endif
 
-
 ##################
 # Shell commands #
 ##################
@@ -153,108 +118,10 @@ GIT	= git
 ifeq ($(PLATFORM),MacOS)
 TAR     = gtar
 else
-# Unix, Cygwin
+# Unix, Cygwin, Win32
 TAR     = tar
 endif
 
-##################
-# Make commands #
-##################
-
-map=$(foreach a,$(2),$(call $(1),$(a)))
-
-define assert_defined
-ifndef $(1)
-$$(error Undefined variable $(1) please report.)
-endif
-endef
-
-###########################
-# Command pretty printing #
-###########################
-
-PRINT_OCAMLC   	=$(PRINT) 'Ocamlc      '#
-PRINT_OCAMLOPT 	=$(PRINT) 'Ocamlopt    '#
-PRINT_DEP      	=$(PRINT) 'Ocamldep    '#
-PRINT_OCAMLLEX 	=$(PRINT) 'Ocamllex    '#
-PRINT_OCAMLYACC	=$(PRINT) 'Ocamlyacc   '#
-PRINT_OCAMLMKTOP=$(PRINT) 'Ocamlmktop  '#
-PRINT_DOC	=$(PRINT) 'Ocamldoc    '#
-PRINT_OCAMLCP  	=$(PRINT) 'Profiling   '#
-PRINT_CAMLP4   	=$(PRINT) 'Camlp4      '#
-PRINT_PACKING  	=$(PRINT) 'Packing     '#
-PRINT_LINKING  	=$(PRINT) 'Linking     '#
-PRINT_INFERRING	=$(PRINT) 'Inferring   '#
-PRINT_CC   	=$(PRINT) 'CC          '#
-
-PRINT_MAKING   	=$(PRINT) 'Generating  '#
-PRINT_MV       	=$(PRINT) 'Moving to   '#
-PRINT_CP       	=$(PRINT) 'Copying to  '#
-PRINT_RM       	=$(PRINT) 'Cleaning    '#
-PRINT_EXEC	=$(PRINT) 'Running     '#
-PRINT_TAR    	=$(PRINT) 'Archiving   '#
-PRINT_UNTAR    	=$(PRINT) 'Unarchiving '#
-PRINT_CONFIG   	=$(PRINT) 'Configuring '#
-PRINT_BUILD   	=$(PRINT) 'Building    '#
-PRINT_INSTALL  	=$(PRINT) 'Installing  '#
-PRINT_UPDATE  	=$(PRINT) 'Updating    '#
-
-PRINT_DOT	=$(PRINT) 'Dot         '#
-PRINT_LATEX	=$(PRINT) 'Latex       '#
-PRINT_DVIPS	=$(PRINT) 'Dvips       '#
-PRINT_HEVEA	=$(PRINT) 'Hevea       '#
-
-#########
-# Tests #
-#########
-
-
-#################
-# Documentation #
-#################
-
-NATIVE_OCAMLDOC:=$(shell ocamlfind ocamldoc -v | grep -o ocamldoc.opt)
-
-ifeq ("$(NATIVE_OCAMLDOC)","ocamldoc.opt")
-DOC_PLUGIN=$(DOC_DIR)/docgen.cmxs
-else
-DOC_PLUGIN=$(DOC_DIR)/docgen.cmo
-endif
-
-##########################
-# Plugin File Generation #
-##########################
-
-#take the name of the plugin as argument $(1)
-define include_generic_plugin_Makefile
-$(call assert_defined,PLUGIN_DIR)
-$(PLUGIN_DIR)/.Makefile.plugin.generated: $(MAKECONFIG_DIR)/Makefile.plugin.template
-	$(PRINT_MAKING)	$$@
-	$(SED) -e "s/@PLUGIN_NAME@/$(1)/g" $$< > $$@
-
-# We still clean the old Makefile.plugin.generated (without the dot) temporarily
-clean::
-	rm -rf $(PLUGIN_DIR)/.Makefile.plugin.generated
-	rm -rf $(PLUGIN_DIR)/Makefile.plugin.generated
-
-#We always define this variable because it can't wait the generation
-#of the Makefile.plugin.generated since the targets of rules defined in the
-#Makefile of the plugins could use this variable
-$(1)_DIR:=$(PLUGIN_DIR)
-
-sinclude $(PLUGIN_DIR)/.Makefile.plugin.generated
-
-endef
-
-%.check_mli_exists: %.mli
-	touch $@
-
-.PHONY:common_force_rule
-
-%.check_mli_exists: common_force_rule
-	$(error "The file '$*.mli' must be provided. The simplest workaround is 'touch $*.mli')
-
-
 ##########################################################################
 # Local Variables:
 # compile-command: "make"

share/Makefile.config.in

@@ -48,181 +48,22 @@ 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@
-CC =@CC@
-
-###############
-# Ocaml stuff #
-###############
-
-# compilers and others executables
-OCAMLC  	?=@OCAMLC@
-OCAMLOPT	?=@OCAMLOPT@
-OCAMLDEP	?=@OCAMLDEP@ -slash
-OCAMLLEX	?=@OCAMLLEX@
-OCAMLYACC	?=@OCAMLYACC@
-OCAMLMKTOP	?=@OCAMLMKTOP@
-OCAMLMKLIB	?=@OCAMLFIND@ ocamlmklib
-OCAMLFIND	?=@OCAMLFIND@
-OCAMLDOC	?=@OCAMLDOC@
-OCAMLCP		?=@OCAMLCP@
-
-# others ocaml stuffs
-
-# either -annot or -dtypes
-OCAML_ANNOT_OPTION ?=@OCAML_ANNOT_OPTION@
-# ocaml stdlib path
-OCAMLLIB	?=@OCAMLLIB@
-# either opt or byte
-OCAMLBEST	?=@OCAMLBEST@
-
-OCAMLVERSION 	?=@OCAMLVERSION@
-
-OCAMLMAJORNB    ?=@OCAMLMAJORNB@
-OCAMLMINORNB    ?=@OCAMLMINORNB@
-OCAMLPATCHNB    ?=@OCAMLPATCHNB@
-
-HAS_OCAML409    ?=@HAS_OCAML409@
-HAS_OCAML410    ?=@HAS_OCAML410@
-
-PLATFORM	?=@PLATFORM@
-OCAMLWIN32	?=@OCAMLWIN32@
-DLLEXT          ?=@DLLEXT@
-
-DEVELOPMENT	?=@DEVELOPMENT@
-
-#############
-# Libraries #
-#############
-
-# ocamlgraph
-HAS_OCAMLGRAPH_2 ?= @HAS_OCAMLGRAPH_2@
-HAS_DGRAPH ?= @HAS_DGRAPH@
-
-# lablgtk
-HAS_LABLGTK	?=@HAS_LABLGTK@
-HAS_LABLGTK_CUSTOM_MODEL ?=@HAS_LABLGTK@
-LABLGTK_PATH ?=@LABLGTK_PATH@
-LABLGTK ?= lablgtk@LABLGTK_VERSION@
-# lablgtksourceview
-HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@
-#gnomecanvas
-HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
-
-LABLGTK_VERSION ?=@LABLGTK_VERSION@
-ifeq ("$(LABLGTK_VERSION)","3")
-  GTKSOURCEVIEW:=lablgtk3-sourceview3
-  THREAD:=-thread
-else
-  GTKSOURCEVIEW:=\
-    $(patsubst lablgtk%,$(LABLGTK).%,$(basename $(notdir @GTKSOURCEVIEW@)))
-  THREAD:=
-endif
-
-# apron
-HAS_APRON	?=@HAS_APRON@
-
-# mpfr
-HAS_MPFR ?=@HAS_MPFR@
-
-# landmarks
-HAS_LANDMARKS	?=@HAS_LANDMARKS@
-
-# python 3.7
-HAS_PYTHON37 ?=@HAS_PYTHON37@
-
-##########################
-# Miscellaneous commands #
-##########################
-
-OTAGS		?=@OTAGS@
-DOT		?=@DOT@
-HAS_DOT		?=@HAS_DOT@
-
-HEADACHE 	?= headache -c $(FRAMAC_SRC)/headers/headache_config.txt
-
-UNIX2DOS        ?= @UNIX2DOS@
-HAS_UNIX2DOS    ?= @HAS_UNIX2DOS@
 
 ###########################
 # Miscellaneous variables #
 ###########################
 
-VERBOSEMAKE	?=@VERBOSEMAKE@
-LOCAL_MACHDEP	?=@LOCAL_MACHDEP@
-EXE		?=@EXE@
-
-# Required by Cil
-UNDERSCORE_NAME ?=@UNDERSCORE_NAME@
-HAVE_BUILTIN_VA_LIST ?=@HAVE_BUILTIN_VA_LIST@
-
-# test directories for ptests configuration
-# Non-plugin test directories containing some ML files to compile
-TEST_DIRS_AS_PLUGIN:=\
-  dynamic saveload spec misc syntax cil \
-  pretty_printing builtins libc value
-
-ifeq ($(HAS_PYTHON37),yes)
-TEST_DIRS_AS_PLUGIN+= compliance fc_script jcdb
-endif
-
-PLUGIN_TESTS_LIST+=$(TEST_DIRS_AS_PLUGIN)
-
-##########################
-# Variables for plug-ins #
-##########################
-
-EXTERNAL_PLUGINS ?=@EXTERNAL_PLUGINS@
-
-# Integrated plugins
-ENABLE_CALLGRAPH                  ?=@ENABLE_CALLGRAPH@
-ENABLE_CONSTANT_PROPAGATION       ?=@ENABLE_SEMANTIC_CONSTANT_FOLDING@
-ENABLE_FROM_ANALYSIS              ?=@ENABLE_FROM_ANALYSIS@
-ENABLE_GUI	                  ?=@ENABLE_GUI@
-ENABLE_IMPACT	                  ?=@ENABLE_IMPACT@
-ENABLE_INOUT	                  ?=@ENABLE_INOUT@
-ENABLE_METRICS	                  ?=@ENABLE_METRICS@
-ENABLE_OCCURRENCE                 ?=@ENABLE_OCCURRENCE@
-ENABLE_PDG	                  ?=@ENABLE_PDG@
-ENABLE_POSTDOMINATORS             ?=@ENABLE_POSTDOMINATORS@
-ENABLE_REDUC                      ?=@ENABLE_REDUC@
-ENABLE_RTEGEN                     ?=@ENABLE_RTEGEN@
-ENABLE_SCOPE	                  ?=@ENABLE_SCOPE@
-ENABLE_SLICING	                  ?=@ENABLE_SLICING@
-ENABLE_SPARECODE                  ?=@ENABLE_SPARECODE@
-ENABLE_USERS	                  ?=@ENABLE_USERS@
-ENABLE_EVA                      ?=@ENABLE_EVA@
-
-#bytes is part of the stdlib, but is used as a transitional package.
-LIBRARY_NAMES := \
-  findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray \
-  ppx_import ppx_deriving.eq
-
-ifeq ($(HAS_LANDMARKS),yes)
-LIBRARY_NAMES += landmarks landmarks-ppx
-endif
+# Used by Makefile.common
+PLATFORM	?=@PLATFORM@
 
-ifneq ($(ENABLE_GUI),no)
-  LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW)
-  ifeq ($(HAS_OCAMLGRAPH_2),yes)
-    ifeq ($(HAS_DGRAPH),yes)
-      LIBRARY_NAMES_GUI+=ocamlgraph_gtk
-    endif
-  else
-    ifeq ($(HAS_GNOMECANVAS),yes)
-      LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas
-      GRAPH_GUICMO= dgraph.cmo
-      GRAPH_GUICMX= dgraph.cmx
-      GRAPH_GUIO= dgraph.o
-    endif
-  endif
-else
-LIBRARY_NAMES_GUI =
-endif
+# Used by Makefile.common
+VERBOSEMAKE	?=@VERBOSEMAKE@
 
 #######################
 # Working directories #

src/kernel_internals/runtime/dump_config.ml

@@ -51,10 +51,10 @@ let dump_to_json () =
     "major_version", `Int Fc_config.major_version ;
     "minor_version", `Int Fc_config.minor_version ;
     "is_gui", `Bool Fc_config.is_gui ;
-    "lablgtk", `String Fc_config.lablgtk ;
-    (* "ocamlc", `String Fc_config.ocamlc ;
-     * "ocamlopt", `String Fc_config.ocamlopt ; *)
-    "ocaml_wflags", `String Fc_config.ocaml_wflags ;
+    (* "lablgtk", `String Fc_config.lablgtk ;
+     * "ocamlc", `String Fc_config.ocamlc ;
+     * "ocamlopt", `String Fc_config.ocamlopt ;
+     * "ocaml_wflags", `String Fc_config.ocaml_wflags ; *)
     "datadir", `String (Fc_config.datadir:>string) ;
     "datadirs",
     list string (Filepath.Normalized.to_string_list Fc_config.datadirs) ;

src/kernel_internals/runtime/fc_config.ml.in

@@ -32,9 +32,6 @@ let minor_version = @MINOR_VERSION@
 
 let is_gui = Frama_c_very_first.Gui_init.is_gui
 
-let lablgtk = "@LABLGTK@"
-
-let ocaml_wflags = "@WARNINGS@"
 let datadirs = (List.map Filepath.Normalized.of_string Config_data.Sites.share)
 let datadir = List.hd (List.rev datadirs)
 

src/kernel_internals/runtime/fc_config.mli

@@ -48,14 +48,6 @@ val is_gui: bool
       @since frama-c-trunk not anymore a reference
 *)
 
-val lablgtk: string
-(** Name of the lablgtk version against which Frama-C has been compiled.
-    blank if only command-line mode is available. *)
-
-val ocaml_wflags: string
-(** Warning flags used when compiling Frama-C.
-    @since Chlorine-20180501 *)
-
 val datadirs: Filepath.Normalized.t list
 (** Directories where architecture independent files are in order of
     priority.

src/libraries/stdlib/dune

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;                                                                        ;;
-;;  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
-  (targets transitioning.ml)
-  (deps transitioning.ml.in ../../../config.sed)
-  (action (with-stdout-to transitioning.ml (run sed -f ../../../config.sed transitioning.ml.in)))
-)

src/plugins/aorai/Makefile.in

-##########################################################################
-#                                                                        #
-#  This file is part of Aorai plug-in 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)                                                 #
-#    INSA  (Institut National des Sciences Appliquees)                   #
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Makefile for compiling Aorai independently of Frama-C.
-#
-# To be used independently of Frama-C, a version of Frama-C compatible with
-# Aorai has to be properly installed as long as the Aorai-specific stuff.
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-PLUGIN_DIR ?=.
-
-PLUGIN_ENABLE:=@ENABLE_AORAI@
-PLUGIN_NAME:=Aorai
-PLUGIN_GENERATED:= $(addprefix ${PLUGIN_DIR}/, \
-		aorai_eva_analysis.ml \
-		promelalexer_withexps.ml promelaparser_withexps.ml \
-		promelaparser_withexps.mli \
-		promelalexer.ml promelaparser.ml promelaparser.mli \
-		ltllexer.ml ltlparser.ml ltlparser.mli \
-		yalexer.ml yaparser.ml yaparser.mli)
-PLUGIN_CMO:= bool3 \
-	aorai_option \
-	path_analysis \
-	promelaoutput \
-	logic_simplification \
-	aorai_graph \
-	aorai_metavariables \
-	data_for_aorai \
-	aorai_utils \
-	ltl_output \
-	utils_parser \
-	ltlparser \
-	ltllexer \
-	yaparser \
-	yalexer \
-	promelaparser \
-	promelalexer \
-	promelaparser_withexps \
-	promelalexer_withexps \
-	aorai_dataflow \
-	aorai_visitors \
-	aorai_eva_analysis \
-	aorai_register
-PLUGIN_CMI:= ltlast promelaast
-
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= \
-	aorai_eva_analysis.enabled.ml aorai_eva_analysis.disabled.ml \
-	Makefile.in configure.ac configure
-PLUGIN_HAS_EXT_DOC:=no # [JS 2010/07/28] was 'yes'
-                       # but prevent 'make src-distrib to work
-PLUGIN_DEPENDENCIES:=
-
-# Dynamic dependencies
-
-ifneq "$(ENABLE_EVA)" "no"
-PLUGIN_DEPENDENCIES+= Eva
-AORAI_EVA_ANALYSIS:= $(PLUGIN_DIR)/aorai_eva_analysis.enabled.ml
-else
-AORAI_EVA_ANALYSIS:= $(PLUGIN_DIR)/aorai_eva_analysis.disabled.ml
-endif
-
-$(PLUGIN_DIR)/aorai_eva_analysis.ml: $(AORAI_EVA_ANALYSIS)
-	$(PRINT_MAKING) $@
-	$(CP) $(AORAI_EVA_ANALYSIS) $@
-	$(CHMOD_RO) $@
-
-$(PLUGIN_DIR)/aorai_eva_analysis.ml: $(PLUGIN_DIR)/Makefile share/Makefile.config
-
-# Tests
-
-# aorai_ya can always be run
-PLUGIN_TESTS_DIRS:=ya
-
-ifeq (@HAS_LTLTOBA@,yes)
-PLUGIN_TESTS_DIRS+=ltl
-endif
-
-PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/Aorai_test.ml $(PLUGIN_DIR)/tests/ya/name_projects.ml
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-AORAI_WP_SHARE=-aorai-test-wp-share $(FRAMAC_ROOT_SRCDIR)/src/plugins/wp/share
-else
-CONFIG_STATUS_DIR=.
-AORAI_WP_SHARE=
-endif
-
-TEST_DEPENDENCIES:= \
-  $(Aorai_DIR)/tests/Aorai_test.cmxs \
-  $(Aorai_DIR)/tests/Aorai_test.cmo \
-  $(Aorai_DIR)/tests/ya/name_projects.cmxs \
-  $(Aorai_DIR)/tests/ya/name_projects.cmo
-
-Aorai_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
-
-# 'prove' ptests config: ensure ACSL and C instrumentation coincide
-# Launch this configuration for all tests with
-# make aorai-test-prove
-# To launch only one test, you can use PTESTS_OPTS, as in
-# PTESTS_OPTS="tests/ya/stack.i -add-options '-wp-verbose 1'" make aorai-test-prove
-#
-# This requires to have a copy of the wp-cache repository
-# (see ../wp/tests/README.md for more information). If it is not
-# in its default place of ../wp-cache, use AORAI_WP_CACHE variable to give the
-# proper absolute path.
-# Don't forget to add the new cache files to the repo if needed,
-# in particular if CI complains about its aorai-prove target.
-
-$(Aorai_DIR)/tests/ptests_config: $(Aorai_DIR)/tests/test_config_prove
-
-$(Aorai_DIR)/tests/test_config_prove: \
-  $(Aorai_DIR)/tests/test_config_prove.in $(Aorai_DIR)/Makefile
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
-	$(CHMOD_RO) $@
-
-AORAI_WP_CACHEDIR?=$(abspath $(Aorai_DIR)/../wp-cache)
-AORAI_WP_CACHE?=update
-
-.PHONY: aorai-test-prove
-aorai-test-prove: $(TEST_DEPENDENCIES) $(Aorai_DIR)/tests/test_config_prove
-	FRAMAC_WP_CACHE=$(AORAI_WP_CACHE) \
-	FRAMAC_WP_CACHEDIR=$(AORAI_WP_CACHEDIR) \
-	PTESTS_OPTS="$$PTESTS_OPTS -config prove" \
-	$(MAKE) Aorai_TESTS
-
-# Regenerating the Makefile on need
-
-$(Aorai_DIR)/Makefile: $(Aorai_DIR)/Makefile.in \
-			$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
-
-headers::
-	$(SED) -e 's/This file is/Files in this archive are/' \
-	       $(FRAMAC_SRC)/headers/open-source/INSA_INRIA_LGPL \
-	> $(FRAMAC_SRC)/doc/aorai/example/LICENSE

src/plugins/dive/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-#######################
-# Frama-C Environment #
-#######################
-
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE	:= $(shell frama-c-config -print-share-path)
-endif
-
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR	:= $(shell frama-c-config -print-libpath)
-endif
-
-#########################
-# Plug-in configuration #
-#########################
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_DIVE@
-PLUGIN_NAME := Dive
-PLUGIN_CMO := self callstack node_kind node_range dive_graph context build \
-  main server_interface
-PLUGIN_CMI := dive_types
-PLUGIN_DEPENDENCIES:= Eva Studia Server
-PLUGIN_HAS_MLI:= yes
-PLUGIN_TESTS_DIRS:=dive
-PLUGIN_GENERATED:=
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
-CONFIG_STATUS_DIR_DEP:=
-else
-CONFIG_STATUS_DIR:=$(Dive_DIR)
-CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
-endif
-
-$(Dive_DIR)/Makefile: $(Dive_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/e-acsl/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-#######################
-# Frama-C Environment #
-#######################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-###################
-# Plug-in sources #
-###################
-
-# libraries
-SRC_LIBRARIES:= \
-	error \
-	builtins \
-	functions \
-	misc \
-	gmp_types \
-	logic_aggr \
-	varname
-SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
-
-# project initializer
-SRC_PROJECT_INITIALIZER:= \
-	rtl \
-	prepare_ast
-SRC_PROJECT_INITIALIZER:=\
-  $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
-
-# analyses
-ANALYSES_CMI:= \
-	analyses_types
-ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
-
-SRC_ANALYSES:= \
-	lscope \
-	analyses_datatype \
-	rte \
-	e_acsl_visitor \
-	logic_normalizer \
-	bound_variables \
-	interval \
-	typing \
-	labels \
-	literal_strings \
-	memory_tracking \
-	exit_points \
-	analyses
-SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
-
-# code generator
-CODE_GENERATOR_CMI:= \
-	contract_types
-CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
-
-SRC_CODE_GENERATOR:= \
-	translation_error \
-	smart_exp \
-	smart_stmt \
-	gmp \
-	env \
-	assert \
-	rational \
-	typed_number \
-	assigns \
-	logic_functions \
-	loops \
-	quantif \
-	memory_translate \
-	logic_array \
-	translate_utils \
-	translate_ats \
-	translate_terms \
-	translate_predicates \
-	translate_rtes \
-	contract \
-	translate_annots \
-	temporal \
-	memory_observer \
-	literal_observer \
-	global_observer \
-	libc \
-	injector
-SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
-
-#########################
-# Plug-in configuration #
-#########################
-
-PLUGIN_DIR ?=.
-PLUGIN_EXTRA_DIRS:=\
-	src \
-	src/libraries \
-	src/analyses \
-	src/project_initializer \
-	src/code_generator
-PLUGIN_ENABLE:=@ENABLE_E_ACSL@
-PLUGIN_NAME:=E_ACSL
-PLUGIN_CMO:= src/local_config \
-	src/options \
-	$(SRC_LIBRARIES) \
-	$(SRC_PROJECT_INITIALIZER) \
-	$(SRC_ANALYSES) \
-	$(SRC_CODE_GENERATOR) \
-	src/main
-PLUGIN_CMI:= \
-	$(LIBRARIES_CMI) \
-	$(ANALYSES_CMI) \
-	$(CODE_GENERATOR_CMI)
-PLUGIN_HAS_MLI:=yes
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_DEPENDENCIES:= RteGen
-PLUGIN_GENERATED:=
-
-# We "save" this variable so that it can be used once PLUGIN_DIR has been reset
-EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
-
-# Suppress a spurious warning with OCaml >= 4.04.0
-$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmo \
-$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmi: E_ACSL_BFLAGS+= -w -60
-$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmx: E_ACSL_OFLAGS+= -w -60
-
-###############
-# Local Flags #
-###############
-# Do not edit the line below: it is automatically set by 'make e-acsl-distrib'
-IS_DISTRIBUTED:=no
-
-#######################
-# Local configuration #
-#######################
-
-PLUGIN_GENERATED += $(EACSL_PLUGIN_DIR)/src/local_config.ml
-
-VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION
-
-################
-# Version      #
-################
-
-EACSL_VERSION:=$(shell sed -e 's/\\(.*\\)/\\1/' $(VERSION_FILE))
-
-$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile $(VERSION_FILE)
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
-	$(ECHO) "let version = \""$(EACSL_VERSION)"\"" >> $@
-	$(CHMOD_RO) $@
-
-###########
-# Testing #
-###########
-
-ifeq (@MAY_RUN_TESTS@,yes)
-
--include in_frama_ci
-
-PLUGIN_TESTS_DIRS := \
-	examples \
-	bts \
-	concurrency \
-	constructs \
-	arith \
-	memory \
-	gmp-only \
-	full-mtracking \
-	format \
-	temporal \
-	special \
-	builtin \
-	libc
-
-PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.ml
-
-DEV?=
-ifeq ("$(DEV)","yes")
-  EACSL_TEST_CONFIG:=dev
-endif
-
-ifdef EACSL_TEST_CONFIG
-  # Prepend PTESTS_OPTS with the test config to use. If the user-provided
-  # PTESTS_OPTS variable contains another -config instruction, then it will be
-  # prioritized over the one selected by the Makefile.
-  E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: override PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG) $(PTESTS_OPTS)
-endif
-
-TEST_DEPENDENCIES:= \
-	$(EACSL_PLUGIN_DIR)/tests/ptests_config \
-	$(EACSL_PLUGIN_DIR)/tests/test_config \
-	$(EACSL_PLUGIN_DIR)/tests/test_config_dev \
-	$(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo \
-	$(EACSL_PLUGIN_DIR)/tests/wrapper.sh
-
-ifeq ($(OCAMLBEST),opt)
-TEST_DEPENDENCIES += \
-	$(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmxs
-endif
-
-ifneq ("$(PLUGIN_ENABLE)","no")
-# Add the test dependencies to the test targets, but also to
-# `plugins_ptests_config` so that they are built along with the main target.
-plugins_ptests_config: $(TEST_DEPENDENCIES)
-E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
-tests:: $(TEST_DEPENDENCIES)
-endif
-
-clean::
-	for d in $(E_ACSL_EXTRA_DIRS); do \
-	  $(RM) $$d/*~; \
-	done
-	$(PRINT_RM) cleaning generated test files
-	$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
-	$(RM) $(foreach dir, $(PLUGIN_TESTS_DIRS), tests/$(dir)/result/*)
-
-endif
-
-################################################
-# Third-party C libraries                      #
-################################################
-
-EACSL_LIBDIR := $(EACSL_PLUGIN_DIR)/lib
-
-############
-# DLMALLOC #
-############
-
-EACSL_DLMALLOC_REL_DIR := contrib/libdlmalloc
-EACSL_DLMALLOC_DIR := $(EACSL_PLUGIN_DIR)/$(EACSL_DLMALLOC_REL_DIR)
-EACSL_DLMALLOC_LIBNAME = libeacsl-dlmalloc.a
-EACSL_DLMALLOC_LIB = $(EACSL_LIBDIR)/$(EACSL_DLMALLOC_LIBNAME)
-EACSL_DLMALLOC_SRC = $(EACSL_DLMALLOC_DIR)/dlmalloc.c
-EACSL_DLMALLOC_OBJ  = dlmalloc.o
-# Don't forget to update "e-acsl-gcc.sh" if the flags are updated
-EACSL_DLMALLOC_FLAGS = \
-  -DHAVE_MORECORE=0 \
-  -DHAVE_MMAP=1  \
-  -DNO_MALLINFO=1 \
-  -DNO_MALLOC_STATS=1 \
-  -DMSPACES=1 \
-  -DONLY_MSPACES \
-  -DMALLOC_ALIGNMENT=32 \
-  -DMSPACE_PREFIX="__e_acsl_" \
-  -DUSE_LOCKS=1 \
-  -DUSE_SPIN_LOCKS=1
-
-$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC) $(EACSL_PLUGIN_DIR)/Makefile
-	$(MKDIR) $(EACSL_LIBDIR)
-	echo 'CC           $<'
-	$(CC) $< -c -O2 -g3 -o$(EACSL_DLMALLOC_OBJ) $(EACSL_DLMALLOC_FLAGS)
-	echo 'AR           $@'
-	$(AR) crus $@ $(EACSL_DLMALLOC_OBJ)
-	echo 'RANLIB       $@'
-	ranlib $@
-
-ifneq ("$(PLUGIN_ENABLE)","no")
-all:: $(EACSL_DLMALLOC_LIB)
-
-clean::
-	$(RM) $(EACSL_DLMALLOC_LIB)
-endif
-
-############
-# Cleaning #
-############
-
-EACSL_CLEANFILES = doc/doxygen/doxygen.cfg \
-	Makefile config.log config.status configure .depend autom4te.cache/* \
-	META.frama-c-e_acsl Makefile.plugin.generated src/local_config.ml \
-	top/* \
-	$(TEST_DEPENDENCIES)
-
-e-acsl-distclean: clean
-	$(PRINT_RM) generated project files
-	$(RM) $(wildcard $(addprefix $(E_ACSL_DIR)/, $(EACSL_CLEANFILES)))
-
-#################################################################
-# Common variables between source distribution and installation #
-#################################################################
-
-EACSL_C_DIRECTORIES := \
-	e-acsl \
-	e-acsl/internals \
-	e-acsl/instrumentation_model \
-	e-acsl/observation_model \
-	e-acsl/observation_model/internals \
-	e-acsl/observation_model/bittree_model \
-	e-acsl/observation_model/segment_model \
-	e-acsl/numerical_model \
-	e-acsl/libc_replacements
-
-EACSL_SCRIPTS := \
-	scripts/e-acsl-gcc.sh
-
-EACSL_BASHCOMPS := \
-	scripts/e-acsl-gcc.sh.comp
-
-EACSL_MANPAGES := \
-	man/e-acsl-gcc.sh.1
-
-################################
-# Building source distribution #
-################################
-
-EACSL_CONTRIB_FILES = \
-  $(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c
-
-EACSL_DOC_FILES = \
-	doc/doxygen/doxygen.cfg.in \
-	doc/Changelog \
-	$(EACSL_MANPAGES)
-
-EACSL_TEST_FILES = \
-	tests/test_config_dev \
-	tests/test_config \
-	tests/wrapper.sh \
-	tests/gmp-only/test_config \
-	tests/gmp-only/test_config_dev \
-	tests/full-mtracking/test_config \
-	tests/full-mtracking/test_config_dev \
-	tests/builtin/test_config \
-	tests/builtin/test_config_dev \
-	tests/temporal/test_config \
-	tests/temporal/test_config_dev \
-	tests/format/test_config \
-	tests/format/test_config_dev \
-	tests/concurrency/test_config \
-	tests/concurrency/test_config_dev \
-	tests/E_ACSL_test.ml
-
-EACSL_TESTS_C_FILES = \
-  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-      $(dir)/*.[ich] \
-  ) \
-  tests/utils/signalled.h
-
-# Test files without header management
-EACSL_DISTRIB_TESTS = \
-  $(EACSL_TESTS_C_FILES) \
-  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-      $(dir)/test_config \
-      $(dir)/test_config_dev \
-      $(dir)/oracle/* \
-      $(dir)/oracle_dev/* \
-  ) \
-  tests/builtin/utils \
-  tests/format/utils
-
-EACSL_RTL_FILES = $(EACSL_RTL_SRC)
-
-EACSL_SCRIPT_FILES = $(EACSL_SCRIPTS)
-
-EACSL_BASHCOMP_FILES = $(EACSL_BASHCOMPS)
-
-EACSL_LICENSE_FILES = \
-  license/CEA_LGPL license/SPARETIMELABS \
-  license/headache_config.txt license/LGPLv2.1
-
-EACSL_MISC_FILES = \
-  configure.ac Makefile.in README tab-in-changelog.sh
-
-EACSL_SHARE_FILES = \
-	$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
-
-EACSL_DISTRIB_EXTERNAL =\
-  $(EACSL_SHARE_FILES) \
-  $(EACSL_MISC_FILES) \
-  $(EACSL_DOC_FILES) \
-  $(EACSL_TEST_FILES) \
-  $(EACSL_RTL_FILES) \
-  $(EACSL_SCRIPT_FILES) \
-  $(EACSL_BASHCOMP_FILES) \
-  $(EACSL_LICENSE_FILES) \
-  $(EACSL_CONTRIB_FILES)
-
-PLUGIN_DISTRIB_EXTERNAL:= $(EACSL_DISTRIB_EXTERNAL)
-
-# Files of `DISTRIB_FILES` without header and not listed in file
-# `headers/header_specs.txt`.
-PLUGIN_HEADER_EXCEPTIONS:=
-
-# Files that are not listed in `DISTRIB_FILES`
-# and dedicated to distributed tests
-PLUGIN_DISTRIB_TESTS:= $(EACSL_DISTRIB_TESTS)
-
-########
-# Misc #
-########
-
-wc:
-	ocamlwc -p $(EACSL_OCAML_FILES)
-
-# Files to format with clang-format
-EACSL_CLANG_FORMAT_SRC:=\
-	$(addprefix $(EACSL_PLUGIN_DIR)/,$(EACSL_TESTS_C_FILES)) \
-	$(addprefix $(EACSL_PLUGIN_DIR)/,$(EACSL_SHARE_FILES))
-
-# Format C files
-eacsl-clang-format:
-	if command -v clang-format >/dev/null; then \
-		echo "Formatting E-ACSL C files with clang-format..."; \
-		clang-format -i $(EACSL_CLANG_FORMAT_SRC); \
-	else \
-		echo "clang-format should be installed to check the formatting of E-ACSL C files"; \
-	fi;
-
-# Check if C files are correctly formatted
-eacsl-lint-c:
-	if command -v clang-format >/dev/null; then \
-		echo "Checking formatting of E-ACSL C files..."; \
-		clang-format --dry-run -Werror $(EACSL_CLANG_FORMAT_SRC); \
-	else \
-		echo "clang-format should be installed to check the formatting of E-ACSL C files"; \
-	fi;
-
-# Check for the absence of <TAB> characters in the changelog
-eacsl-lint-changelog:
-	echo "Checking changelog of E-ACSL for the absence of <TAB> characters..."
-	$(EACSL_PLUGIN_DIR)/tab-in-changelog.sh
-
-# Extend lint step with E-ACSL specific lint
-lint:: eacsl-lint-changelog eacsl-lint-c
-
-##########
-# Header #
-##########
-
-ifneq ("$(FRAMAC_INTERNAL)","yes")
-
-EACSL_SPARETIMELABS= \
-	$(EACSL_PLUGIN_DIR)/share/e-acsl/internals/e_acsl_rtl_io.h \
-	$(EACSL_PLUGIN_DIR)/share/e-acsl/internals/e_acsl_rtl_io.c
-
-EACSL_SHARE_BARE= \
-	$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
-EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
-EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))
-
-EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
-	E_ACSL.mli \
-	Makefile.in configure.ac tab-in-changelog.sh \
-	scripts/*.sh \
-	scripts/*.comp \
-	tests/E_ACSL_test.ml \
-	tests/wrapper.sh \
-	man/e-acsl-gcc.sh.1
-EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
-               $(EACSL_CEA_SHARE)
-
-# valid values: open-source, close-source
-EACSL_HEADERS?=open-source
-headers::
-	@echo "Applying $(EACSL_HEADERS) headers..."
-	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/CEA_LGPL_OR_PROPRIETARY.E_ACSL \
-                 $(EACSL_CEA_LGPL)
-	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_SPARETIMELABS \
-                 $(EACSL_SPARETIMELABS)
-	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_DLMALLOC \
-                 $(EACSL_PLUGIN_DIR)/contrib/libdlmalloc/dlmalloc.c
-
-endif
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-###########
-# Install #
-###########
-
-EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))
-
-EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES))
-
-EACSL_INSTALL_BASHCOMPS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_BASHCOMPS))
-
-EACSL_INSTALL_LIB_DIR :=$(FRAMAC_LIBDIR)/e-acsl
-
-EACSL_INSTALL_CONTRIB_DIR :=$(FRAMAC_DATADIR)/e-acsl/contrib
-
-install:: clean-install
-	$(PRINT_INSTALL) E-ACSL share files
-	for dir in $(EACSL_C_DIRECTORIES); do \
-		$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
-		$(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
-	done
-	$(PRINT_INSTALL) E-ACSL libraries
-	$(MKDIR) $(EACSL_INSTALL_LIB_DIR)
-	$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(EACSL_INSTALL_LIB_DIR)
-	$(MKDIR) $(EACSL_INSTALL_CONTRIB_DIR)/libdlmalloc
-	$(CP) $(EACSL_DLMALLOC_SRC) $(EACSL_INSTALL_CONTRIB_DIR)/libdlmalloc
-	$(PRINT_INSTALL) E-ACSL scripts
-	$(MKDIR) $(BINDIR)
-	$(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/
-	$(MKDIR) $(BASHCOMPDIR)
-	$(foreach file, $(EACSL_INSTALL_BASHCOMPS), \
-		$(CP) $(file) \
-		      $(addprefix $(BASHCOMPDIR)/,$(basename $(notdir $(file)))) \
-		&&) true
-	$(PRINT_INSTALL) E-ACSL man pages
-	$(MKDIR) $(MANDIR)/man1
-	$(CP) $(EACSL_INSTALL_MANPAGES) $(MANDIR)/man1/
-
-
-EACSL_INSTALLED_SCRIPTS=$(addprefix $(BINDIR)/,$(notdir $(EACSL_SCRIPTS)))
-
-EACSL_INSTALLED_BASHCOMPS=$(addprefix $(BASHCOMPDIR)/,$(basename $(notdir $(EACSL_BASHCOMPS))))
-
-EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES)))
-
-uninstall::
-	$(PRINT_RM) E-ACSL share files
-	$(RM) -r $(FRAMAC_DATADIR)/e-acsl
-	$(PRINT_RM) E-ACSL libraries
-	$(RM) -r $(EACSL_INSTALL_LIB_DIR)
-	$(PRINT_RM) E-ACSL scripts
-	$(RM) $(EACSL_INSTALLED_SCRIPTS)
-	$(RM) $(EACSL_INSTALLED_BASHCOMPS)
-	$(PRINT_RM) E-ACSL man pages
-	$(RM) $(EACSL_INSTALLED_MANPAGES)
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
-CONFIG_STATUS_DIR_DEP:=
-else
-CONFIG_STATUS_DIR:=$(E_ACSL_DIR)
-CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
-endif
-
-$(E_ACSL_DIR)/Makefile: $(E_ACSL_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
-	cd $(CONFIG_STATUS_DIR) && ./config.status
-
-#####################################
-# Doxygen                           #
-#####################################
-
-DOXYGEN = @DOXYGEN@
-doxygen:
-	if ! test $(DOXYGEN) = "no"; then \
-		$(DOXYGEN) $(E_ACSL_DIR)/doc/doxygen/doxygen.cfg ; \
-	else \
-		echo "Warning: Skip doxygen documentation: \
-Doxygen executable not found."; \
-	fi
-
-doc:: doxygen
-
-clean::
-	$(PRINT_RM) generated documentation
-	$(RM) $(E_ACSL_DIR)/doc/doxygen/html/*
-	$(RM) $(E_ACSL_DIR)/doc/code/*
-	$(RM) $(E_ACSL_DIR)/doc/doxygen/warn.log

src/plugins/instantiate/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-SRC_STRING:= \
-	mem_utils \
-	memcmp \
-	memcpy \
-	memmove \
-	memset
-SRC_STRING:=$(addprefix string/, $(SRC_STRING))
-
-SRC_STDLIB:= \
-	basic_alloc \
-	calloc \
-	free \
-	malloc
-SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB))
-
-###################
-# Plug-in Setting #
-###################
-
-PLUGIN_DIR ?= .
-PLUGIN_ENABLE := @ENABLE_INSTANTIATE@
-PLUGIN_NAME := Instantiate
-PLUGIN_EXTRA_DIRS:=\
-	string\
-	stdlib
-PLUGIN_CMI :=
-PLUGIN_CMO := \
-	options basic_blocks \
-	global_context instantiator_builder \
-	transform register \
-	$(SRC_STRING) \
-	$(SRC_STDLIB)
-
-PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-#PLUGIN_NO_DEFAULT_TEST := no
-PLUGIN_TESTS_DIRS := string stdlib options api plugin
-PLUGIN_DISTRIB_TESTS := \
-  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/oracle/* \
-    $(filter-out result oracle,$(dir)/*)) \
-  ) \
-  $(filter-out result oracle,tests/*)) \
-  $(foreach dir, tests $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/test_config)
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Instantiate_DIR)/Makefile: $(Instantiate_DIR)/Makefile.in \
-				$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/loop_analysis/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-PLUGIN_ENABLE:=@ENABLE_LOOP_ANALYSIS@
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-
-PLUGIN_NAME:= LoopAnalysis
-PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
-PLUGIN_CMI:= region_analysis_sig
-PLUGIN_DEPENDENCIES:= Eva
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
-PLUGIN_TESTS_DIRS:=loop_analysis
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(LoopAnalysis_DIR)/Makefile: $(LoopAnalysis_DIR)/Makefile.in \
-                         $(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/markdown-report/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_MDR@
-PLUGIN_NAME:=Markdown_report
-PLUGIN_HAS_META:=yes
-PLUGIN_GENERATED:=$(PLUGIN_DIR)/Markdown_report.mli
-PLUGIN_CMO:=\
-  sarif mdr_params parse_remarks md_gen sarif_gen mdr_register
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
-PLUGIN_DISTRIB_EXTERNAL:=\
- Makefile.in configure.ac configure share/acsl.xml META.in \
- eva_info.ml eva_info.mli
-PLUGIN_DEPFLAGS:= $(PLUGIN_DIR)/eva_info.mli $(PLUGIN_DIR)/eva_info.ml
-PLUGIN_TESTS_DIRS:= md sarif
-PLUGIN_DISTRIB_TESTS := \
-  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/oracle/* \
-    $(filter-out result oracle,$(dir)/*)) \
-  ) \
-  $(filter-out result oracle,tests/*)) \
-  $(foreach dir, tests $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/test_config)
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-ifneq (@ENABLE_MDR@,no)
-ifneq ($(ENABLE_EVA), no)
-byte:: $(PLUGIN_LIB_DIR)/top/eva_info.cmo $(PLUGIN_LIB_DIR)/top/eva_info.cmi
-opt:: $(PLUGIN_LIB_DIR)/top/eva_info.cmxs $(PLUGIN_LIB_DIR)/top/eva_info.cmi
-install::
-	$(MKDIR) $(PLUGIN_INSTALL_DIR)/top
-	$(CP) $(PLUGIN_LIB_DIR)/top/eva_info.cm* $(PLUGIN_INSTALL_DIR)/top
-
-$(PLUGIN_LIB_DIR)/top/eva_info.cm%: $(Markdown_report_DIR)/eva_info.cm%
-	$(MKDIR) $(dir $@)
-	$(CP) $< $@
-
-$(Markdown_report_DIR)/eva_info.cmo: BFLAGS+=-I $(Markdown_report_DIR)
-$(Markdown_report_DIR)/eva_info.cmx: OFLAGS+=-I $(Markdown_report_DIR)
-
-endif
-endif
-
-$(Markdown_report_DIR)/Markdown_report.mli: \
-  $(Markdown_report_DIR)/mdr_params.mli \
-  $(Markdown_report_DIR)/md_gen.mli \
-  $(Markdown_report_DIR)/Makefile
-	echo "module Mdr_params: sig" > $@
-	cat $(Markdown_report_DIR)/mdr_params.mli >> $@
-	echo "end" >> $@
-	echo "module Md_gen: sig" >> $@
-	cat $(Markdown_report_DIR)/md_gen.mli >> $@
-	echo "end" >> $@
-
-VERSION:=$(shell $(CAT) $(FRAMAC_SRC)/VERSION)
-
-$(Markdown_report_DIR)/META: $(Markdown_report_DIR)/META.in $(FRAMAC_SRC)/VERSION
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(SED) -e 's|@VERSION@|$(VERSION)|' $< > $@
-	$(CHMOD_RO) $@
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-ifeq ("@ENABLE_MDR@","yes")
-install::
-	$(PRINT_CP) $(FRAMAC_DATADIR)/Markdown_report
-	$(MKDIR) $(FRAMAC_DATADIR)/Markdown_report
-	$(CP) $(Markdown_report_DIR)/share/acsl.xml \
-              $(FRAMAC_DATADIR)/Markdown_report
-endif

src/plugins/nonterm/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-###################
-# Plug-in Setting #
-###################
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_NONTERM@
-PLUGIN_NAME:=Nonterm
-PLUGIN_CMO:= nonterm_run
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_DEPENDENCIES:=Eva
-#PLUGIN_NO_DEFAULT_TEST:=no
-PLUGIN_TESTS_DIRS:=nonterm
-PLUGIN_DISTRIB_TESTS := \
-  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/oracle/* \
-    $(filter-out result oracle,$(dir)/*)) \
-  ) \
-  $(filter-out result oracle,tests/*)) \
-  $(foreach dir, tests $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
-    $(dir)/test_config)
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Nonterm_DIR)/Makefile: $(Nonterm_DIR)/Makefile.in \
-                         $(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/obfuscator/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-PLUGIN_DIR ?=.
-
-PLUGIN_ENABLE:=@ENABLE_OBFUSCATOR@
-PLUGIN_NAME:=Obfuscator
-
-PLUGIN_CMO:= options \
-	obfuscator_kind \
-	dictionary \
-	obfuscate \
-	obfuscator_register
-
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_NO_TEST:=yes
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-# Regenerating the Makefile on need
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Obfuscator_DIR)/Makefile: $(Obfuscator_DIR)/Makefile.in \
-			$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/report/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-###################
-# Plug-in Setting #
-###################
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_REPORT@
-PLUGIN_NAME:=Report
-PLUGIN_CMO:= report_parameters scan dump csv classify register
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-#PLUGIN_NO_DEFAULT_TEST:=no
-PLUGIN_TESTS_DIRS:=report
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-ifeq ($(FRAMAC_INTERNAL),yes)
-# To allow testing with WP
-Report_DEFAULT_TESTS: create_share_link
-
-endif
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Report_DIR)/Makefile: $(Report_DIR)/Makefile.in \
-				$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/security_slicing/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_SECURITY_SLICING@
-PLUGIN_NAME:=Security_slicing
-PLUGIN_CMO:= security_slicing_parameters components
-PLUGIN_GUI_CMO:= register_gui
-PLUGIN_UNDOC:= analysis
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_NO_TEST:=yes
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-# Regenerating the Makefile on need
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Security_slicing_DIR)/Makefile: $(Security_slicing_DIR)/Makefile.in \
-				$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status  --file $@

src/plugins/server/Makefile.in

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-# Do not use ?= to initialize both below variables
-# (fixed efficiency issue, see GNU Make manual, Section 8.11)
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
-endif
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
-endif
-
-###################
-# Plug-in Setting #
-###################
-
-PLUGIN_DIR ?=.
-PLUGIN_ENABLE:=@ENABLE_SERVER@
-PLUGIN_NAME:=Server
-PLUGIN_CMO:= \
-	server_parameters \
-	jbuffer \
-	package \
-	data main request states \
-	server_doc \
-	server_batch \
-	server_socket \
-	kernel_ast \
-	kernel_main \
-	kernel_project \
-	kernel_properties
-
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_TESTS_DIRS := batch
-
-PLUGIN_REQUIRES:= yojson
-
-PLUGIN_UNDOC:= server_batch.ml server_zmq.ml server_socket.ml
-
-PLUGIN_GENERATED:= $(PLUGIN_DIR)/Server.mli
-
-##################
-# ZeroMQ Support #
-##################
-
-ifeq (@SERVER_ZMQ@,yes)
-PLUGIN_REQUIRES+= zmq
-PLUGIN_CMO+= server_zmq
-else
-PLUGIN_DISTRIB_EXTERNAL+= server_zmq.ml
-endif
-
-################
-# Generic part #
-################
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-##############
-# Server API #
-##############
-
-SERVER_API= \
-	package.mli \
-	jbuffer.mli \
-	data.mli \
-	request.mli \
-	states.mli \
-	main.mli \
-	kernel_main.mli \
-	kernel_ast.mli \
-	kernel_properties.mli
-
-define Capitalize
-$(shell printf "%s%s" \
-    $$($(ECHO) $(1) | cut -c 1 | tr '[:lower:]' '[:upper:]')
-    $$($(ECHO) $(1) | cut -c 2-))
-endef
-
-define ExportModule
-$(ECHO) "module $(call Capitalize, $(basename $(notdir $(1)))) : sig" >> $(2);
-$(ECHO) '# 1 "$(1)"' >> $(2);
-$(CAT) $(1) >> $(2);
-$(ECHO) "end" >> $(2);
-endef
-
-SERVER_MLI=$(addprefix $(Server_DIR)/, $(SERVER_API))
-
-$(Server_DIR)/Server.mli: $(Server_DIR)/Makefile $(SERVER_MLI)
-	$(PRINT_MAKING) $@ "from" $(SERVER_MLI)
-	$(RM) $@ $@.tmp
-	$(ECHO) "(* This file is generated. Do not edit. *)" >> $@.tmp
-	$(ECHO) "(** {b Server Public API} *)" >> $@.tmp
-	$(foreach file,$(SERVER_MLI),$(call ExportModule,$(file),$@.tmp))
-	$(CHMOD_RO) $@.tmp
-	$(MV) $@.tmp $@
-
-#####################################
-# Regenerating the Makefile on need #
-#####################################
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-$(Server_DIR)/Makefile: $(Server_DIR)/Makefile.in \
-	$(CONFIG_STATUS_DIR)/config.status
-	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@