diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 6f12194ddbc0198d72df30192cb7f036339c617c..783ae829a3b230198fe7b60f7acb5bf0b386e4d8 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -48,7 +48,6 @@
/doc/userman/*.idx
/doc/userman/*.log
/doc/userman/*.lof
-/doc/userman/eacslversion.tex
/tests/*/result*/*
.frama-c
META.frama-c-e_acsl
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index d8870d5d675330af434e4497703f6dcdb3ce0f41..3800b3eef5d60b4ae1b22d86f29dde339e274981 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
###############################################################################
+-! E-ACSL [2024-04-04] remove option -e-acsl-version.
+
###############################################################################
Plugin E-ACSL 28.1 (Nickel)
###############################################################################
diff --git a/src/plugins/e-acsl/doc/Makefile.common b/src/plugins/e-acsl/doc/Makefile.common
index 721db0214d0c22fd6a818762b8585e84d92bfd5a..9174cb553500a2404a25f44f0e56b763423b154c 100644
--- a/src/plugins/e-acsl/doc/Makefile.common
+++ b/src/plugins/e-acsl/doc/Makefile.common
@@ -2,9 +2,6 @@
VERSION_FILE=$(wildcard ../../../../../VERSION)
CODENAME_FILE=$(wildcard ../../../../../VERSION_CODENAME)
-EACSL_VERSION=$(shell cat $(VERSION_FILE))
-EACSL_CODENAME=$(shell cat $(CODENAME_FILE))
-FC_VERSION=$(shell cat $(VERSION_FILE))
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
@@ -12,14 +9,6 @@ include $(EACSL_DIR)/doc/support/MakeLaTeXModern
# Generic rules #
#################
-eacslversion.tex: Makefile $(VERSION_FILE) $(CODENAME_FILE)
- rm -f $@
- printf '\\newcommand{\\eacslpluginversion}{$(EACSL_VERSION)\\xspace}\n' > $@
- printf '\\newcommand{\\eacslplugincodename}{$(EACSL_CODENAME)\\xspace}\n' >> $@
- printf '\\newcommand{\\framacversion}{$(FC_VERSION)\\xspace}\n' >> $@
- printf '\\fcversion{\\framacversion}\n' >> $@
- chmod a-w $@
-
%.1: %.mp
mpost -interaction=batchmode $<
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index 6ab09b0f9a2d0ed039249502d7cae4f0c19ffd42..cf93cfc14764d31ce92f0d2d1e0a15ec5b620244 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -3,7 +3,6 @@ eu-flag.jpg
frama-c-book.cls
e-acsl.pdf
e-acsl-implementation.pdf
-eacslversion.tex
fc-macros.tex
logos
*.fls
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 961f6fe09ec4ba3fcedf46c9a869f5aa369181f9..93b96efb202ebb952407ef399ab1bfa1b1d9ff69 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -8,7 +8,7 @@ include $(EACSL_DIR)/doc/Makefile.common
##########
MAIN=main
-DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
+DEPS_MODERN=macros_modern.tex biblio.bib \
intro_modern.tex speclang_modern.tex \
libraries_modern.tex concl_modern.tex changes_modern.tex \
term_modern.bnf binders_modern.bnf predicate_modern.bnf \
@@ -21,7 +21,8 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
higherorder_modern.bnf logictypedecl_modern.bnf logicreads_modern.bnf \
allocation_modern.bnf abrupt_modern.bnf dependencies_modern.bnf \
volatile-gram_modern.bnf \
- bsearch.c bsearch2.c link.c
+ bsearch.c bsearch2.c link.c \
+ $(VERSION_FILE)
##############
# Main rules #
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 67f698182412223e3aa480d0380c5b2c81f368f1..3146f0a1d6f6b525eae48ced3c6f5eb684b92693 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -190,9 +190,9 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
% Next version
-%\subsection*{Version \eacslplugincodename-\eacslpluginversion}
+%\subsection*{Version Frama-C+dev}
-\subsection*{Version \eacslplugincodename-\eacslpluginversion}
+\subsection*{Version Chrome-24}
\begin{itemize}
\item \changeinsection{higherorder}{support for \lstinline|\\sum|,
\lstinline|\\prod|, and \lstinline|\\numof|}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index 3e816ad9239fb352d2bc753276f595603fa0b819..a6a7ff005ed0f04ecc9553f8c814788d6c4291e3 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -4,7 +4,7 @@
This document is a reference manual for
\ifthenelse{\boolean{PrintImplementationRq}}%
{the \eacsl implementation provided by the \eacsl plug-in~\cite{eacsl-plugin}
- (version\eacslpluginversion) of the \framac framework~\cite{framac}.}%
+ of the \framac framework~\cite{framac}, version~\framacversion.}%
{E-ACSL.}
\eacsl is an acronym for ``Executable ANSI/ISO C
Specification Language''. It is an ``executable'' subset of
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index c94c46b0b8d30bb8c0608cf9ad9bbc968040ddf7..687af75e8b5f6310723ccc90ffc93e74533449ac 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.tex
@@ -4,6 +4,9 @@
\usepackage{comment}
+\newcommand{\framacversion}%
+ {\input{../../../../../VERSION}\unskip{} (\input{../../../../../VERSION_CODENAME}\unskip)}
+
\newcommand{\framac}{\textsc{Frama-C}\xspace}
\newcommand{\acsl}{\textsc{ACSL}\xspace}
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index c927ccde843f89b6c12efcde5f0045979fa252a2..00deb5cb4eba96c445cfd30b2e3c5b98efc209f3 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -4,7 +4,7 @@
\usepackage{ifthen}
\input{./macros_modern}
-\input{eacslversion.tex}
+\fcversion{\framacversion}
%Do not touch the following line. It is used in a Makefile hack to
%produce the ACSL documents for the ACSL working group.
%--\setboolean{PrintRemarks}{false}
@@ -40,7 +40,7 @@
\ifthenelse{\boolean{PrintImplementationRq}}%
{\subtitle{Version \eacsllangversion \space --
- Implementation in \framac \eacsl version \eacslpluginversion}}
+ Implementation in \framac \eacsl version \framacversion}}
{\subtitle{Version \eacsllangversion}}
\author{Julien Signoles}
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 92cad665e87cba877eb8a60433be29c78d0653f0..4404bea99f694e665a2272a02ec0f9699aa50794 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -11,7 +11,7 @@ MAIN=main
C_CODE=$(wildcard examples/*.[ci])
-DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
+DEPS_MODERN=biblio.bib macros.tex \
introduction.tex \
provides.tex \
limitations.tex \
@@ -33,7 +33,7 @@ $(MAIN).pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
*.haux *.hbbl *.htoc *.cb *.cm? *.bbl *.blg *.idx *.ind *.ilg \
- transf trans.ml pp.ml pp eacslversion.tex
+ transf trans.ml pp.ml pp
super-clean: clean
rm -f $(MAIN).pdf
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index dd28d602b2827650750e45e4e4f9c4e35b196509..7fa49640743606171b61e837095b9c1680f6d100 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -3,8 +3,7 @@
\framac~\cite{userman,fac15} is a modular analysis framework for the C
programming language which supports the ACSL specification
language~\cite{acsl}. This manual documents the \eacsl plug-in of \framac,
-version \eacslpluginversion. The \eacsl version you are using is indicated by the
-command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \eacsl
+version \framacversion. \eacsl
automatically translates an annotated C program into another program that fails
at runtime if an annotation is violated. If no annotation is violated, the
behavior of the new program is exactly the same as the one of the original
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index 212365b7a111053a983228da87649b6f6f991e29..0a1b91456d10c4458c3de5b447820efa8630f7be 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -4,6 +4,9 @@
\usepackage{comment}
+\newcommand{\framacversion}%
+ {\input{../../../../../VERSION}\unskip{} (\input{../../../../../VERSION_CODENAME}\unskip)}
+
\newcommand{\framac}{\textsc{Frama-C}\xspace}
\newcommand{\acsl}{\textsc{ACSL}\index{ACSL}\xspace}
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 64b3e1d0b6c5f03cb7be61548eee876fda08e517..2f566ffbadcbdd42d66fa7720195de78133201a1 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -6,7 +6,7 @@
\usepackage{imakeidx}
\input{macros}
-\input{eacslversion}
+\fcversion{\framacversion}
\makeindex
@@ -39,10 +39,9 @@
This is the user manual of the \framac plug-in
\eacsl\footnote{\url{https://frama-c.com/fc-plugins/e-acsl.html}}. The contents
-of this document correspond to its version \eacslpluginversion compatible with
-version \framacversion{} of \framac~\cite{userman,baudin21cacm}. The development of
-the \eacsl plug-in is still ongoing. Features described by this document may
-evolve in the future.
+of this document correspond to \framac~\cite{userman,baudin21cacm}'s version
+\framacversion{}. The development of the \eacsl plug-in is still ongoing.
+Features described by this document may evolve in the future.
\section*{Acknowledgements}
diff --git a/src/plugins/e-acsl/src/local_config.ml b/src/plugins/e-acsl/src/local_config.ml
deleted file mode 100644
index 8aa2ec00317afe937866044565417744ac5d5086..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/local_config.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-let version = "todo"
diff --git a/src/plugins/e-acsl/src/local_config.mli b/src/plugins/e-acsl/src/local_config.mli
deleted file mode 100644
index e978c54736d0396742b024e7508564418ca2660d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/local_config.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-val version: string
-
-(*
-Local Variables:
-compile-command: "make"
-End:
-*)
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 2b7310f6b8870751eba302ed36bf354d4ba1c922..2827052e1242dc45a719d48f2ae41b74758af43c 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -202,26 +202,6 @@ module Widening_output =
by case basis."
end)
-let () = Parameter_customize.set_group help
-module Version =
- False
- (struct
- let option_name = "-e-acsl-version"
- let help = "version of plug-in E-ACSL"
- end)
-
-let version () =
- if Version.get () then begin
- Log.print_on_output
- (fun fmt ->
- Format.fprintf
- fmt
- "Version of plug-in E-ACSL: %s@?"
- Local_config.version);
- raise Cmdline.Exit
- end
-let () = Cmdline.run_after_configuring_stage version
-
let parameter_states =
[ Valid.self;
Gmp_only.self;