diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 6e2bb962d2c1b007b99c524d08c6cc580be0fbdd..aab26d649b8266865f15ee8a9a93d983d284cb2d 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -18,6 +18,7 @@
/share/e-acsl/*.cm*
/share/e-acsl/*.annot
/share/e-acsl/*_DEP
+/doc/manuals
/doc/code
/doc/refman/*.out
/doc/refman/*.bbl
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index a5cb7784ea01987e9d45e20466d54ad6168de37e..efb479fcfd6537082b1c246d436848751f9f5847 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -82,13 +82,15 @@ PLUGIN_CMO:= local_config \
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
-# Suppress a spurious warning in ocaml 4.04.0
-mmodel_analysis.cmo mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
-mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
# 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 in ocaml 4.04.0
+$(EACSL_PLUGIN_DIR)/mmodel_analysis.cmo \
+$(EACSL_PLUGIN_DIR)/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
+
###############
# Local Flags #
###############
@@ -350,6 +352,8 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
# Install #
###########
+MANUALS=$(wildcard $(E_ACSL_DIR)/doc/manuals/*.pdf)
+
install::
$(PRINT_INSTALL) E-ACSL share files
$(MKDIR) $(FRAMAC_DATADIR)/e-acsl
@@ -365,14 +369,11 @@ install::
$(FRAMAC_DATADIR)/e-acsl/glibc
# manuals are not present in standard distribution.
# Don't fail because of that.
- if test -f $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf; then \
- $(PRINT_INSTALL) E-ACSL manuals \
- $(MKDIR) $(FRAMAC_DATADIR)/manuals \
- $(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
- $(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
- $(E_ACSL_DIR)/doc/manuals/e-acsl-manual.pdf \
- $(FRAMAC_DATADIR)/manuals; \
- fi
+ifneq ("$(MANUALS)","")
+ $(PRINT_INSTALL) E-ACSL manuals
+ $(MKDIR) $(FRAMAC_DATADIR)/manuals
+ $(CP) $(MANUALS) $(FRAMAC_DATADIR)/manuals;
+endif
$(PRINT_INSTALL) E-ACSL libraries
$(MKDIR) $(LIBDIR)
$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index ae75562668d1c354cc0d875380f61c9be26ce459..2746df6846d7f39df49c85c7cf5c3f277a3e8f5b 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -2,7 +2,11 @@
# Inputs #
##########
+# If in internal mode, use Frama-C's VERSION
+VERSION_FILE=$(wildcard ../../../../../VERSION)
+ifeq ("$(VERSION_FILE)","")
VERSION_FILE=../../VERSION
+endif
EACSL_VERSION=$(shell cat $(VERSION_FILE))
MAIN=main
@@ -22,8 +26,8 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
##############
.PHONY: all e-acsl default
-default: e-acsl.pdf
-e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
+default: all
+e-acsl: e-acsl-implementation.pdf e-acsl.pdf
all: e-acsl
e-acsl-implementation.pdf: $(DEPS_MODERN)
@@ -45,6 +49,7 @@ $(MAIN).pdf: $(DEPS_MODERN)
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install: e-acsl-implementation.pdf e-acsl.pdf
+ mkdir -p $(EACSL_DIR)/doc/manuals
cp -f $^ $(EACSL_DIR)/doc/manuals
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index b931906930cb3d7f7c1ddf04b78133779b649459..a59b2e01486e1a8e226388e0b6735e6b3593c304 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.8+dev}
+\newcommand{\eacslversion}{Phosphorus-20170501-beta1}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index fad5ef6f5c8b84f453fc34b4149545d2704301d9..78a65233dce068133242e77f08e5ce9c6ef61a87 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -37,8 +37,8 @@
\ifthenelse{\boolean{PrintImplementationRq}}%
{\coverpage{\vbox{\mbox{E-ACSL Version \version}\\[5mm]
-\mbox{\huge{Implementation in Frama-C plug-in E-ACSL
- version \eacslversion{}}}}}}%
+\mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
+\mbox{\huge{version \eacslversion{}}}}}}%
{\coverpage{\vbox{\mbox{E-ACSL}\\[2mm]\vbox{\mbox{\huge{Executable ANSI/ISO C
Specification Language}}}\\[2mm]
\mbox{Version \version}}}}
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 2855dee8cda9a43228c879ec6d75e63de727cb39..b5e7003817f2aff3791161c247d7f5bce39788fe 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,8 +1,14 @@
MAIN=main
C_CODE=$(wildcard examples/*.[ci])
+VERSION_FILE=../../../../../VERSION
+ifeq ("$(wildcard $(VERSION_FILE))", "")
VERSION_FILE=../../VERSION
FC_VERSION= Silicon
+else
+#internal mode
+FC_VERSION=$(shell cat $(VERSION_FILE))
+endif
EACSL_VERSION= $(shell cat $(VERSION_FILE))
DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
@@ -20,6 +26,7 @@ main.pdf: $(DEPS_MODERN)
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install:
+ mkdir -p $(EACSL_DIR)/doc/manuals/
cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
# cp -f main.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 11d07531f416aa0e1e03ef20666dbf8acc37f458..f87476d001dcf09e39bbf001a411837bade7db51 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -17,8 +17,9 @@
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
-\title{\eacsl Plug-in}{Release \eacslversion compatible
- with \framac \fcversion}
+\title{\eacsl Plug-in}{Release \eacslversion
+ \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{
+ compatible with \framac \fcversion}}
\author{Julien Signoles and Kostyantyn Vorobyov}
\begin{tabular}{l}
CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\