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