Merge branch 'stable/phosphorus'

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

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)

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

src/plugins/e-acsl/doc/refman/eacslversion.tex

-\newcommand{\eacslversion}{0.8+dev}
+\newcommand{\eacslversion}{Phosphorus-20170501-beta1}

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}}}}

src/plugins/e-acsl/doc/userman/Makefile

 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

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 \\