diff --git a/.gitignore b/.gitignore
index 44f7cfb3f2b3a1c247c6a94552eb8076c32a208a..0c9a3ffad1279180824a46972c05496b083c2975 100644
--- a/.gitignore
+++ b/.gitignore
@@ -202,7 +202,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 2a718c040cda65ea12cdd7ccd31662c34df0b327..41c1b6b039f502b6045a85fae1d8efcba55e3e92 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
-
DUNE_BUILD_OPTS?=
RELEASE?=no
@@ -64,81 +57,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/VERSION b/VERSION
index be8e64f5a38cfeb3e1c58884871821fdedcf09c7..e395c9270cf14da055f641dbad906e581e6d33c7 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-25.0
+25.0+dev
diff --git a/opam/opam b/opam/opam
index d695a2b519994c3aefd5ad145ee454344922168c..8d9d456ce0ba2e92a52273b9f7a1eba376e00a7e 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "25.0~beta"
+version: "25.0+dev"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -68,7 +68,7 @@ authors: [
homepage: "https://frama-c.com/"
license: "LGPL-2.1-only"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-25.0-beta-Manganese.pdf"
+doc: "http://frama-c.com/download/user-manual-25.0-Manganese.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
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/from/callwise.ml b/src/plugins/from/callwise.ml
index 4891f63d8760583be27bb554abdaccb5c4690a77..f1119b1bed4377aa39a0f9a4b5cc69552238a4de 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -64,9 +64,9 @@ let record_callwise_dependencies_in_db call_site froms =
Tbl.replace call_site (Function_Froms.join previous froms)
with Not_found -> Tbl.add call_site froms
-let call_for_individual_froms (call_type, value_initial_state, call_stack) =
+let call_for_individual_froms callstack _kf call_type value_initial_state =
if From_parameters.ForceCallDeps.get () then begin
- let current_function, call_site = List.hd call_stack in
+ let current_function, call_site = List.hd callstack in
let register_from froms =
record_callwise_dependencies_in_db call_site froms;
match !call_froms_stack with
@@ -151,15 +151,13 @@ let compute_call_from_value_states current_function states =
Callwise_Froms.compute_and_return current_function
-let record_for_individual_froms (call_stack, value_res) =
+let record_for_individual_froms callstack cur_kf value_res =
if From_parameters.ForceCallDeps.get () then begin
let froms = match value_res with
- | Value_types.Normal (states, _after_states)
- | Value_types.NormalStore ((states, _after_states), _) ->
- let cur_kf, _ = List.hd call_stack in
+ | Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let froms =
if Eva.Analysis.save_results cur_kf
- then compute_call_from_value_states cur_kf (Lazy.force states)
+ then compute_call_from_value_states cur_kf (Lazy.force before_stmts)
else Function_Froms.top
in
let pre_state = match !call_froms_stack with
@@ -168,28 +166,21 @@ let record_for_individual_froms (call_stack, value_res) =
in
if From_parameters.VerifyAssigns.get () then
!Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
- (match value_res with
- | Value_types.NormalStore (_, memexec_counter) ->
- MemExec.replace memexec_counter froms
- | _ -> ());
+ MemExec.replace memexec_counter froms;
froms
- | Value_types.Reuse counter ->
+ | Reuse counter ->
MemExec.find counter
in
- end_record call_stack froms
+ end_record callstack froms
end
(* Register our callbacks inside the value analysis *)
-let () = From_parameters.ForceCallDeps.add_update_hook
- (fun _bold bnew ->
- if bnew then begin
- Db.Value.Call_Type_Value_Callbacks.extend_once call_for_individual_froms;
- Db.Value.Record_Value_Callbacks_New.extend_once
- record_for_individual_froms;
- end)
+let () =
+ Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms;
+ Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms
let force_compute_all_calldeps ()=
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d0abe639b314d4f961eb13f6b8ca70aa8bb15206..632d4a4bd1a12115325af5944788a0bf50df5447 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -587,11 +587,10 @@ module Callwise = struct
let call_inout_stack = ref []
- let call_for_callwise_inout (call_type, state, call_stack) =
- let (current_function, ki as call_site) = List.hd call_stack in
+ let call_for_callwise_inout callstack _kf call_type state =
+ let (current_function, ki as call_site) = List.hd callstack in
let merge_inout inout =
- Db.Operational_inputs.Record_Inout_Callbacks.apply
- (call_stack, inout);
+ Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
if ki = Kglobal
then merge_call_in_global_tables call_site inout
else
@@ -698,35 +697,30 @@ module Callwise = struct
in
Computer.end_dataflow ()
- let record_for_callwise_inout ((call_stack: Db.Value.callstack), value_res) =
+ let record_for_callwise_inout callstack kf value_res =
let inout = match value_res with
- | Value_types.Normal (states, _after_states)
- | Value_types.NormalStore ((states, _after_states), _) ->
- let kf, _ = List.hd call_stack in
+ | Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let inout =
if Eva.Analysis.save_results kf
- then compute_call_from_value_states kf call_stack (Lazy.force states)
+ then
+ let cvalue_states = Lazy.force before_stmts in
+ compute_call_from_value_states kf callstack cvalue_states
else top
in
- (match value_res with
- | Value_types.NormalStore (_, memexec_counter) ->
- MemExec.replace memexec_counter inout
- | _ -> ());
+ MemExec.replace memexec_counter inout;
inout
-
- | Value_types.Reuse counter ->
+ | Reuse counter ->
MemExec.find counter
in
- Db.Operational_inputs.Record_Inout_Callbacks.apply
- (call_stack, inout);
- end_record call_stack inout
+ Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
+ end_record callstack inout
(* Register our callbacks inside the value analysis *)
let () =
- Db.Value.Record_Value_Callbacks_New.extend_once record_for_callwise_inout;
- Db.Value.Call_Type_Value_Callbacks.extend_once call_for_callwise_inout;;
+ Eva.Cvalue_callbacks.register_call_results_hook record_for_callwise_inout;
+ Eva.Cvalue_callbacks.register_call_hook call_for_callwise_inout
end
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/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index e630950b1fd2fbcc3a0dea44b31d44f218c9b301..c5682f2f8573b010bd44f8954b5cf7862387c71c 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -265,14 +265,12 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let arguments = compute_arguments call.arguments call.rest in
try
let call_result = builtin pre arguments in
- let call_stack = Eva_utils.call_stack () in
let froms =
match call_result with
| Full result -> `Builtin result.c_from
- | States _ -> `Builtin None
- | Result _ -> `Spec (Annotations.funspec call.kf)
+ | States _ | Result _ -> `Builtin None
in
- Db.Value.Call_Type_Value_Callbacks.apply (froms, pre, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf froms pre;
process_result call post call_result
with
| Invalid_nb_of_args n ->
diff --git a/src/plugins/value/dune b/src/plugins/value/dune
index bbb46ac8f0c97ac0a9b5311d684e52cfb0fff49b..d0285778cc47660df0c498af1f40fde13967ba14 100644
--- a/src/plugins/value/dune
+++ b/src/plugins/value/dune
@@ -65,6 +65,7 @@
builtins_watchpoint
compute_functions
cvalue_backward
+ cvalue_callbacks
cvalue_domain
cvalue_forward
cvalue_init
@@ -165,7 +166,7 @@
(deps
gen-api.sh Eva.ml.in Eva.mli.in
engine/analysis.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli
- domains/cvalue/builtins.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
+ domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
)
(action (run %{deps}))
)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index ac17b268d15e9a6f9819f355b847fbbe84907786..530750b8893c46895e211c3303d70ac4b1a202de 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -184,9 +184,8 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack = Eva_utils.call_stack () in
let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
- Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf `Memexec cvalue;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
@@ -202,7 +201,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Self.debug ~dkey
"calling Record_Value_New callbacks on saved previous result";
end;
- Db.Value.Record_Value_Callbacks_New.apply (stack, Value_types.Reuse i);
+ let reuse = Cvalue_callbacks.Reuse i in
+ Cvalue_callbacks.apply_call_results_hooks call.callstack call.kf reuse;
(* call can be cached since it was cached once *)
Transfer.{states; cacheable = Cacheable; builtin=false}
@@ -234,11 +234,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_using_spec_or_body target kinstr call state =
let global = match kinstr with Kglobal -> true | _ -> false in
let pp = not global && Parameters.ValShowProgress.get () in
- let call_stack = Eva_utils.call_stack () in
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
- Value_types.Callstack.pretty_short call_stack
+ Value_types.Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let compute, kind =
@@ -248,7 +247,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Spec funspec ->
compute_using_spec funspec, `Spec funspec
in
- Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let resulting_states, cacheable = compute kinstr call state in
if pp then
Self.feedback
@@ -293,8 +292,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
- let cs = Eva_utils.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
+ let kind = `Spec spec in
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
@@ -352,9 +351,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute () =
Eva_utils.push_call_stack kf Kglobal;
store_initial_state kf init_state;
- let call =
- { kf; callstack = []; arguments = []; rest = []; return = None; }
- in
+ let callstack = [kf, Kglobal] in
+ let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 3be91801bcbca06a175e6401925edbe0caf4568e..2fc4a8215b03a066dee2e8499146a89fe38660b4 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -448,8 +448,8 @@ module Make_Dataflow
(* TODO: apply on all domains. *)
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
- Db.Value.Compute_Statement_Callbacks.apply
- (stmt, Eva_utils.call_stack (), cvalue_states)
+ let callstack = Eva_utils.call_stack () in
+ Cvalue_callbacks.apply_statement_hooks callstack stmt cvalue_states
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
@@ -723,21 +723,12 @@ module Make_Dataflow
Db.Value.Record_Value_Callbacks.apply
(callstack, merged_pre_cvalues)
end;
- if not (Db.Value.Record_Value_Callbacks_New.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value_New callbacks";
- if Parameters.MemExecAll.get () then
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.NormalStore ((merged_pre_cvalues, merged_post_cvalues),
- (Mem_exec.new_counter ())))
- else
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.Normal (merged_pre_cvalues, merged_post_cvalues))
- end;
+ let states =
+ Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
+ after_stmts = merged_post_cvalues }
+ in
+ let results = Cvalue_callbacks.Store (states, Mem_exec.new_counter ()) in
+ Cvalue_callbacks.apply_call_results_hooks callstack kf results;
if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
then begin
if Parameters.ValShowProgress.get () then
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 9134b02da047024d6cc98b06eceb891721f6108c..fb0da4b9b937d09ce4fa8aac3de912354e5851ab 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -179,7 +179,7 @@ let make_recursion call depth =
let make call =
let is_same_kf (f, _) = Kernel_function.equal f call.kf in
let previous_calls = List.filter is_same_kf call.callstack in
- let depth = List.length previous_calls in
+ let depth = List.length previous_calls - 1 in
if depth > 0
then Some (make_recursion call depth)
else None
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 303e69ee16dde632435d82c0f774c42a3d3b122a..09bcb4f40fc720fe7c09bcbe9c2692eb2c10fc34 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -531,9 +531,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------- Make an Eval.call ---------------------------- *)
(* Create an Eval.call *)
- let create_call kf args =
+ let create_call stmt kf args =
let return = Library_functions.get_retres_vi kf in
- let callstack = Eva_utils.call_stack () in
+ let callstack = (kf, Kstmt stmt) :: Eva_utils.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -572,12 +572,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.map replace_arg call.arguments in
{ call with arguments; }
- let make_call ~subdivnb kf arguments valuation state =
+ let make_call ~subdivnb stmt kf arguments valuation state =
(* Evaluate the arguments of the call. *)
let determinate = is_determinate kf in
compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
- let call = create_call kf args in
+ let call = create_call stmt kf args in
let recursion = Recursion.make call in
let call = Extlib.opt_fold replace_recursive_call recursion call in
call, recursion, valuation
@@ -731,9 +731,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Eva_utils.call_stack ()) cvalue_state;
- Db.Value.Call_Type_Value_Callbacks.apply
- (`Builtin None, cvalue_state, stack_with_call)
-
+ let kind = `Builtin None in
+ Cvalue_callbacks.apply_call_hooks stack_with_call kf kind cvalue_state
(* --------------------- Process the call statement ---------------------- *)
@@ -756,7 +755,7 @@ module Make (Abstract: Abstractions.Eva) = struct
[(Partition.Key.empty, state)]
else
(* Create the call. *)
- let eval, alarms = make_call ~subdivnb kf args valuation state in
+ let eval, alarms = make_call ~subdivnb stmt kf args valuation state in
Alarmset.emit ki_call alarms;
let states =
let+ call, recursion, valuation = eval in
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 76f96cf20bc10c0f141cb2ac03e1448bd620c1b8..c0335e7761b4eb99e365b9775c9ceb7061e78fc5 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -238,7 +238,7 @@ type callstack = call_site list
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
callstack: callstack; (** The current callstack
- (without this call). *)
+ (with this call on top). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
diff --git a/src/plugins/value/utils/cvalue_callbacks.ml b/src/plugins/value/utils/cvalue_callbacks.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9a8be4126b2789f785ffa29ab9434238264a5cfd
--- /dev/null
+++ b/src/plugins/value/utils/cvalue_callbacks.ml
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+let dkey = Self.dkey_callbacks
+
+type callstack = (kernel_function * kinstr) list
+type state = Cvalue.Model.t
+
+type analysis_kind =
+ [ `Builtin of Value_types.call_froms
+ | `Spec of funspec
+ | `Def
+ | `Memexec ]
+
+module Call =
+ Hook.Build
+ (struct type t = callstack * kernel_function * analysis_kind * state end)
+
+let register_call_hook f =
+ Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
+
+let apply_call_hooks callstack kf kind state =
+ Call.apply (callstack, kf, kind, state);
+ Db.Value.Call_Type_Value_Callbacks.apply (kind, state, callstack)
+
+
+type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
+type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
+
+type call_results =
+ | Store of results * int
+ | Reuse of int
+
+module Call_Results =
+ Hook.Build (struct type t = callstack * kernel_function * call_results end)
+
+let register_call_results_hook f =
+ Call_Results.extend (fun (callstack, kf, results) -> f callstack kf results)
+
+let apply_call_results_hooks callstack kf call_results =
+ if Parameters.ValShowProgress.get ()
+ && not (Call_Results.is_empty ()
+ && Db.Value.Record_Value_Callbacks_New.is_empty ())
+ then Self.debug ~dkey "now calling Call_Results callbacks";
+ Call_Results.apply (callstack, kf, call_results);
+ let results =
+ match call_results with
+ | Reuse i -> Value_types.Reuse i
+ | Store ({before_stmts; after_stmts}, i) ->
+ Value_types.NormalStore ((before_stmts, after_stmts), i)
+ in
+ Db.Value.Record_Value_Callbacks_New.apply (callstack, results)
+
+
+module Statement =
+ Hook.Build (struct type t = callstack * stmt * state list end)
+
+let register_statement_hook f =
+ Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
+
+let apply_statement_hooks callstack stmt states =
+ Statement.apply (callstack, stmt, states);
+ Db.Value.Compute_Statement_Callbacks.apply (stmt, callstack, states)
diff --git a/src/plugins/value/utils/cvalue_callbacks.mli b/src/plugins/value/utils/cvalue_callbacks.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cb26f37aa10beb18fff6f8edc4f9e4eaff19445c
--- /dev/null
+++ b/src/plugins/value/utils/cvalue_callbacks.mli
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+[@@@ api_start]
+
+(** Register actions to performed during the Eva analysis,
+ with access to the states of the cvalue domain. *)
+
+type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+type state = Cvalue.Model.t
+
+type analysis_kind =
+ [ `Builtin of Value_types.call_froms
+ | `Spec of Cil_types.funspec
+ | `Def
+ | `Memexec ]
+
+(** Registers a function to be applied at the beginning of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called, the kind of analysis performed by Eva for this call,
+ and the cvalue state at the beginning of the call. *)
+val register_call_hook:
+ (callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
+ -> unit
+
+
+type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
+type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
+
+(** Results of a function call. *)
+type call_results =
+ | Store of results * int
+ (** Cvalue states before and after each statement of the given function,
+ plus a unique integer id for the call. *)
+ | Reuse of int
+ (** The results are the same as a previous call with the given integer id,
+ previously recorded with the [Store] constructor. *)
+
+(** Registers a function to be applied at the end of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called and the cvalue states resulting from its analysis. *)
+val register_call_results_hook:
+ (callstack -> Cil_types.kernel_function -> call_results -> unit)
+ -> unit
+
+[@@@ api_end]
+
+val register_statement_hook:
+ (callstack -> Cil_types.stmt -> state list -> unit) -> unit
+
+val apply_call_hooks:
+ callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit
+val apply_call_results_hooks:
+ callstack -> Cil_types.kernel_function -> call_results -> unit
+val apply_statement_hooks:
+ callstack -> Cil_types.stmt -> state list -> unit
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
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index c5d23a2cbd6870325adf211e6bde1b09c99cfab4..aac1b7410d2177b68888a0a52de635a1bc3bc49b 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -228,16 +228,16 @@
[kernel] imprecise.c:114: approximating value to write.
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes
-[kernel] imprecise.c:111:
- more than 200(300) elements to enumerate. Approximating.
-[kernel] imprecise.c:114:
- more than 200(300) elements to enumerate. Approximating.
[from] Computing for function many_writes
[kernel] imprecise.c:111:
more than 200(300) dependencies to update. Approximating.
[kernel] imprecise.c:114:
more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes
+[kernel] imprecise.c:111:
+ more than 200(300) elements to enumerate. Approximating.
+[kernel] imprecise.c:114:
+ more than 200(300) elements to enumerate. Approximating.
[eva] Done for function many_writes
[eva] computing for function overlap <- main.
Called from imprecise.c:151.
diff --git a/tests/builtins/oracle_equality/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle
index 1671979a21da9093f750711b69ddf89ae1266418..b06a17f898d8a32e07efd66bfb840b4f06213b94 100644
--- a/tests/builtins/oracle_equality/imprecise.res.oracle
+++ b/tests/builtins/oracle_equality/imprecise.res.oracle
@@ -4,11 +4,11 @@
220a223,224
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d232
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a233,234
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d242
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a235,236
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_octagon/imprecise.res.oracle b/tests/builtins/oracle_octagon/imprecise.res.oracle
index 86e47c5ed0f3386d84358609df6e197296d4fdb8..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_octagon/imprecise.res.oracle
+++ b/tests/builtins/oracle_octagon/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d230
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a231,232
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a233,234
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/imprecise.res.oracle b/tests/builtins/oracle_symblocs/imprecise.res.oracle
index 86e47c5ed0f3386d84358609df6e197296d4fdb8..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_symblocs/imprecise.res.oracle
+++ b/tests/builtins/oracle_symblocs/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d230
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a231,232
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a233,234
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/value/oracle/replace_by_show_each.res.oracle b/tests/value/oracle/replace_by_show_each.res.oracle
index 85c7d6b9a717f017cf2449e736a7764c00f81c4d..18b7f724883947d6e3ec4f3e8844af1540c495fc 100644
--- a/tests/value/oracle/replace_by_show_each.res.oracle
+++ b/tests/value/oracle/replace_by_show_each.res.oracle
@@ -6,10 +6,10 @@
x ∈ {0}
[eva] replace_by_show_each.c:23: Frama_C_show_each_2:
[eva] replace_by_show_each.c:25: Frama_C_show_each_1:
-[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
- Results will be imprecise.
[from] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise.
+[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
+ Results will be imprecise.
[eva:alarm] replace_by_show_each.c:26: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
[eva] Recording results for main