diff --git a/.gitignore b/.gitignore
index aacaa22f30990e7a8d314cc19fa298718856ba74..d2b865233b33fa755b314335235c8f0c62992811 100644
--- a/.gitignore
+++ b/.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
diff --git a/Makefile b/Makefile
index 39951f046496d79fdd4333ad42ed245bb9599f80..1e7e0a9d5e4c82ca20c5aa331bf02a913a06075a 100644
--- a/Makefile
+++ b/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 #
diff --git a/share/Makefile.common b/share/Makefile.common
index c3f8cd6de2d6a6e10f0f5c0e8bc248c0c165f7ee..604c069a2d101c5e3b26d63abf92927a062fa098 100644
--- a/share/Makefile.common
+++ b/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"
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 12cd6881533fab745cae58091974daa54d1ca167..e3a8475d0da5176db1dea649cda72fb051e7f28a 100644
--- a/share/Makefile.config.in
+++ b/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 #
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
index 36a0d0fea55d9739f74326eaa35d4e634686bb60..d932f5a2f6da166f10144d7094a1c634d2fd892d 100644
--- a/src/kernel_internals/runtime/dump_config.ml
+++ b/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) ;
diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in
index f24f0a68b402a2001536851ab66a69522619754d..2889e6566f1ef4c84261db87794909a2b1c95ca4 100644
--- a/src/kernel_internals/runtime/fc_config.ml.in
+++ b/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)
diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli
index 5f6af30299f6eedebd81bb832c88680235b4d1b1..181574f0a5ac6f285b080e1ae2db76952393de3c 100644
--- a/src/kernel_internals/runtime/fc_config.mli
+++ b/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.
diff --git a/src/libraries/stdlib/dune b/src/libraries/stdlib/dune
deleted file mode 100644
index c79da3d5fd5daad3a75d158f4a5b9c3fcd4efff8..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/dune
+++ /dev/null
@@ -1,27 +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). ;;
-;; ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(rule
- (targets transitioning.ml)
- (deps transitioning.ml.in ../../../config.sed)
- (action (with-stdout-to transitioning.ml (run sed -f ../../../config.sed transitioning.ml.in)))
-)
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml
similarity index 100%
rename from src/libraries/stdlib/transitioning.ml.in
rename to src/libraries/stdlib/transitioning.ml
diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
deleted file mode 100644
index 944a500bab9091dba2766758958f44328e3e0196..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/Makefile.in
+++ /dev/null
@@ -1,169 +0,0 @@
-##########################################################################
-# #
-# 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
diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
deleted file mode 100644
index 3efa3bc692c896dae500621825880f7771866e8e..0000000000000000000000000000000000000000
--- a/src/plugins/dive/Makefile.in
+++ /dev/null
@@ -1,71 +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). #
-# #
-##########################################################################
-
-#######################
-# 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 $@
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
deleted file mode 100644
index 8bfa6aa9f51ab92b34b9ca2abd70cc564130bc97..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/Makefile.in
+++ /dev/null
@@ -1,588 +0,0 @@
-##########################################################################
-# #
-# 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
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
deleted file mode 100644
index 1243f1bb6bedf316c9d36d046e21dee5c5c7a2df..0000000000000000000000000000000000000000
--- a/src/plugins/instantiate/Makefile.in
+++ /dev/null
@@ -1,96 +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). #
-# #
-##########################################################################
-
-# 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 $@
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
deleted file mode 100644
index c0f1bcdcb41a35af74e2f88b87f9e0230457a27f..0000000000000000000000000000000000000000
--- a/src/plugins/loop_analysis/Makefile.in
+++ /dev/null
@@ -1,54 +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). #
-# #
-##########################################################################
-
-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 $@
diff --git a/src/plugins/markdown-report/Makefile.in b/src/plugins/markdown-report/Makefile.in
deleted file mode 100644
index 1319104e18fc93bb3628eb66df1c26e52f7754ac..0000000000000000000000000000000000000000
--- a/src/plugins/markdown-report/Makefile.in
+++ /dev/null
@@ -1,106 +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). #
-# #
-##########################################################################
-
-# 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
diff --git a/src/plugins/nonterm/Makefile.in b/src/plugins/nonterm/Makefile.in
deleted file mode 100644
index a45d5b990a5a9f948f6ebd1db46811a427c8c344..0000000000000000000000000000000000000000
--- a/src/plugins/nonterm/Makefile.in
+++ /dev/null
@@ -1,72 +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). #
-# #
-##########################################################################
-
-# 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 $@
diff --git a/src/plugins/obfuscator/Makefile.in b/src/plugins/obfuscator/Makefile.in
deleted file mode 100644
index 3fe4c0886d3640c5e3a99ac962ceff6b890c1416..0000000000000000000000000000000000000000
--- a/src/plugins/obfuscator/Makefile.in
+++ /dev/null
@@ -1,55 +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). #
-# #
-##########################################################################
-
-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 $@
diff --git a/src/plugins/report/Makefile.in b/src/plugins/report/Makefile.in
deleted file mode 100644
index 079eeda0df829b83f5fc48d24ec177b08ab74a48..0000000000000000000000000000000000000000
--- a/src/plugins/report/Makefile.in
+++ /dev/null
@@ -1,69 +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). #
-# #
-##########################################################################
-
-# 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 $@
diff --git a/src/plugins/security_slicing/Makefile.in b/src/plugins/security_slicing/Makefile.in
deleted file mode 100644
index 3eeab8cce57a6931a63613e3ba9309f530408741..0000000000000000000000000000000000000000
--- a/src/plugins/security_slicing/Makefile.in
+++ /dev/null
@@ -1,53 +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). #
-# #
-##########################################################################
-
-# 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 $@
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
deleted file mode 100644
index 943f93e2fe1ddb98ce547a23397196bcbab2a5e4..0000000000000000000000000000000000000000
--- a/src/plugins/server/Makefile.in
+++ /dev/null
@@ -1,130 +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). #
-# #
-##########################################################################
-
-# 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 $@
diff --git a/src/plugins/studia/Makefile.in b/src/plugins/studia/Makefile.in
deleted file mode 100644
index 49711fab8c04a5244d667aa4ed039293ee26ab36..0000000000000000000000000000000000000000
--- a/src/plugins/studia/Makefile.in
+++ /dev/null
@@ -1,64 +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). #
-# #
-##########################################################################
-
-# 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_STUDIA@
-PLUGIN_NAME:=Studia
-PLUGIN_CMO:= options writes reads studia_request
-PLUGIN_GUI_CMO:= studia_gui
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-PLUGIN_DEPENDENCIES:=Eva
-PLUGIN_NO_TEST:=no
-
-################
-# 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
-
-$(Studia_DIR)/Makefile: $(Studia_DIR)/Makefile.in \
- $(CONFIG_STATUS_DIR)/config.status
- cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
diff --git a/src/plugins/variadic/Makefile.in b/src/plugins/variadic/Makefile.in
deleted file mode 100644
index d1eb8663af0792793af4ca6100f175156d607270..0000000000000000000000000000000000000000
--- a/src/plugins/variadic/Makefile.in
+++ /dev/null
@@ -1,75 +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). #
-# #
-##########################################################################
-
-# 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_VARIADIC@
-PLUGIN_NAME := Variadic
-PLUGIN_CMI := format_types va_types
-PLUGIN_CMO := options extends environment replacements \
- format_string format_pprint format_typer format_parser \
- generic standard classify translate \
- register
-PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-#PLUGIN_NO_DEFAULT_TEST := no
-PLUGIN_TESTS_DIRS := declared defined known erroneous
-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
-
-$(Variadic_DIR)/Makefile: $(Variadic_DIR)/Makefile.in \
- $(CONFIG_STATUS_DIR)/config.status
- cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
deleted file mode 100644
index 6ce0a0bad6b5f612e8bb22abd87fe93f8eafe4a4..0000000000000000000000000000000000000000
--- a/src/plugins/wp/Makefile.in
+++ /dev/null
@@ -1,346 +0,0 @@
-##########################################################################
-# #
-# This file is part of WP plug-in of Frama-C. #
-# #
-# Copyright (C) 2007-2022 #
-# CEA (Commissariat a l'energie atomique et aux energies #
-# 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 ?=.
-
-ifneq ("$(FRAMAC_INTERNAL)","yes")
-include $(FRAMAC_SHARE)/Makefile.config
-endif
-
-# Resources Installation
-include $(PLUGIN_DIR)/share/Makefile.resources
-
-# Extension of the GUI for wp is compilable
-# only if gnomecanvas is available
-#ifeq ($(HAS_GNOMECANVAS),yes)
-PLUGIN_GUI_CMO:= \
- GuiConfig \
- GuiList \
- GuiSequent \
- GuiProver \
- GuiTactic \
- GuiProof \
- GuiComposer \
- GuiGoal \
- GuiSource \
- GuiPanel \
- GuiNavigator
-#endif
-
-PLUGIN_REQUIRES:= why3
-
-PLUGIN_ENABLE:=@ENABLE_WP@
-PLUGIN_NAME:=Wp
-PLUGIN_CMO:= \
- rformat wprop \
- wp_parameters wp_error \
- Why3Provers \
- Context Warning \
- dyncall ctypes clabels \
- AssignsCompleteness MemoryContext wpContext \
- LogicUsage RefUsage \
- Layout Region \
- RegionAnnot RegionAccess RegionDump RegionAnalysis \
- normAtLabels wpPropId \
- Lang Repr Matrix Passive Splitter \
- LogicBuiltins Definitions \
- Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
- Letify Cleaning \
- Mstate Conditions \
- Filtering \
- Plang Pcfg Pcond \
- CodeSemantics \
- LogicCompiler \
- LogicSemantics LogicAssigns \
- Sigma MemLoader MemDebug \
- MemEmpty MemZeroAlias MemVar \
- MemMemory MemTyped MemRegion MemVal \
- wpReached wpRTE wpTarget \
- CfgCompiler StmtSemantics \
- VCS script wpo wpReport \
- Footprint Tactical Strategy \
- TacClear TacSplit TacChoice TacRange TacInduction \
- TacArray TacCompound TacUnfold \
- TacHavoc TacInstance TacLemma \
- TacFilter TacCut WpTac TacNormalForm \
- TacRewrite TacBitwised TacBitrange TacBittest TacModMask TacShift \
- TacSequence \
- TacCongruence TacOverflow Auto \
- ProofSession ProofScript ProofEngine \
- ProverTask \
- filter_axioms Cache ProverWhy3 \
- driver prover ProverSearch ProverScript \
- Factory \
- cfgInit cfgAnnot cfgInfos cfgCalculus \
- cfgDump cfgWP \
- cfgGenerator \
- Generator register VC
-
-PLUGIN_CMI:= \
- Sigs mcfg
-
-PLUGIN_GENERATED:= \
- $(PLUGIN_DIR)/script.ml \
- $(PLUGIN_DIR)/rformat.ml \
- $(PLUGIN_DIR)/driver.ml \
- $(PLUGIN_DIR)/Wp.mli
-
-PLUGIN_DEPENDENCIES:= rtegen qed
-PLUGIN_UNDOC+=
-PLUGIN_INTRO:=$(PLUGIN_DIR)/intro_wp.txt
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= \
- Changelog \
- Makefile.in \
- MakeAPI \
- configure.ac \
- configure \
- $(addprefix share/, $(ALL_CEA_RESOURCES) \
- $(ALL_UNMODIFIED_WHY3_RESOURCES) \
- $(ALL_MODIFIED_WHY3_RESOURCES))
-
-CEA_WP_GENEREATED= script.ml rformat.ml driver.ml
-
-# --------------------------------------------------------------------------
-# --- Tests ---
-# --------------------------------------------------------------------------
-
-PLUGIN_TESTS_DIRS:= \
- why3 wp wp_plugin wp_acsl wp_bts \
- wp_store wp_hoare wp_typed wp_usage \
- wp_gallery wp_manual wp_tip \
- wp_region
-
-ifeq ($(FRAMAC_INTERNAL),yes)
-Wp_DEFAULT_TESTS: create_share_link
-endif
-
-# --------------------------------------------------------------------------
-# --- Dynamic Plugin ---
-# --------------------------------------------------------------------------
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-# Regenerating the Makefile on need
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
-CONFIG_STATUS_DIR=$(FRAMAC_SRC)
-else
-CONFIG_STATUS_DIR=.
-endif
-
-WP_CONFIGURE_MAKEFILE= \
- $(Wp_DIR)/Makefile.in \
- $(Wp_DIR)/share/Makefile.resources \
- $(CONFIG_STATUS_DIR)/config.status
-
-$(Wp_DIR)/Makefile: $(WP_CONFIGURE_MAKEFILE)
- @cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
-
-# --------------------------------------------------------------------------
-# --- Qualif Tests ---
-# --------------------------------------------------------------------------
-
-.PHONY: wp-qualif wp-qualif-update wp-qualif-upgrade wp-qualif-push wp-qualif-status
-
-WP_QUALIF_CACHE?=$(abspath $(Wp_DIR)/../wp-cache)
-WP_QUALIF_ENTRIES=git -C $(WP_QUALIF_CACHE) ls-files --others --exclude-standard | wc -l
-
-WP_CHECKOUT_CACHE=\
- echo "[CACHE] repo: $(WP_QUALIF_CACHE)" && \
- git -C $(WP_QUALIF_CACHE) checkout master
-
-wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
- $(WP_CHECKOUT_CACHE)
- FRAMAC_WP_CACHE=replay \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
-
-WP_PULL_CACHE=\
- echo "[CACHE] pull cache" && \
- $(WP_CHECKOUT_CACHE) && \
- git -C $(WP_QUALIF_CACHE) pull --rebase --prune
-
-wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
- $(WP_PULL_CACHE)
- @echo "[TESTS] updating wp-qualif"
- FRAMAC_WP_CACHE=update \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif
- @echo "[CACHE] cache status"
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
- $(WP_PULL_CACHE)
- @echo "[TESTS] upgrading wp-qualif (cache & scripts)"
- FRAMAC_WP_CACHE=update \
- FRAMAC_WP_SCRIPT=update \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif
- @echo "[CACHE] cache status"
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-wp-qualif-push:
- @echo "[CACHE] pushing updates"
- $(WP_CHECKOUT_CACHE)
- git -C $(WP_QUALIF_CACHE) add -A
- git -C $(WP_QUALIF_CACHE) commit -m "[wp] cache updates"
- git -C $(WP_QUALIF_CACHE) push -f
-
-wp-qualif-status:
- @echo "[CACHE] status"
- $(WP_CHECKOUT_CACHE)
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-$(WP_QUALIF_CACHE):
- @echo "[CACHE] cloning wp global at $(WP_QUALIF_CACHE)..."
- @echo "Use env. variable WP_QUALIF_CACHE to change this location."
- @git clone "git@git.frama-c.com:frama-c/wp-cache.git" $(WP_QUALIF_CACHE)
-
-# --------------------------------------------------------------------------
-# --- WP API ---
-# --------------------------------------------------------------------------
-
-WP_API_BASE= \
- wp_parameters.mli \
- ctypes.mli clabels.mli \
- MemoryContext.mli \
- LogicUsage.mli RefUsage.mli \
- normAtLabels.mli \
- wpPropId.mli mcfg.mli \
- Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
- Lang.mli Repr.mli Passive.mli Splitter.mli \
- LogicBuiltins.mli Definitions.mli \
- Cint.mli Cfloat.mli Vset.mli Cstring.mli \
- Sigs.mli Mstate.mli Conditions.mli Filtering.mli \
- Plang.mli Pcfg.mli Pcond.mli \
- CodeSemantics.mli \
- LogicCompiler.mli LogicSemantics.mli \
- Sigma.mli MemVar.mli MemTyped.mli MemVal.mli \
- CfgCompiler.mli StmtSemantics.mli \
- Factory.mli driver.mli VCS.mli Tactical.mli Strategy.mli Auto.mli \
- VC.mli wpo.mli ProverTask.mli prover.mli
-
-define WP_capitalize
-$(shell printf "%s%s" \
- $$($(ECHO) $(1) | cut -c 1 | tr '[:lower:]' '[:upper:]')
- $$($(ECHO) $(1) | cut -c 2-))
-endef
-
-define WP_export
-$(ECHO) "module $(call WP_capitalize, $(basename $(notdir $(1)))) : sig" >> $(2);
-$(ECHO) '# 1 "$(1)"' >> $(2);
-$(CAT) $(1) >> $(2);
-$(ECHO) "end" >> $(2);
-endef
-
-WP_MLI=$(addprefix $(Wp_DIR)/, $(WP_API_BASE))
-
-$(Wp_DIR)/Wp.mli: $(Wp_DIR)/Makefile $(WP_MLI)
- $(PRINT_MAKING) $@
- $(RM) $@ $@.tmp
- $(ECHO) "(* This file is generated. Do not edit. *)" > $@.tmp
- $(ECHO) "(** {b WP Public API} *)" > $@.tmp
- $(foreach file,$(WP_MLI),$(call WP_export,$(file),$@.tmp))
- $(CHMOD_RO) $@.tmp
- $(MV) $@.tmp $@
-
-.PHONY: wp-doc-api
-
-wp-doc-api:
- $(ECHO) "Generating WP documentation"
- @mkdir -p $(Wp_DIR)/doc/html
- $(RM) -fr $(Wp_DIR)/doc/html/*
- $(CP) $(Wp_DIR)/doc/ocamldoc.css $(Wp_DIR)/doc/html/style.css
- $(OCAMLDOC) \
- -package zarith \
- -package why3 \
- -I lib/fc -I lib/plugins -I $(Wp_DIR) -stars \
- -html -d $(Wp_DIR)/doc/html -charset utf-8 \
- -t "Frama-C/WP API Documentation" \
- -intro $(Wp_DIR)/doc/wp-api.odoc \
- -colorize-code -short-functors $(Wp_DIR)/Wp.mli
- $(ECHO) "Generating $(Wp_DIR)/doc/html/index.html"
-
-clean::
- $(RM) $(Wp_DIR)/Wp.mli
- $(RM) -fr $(Wp_DIR)/doc/html
-
-# --------------------------------------------------------------------------
-# --- Installation Resources
-# --------------------------------------------------------------------------
-
-## All relative to share/
-
-ALL_WHY3_SOURCES= $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
-
-ALL_RESOURCES= \
- wp.driver \
- $(ALL_WHY3_SOURCES)
-
-INSTALL_OPT?=
-INSTALL_SHARE=@$(Wp_DIR)/share/instwp $(INSTALL_OPT)
-
-byte:: $(Wp_DIR)/share/instwp
-opt:: $(Wp_DIR)/share/instwp
-clean::
- rm -f $(Wp_DIR)/share/instwp
- rm -f $(Wp_DIR)/share/install.cm*
-
-$(Wp_DIR)/share/instwp: $(Wp_DIR)/share/install.ml
- $(OCAMLC) $(WARNINGS) -w -70 -o $@ unix.cma $^
-
-# --------------------------------------------------------------------------
-# --- Installation ---
-# --------------------------------------------------------------------------
-
-install:: clean-install
- $(PRINT_INSTALL) WP shared files
- $(MKDIR) $(FRAMAC_DATADIR)/wp
- $(INSTALL_SHARE) -p \
- -i $(Wp_DIR)/share \
- -d $(FRAMAC_DATADIR)/wp \
- $(ALL_RESOURCES) -f -b
-
-uninstall::
- $(PRINT_RM) WP shared files
- $(RM) -r $(FRAMAC_DATADIR)/wp
-
-# --------------------------------------------------------------------------
-# --- WP Release Stuff (CEA-LIST Only)
-# --------------------------------------------------------------------------
-sinclude MakeDistrib
-# --------------------------------------------------------------------------
-
-$(Wp_DIR)/.depend: $(Wp_DIR)/driver.mll
-$(Wp_DIR)/driver.mll: $(Wp_DIR)/Makefile