[E-ACSL/Doc] refactor Makefiles of userman/refman

src/plugins/e-acsl/doc/Makefile.common

+# Common makefile for both refman and userman
+
+VERSION_FILE=$(wildcard ../../../../../VERSION)
+EACSL_VERSION=$(shell cat $(VERSION_FILE))
+FC_VERSION=$(shell cat $(VERSION_FILE))
+
+include $(EACSL_DIR)/doc/support/MakeLaTeXModern
+
+#################
+# Generic rules #
+#################
+
+eacslversion.tex: Makefile
+	rm -f $@
+	printf '\\newcommand{\\eacslpluginversion}{$(EACSL_VERSION)\\xspace}\n' > $@
+	printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
+	chmod a-w $@
+
+%.1: %.mp
+	mpost -interaction=batchmode $<
+
+%.mps: %.1
+	mv $< $@
+
+%.pp: %.tex pp
+	./pp -utf8 $< > $@
+
+%.pp: %.c pp
+	./pp -utf8 -c $< > $@
+
+%.tex: %.ctex pp
+	rm -f $@
+	./pp $< > $@
+	chmod a-w $@
+
+%.bnf: %.tex transf
+	rm -f $@
+	./transf $< > $@
+	chmod a-w $@
+
+%_modern.bnf: %.tex transf
+	rm -f $@
+	./transf -modern $< > $@
+	chmod a-w $@
+
+%.ml: %.mll
+	ocamllex $<
+
+%.pdf: %.tex
+	pdflatex $*
+	makeindex $*
+	bibtex $*
+	pdflatex $*
+	pdflatex $*
+
+%.cmo: %.ml
+	ocamlc -c $<

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

+default: all
+
+EACSL_DIR=../..
+include $(EACSL_DIR)/doc/Makefile.common
+
 ##########
 # Inputs #
 ##########
 
-VERSION_FILE=$(wildcard ../../../../../VERSION)
-EACSL_VERSION=$(shell cat $(VERSION_FILE))
-
 MAIN=main
 DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
 	intro_modern.tex speclang_modern.tex \
@@ -22,7 +24,6 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
 ##############
 
 .PHONY: all e-acsl default
-default: all
 e-acsl: e-acsl-implementation.pdf e-acsl.pdf
 all: e-acsl
 
@@ -42,7 +43,6 @@ e-acsl.tex: e-acsl-implementation.tex Makefile
 
 $(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
@@ -50,11 +50,6 @@ install: e-acsl-implementation.pdf e-acsl.pdf
 
 include $(EACSL_DIR)/doc/support/MakeLaTeXModern
 
-eacslversion.tex: Makefile $(VERSION_FILE)
-	rm -f $@
-	printf '\\newcommand{\\eacslversion}{$(EACSL_VERSION)}' > $@
-	chmod a-w $@
-
 .PHONY: clean
 clean:
 	rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
@@ -73,47 +68,3 @@ transf: transf.cmo transfmain.cmo
 	ocamlc -o $@ $^
 
 transfmain.cmo: transf.cmo
-
-#################
-# Generic rules #
-#################
-
-%.1: %.mp
-	mpost -interaction=batchmode $<
-
-%.mps: %.1
-	mv $< $@
-
-%.pp: %.tex pp
-	./pp -utf8 $< > $@
-
-%.pp: %.c pp
-	./pp -utf8 -c $< > $@
-
-%.tex: %.ctex pp
-	rm -f $@
-	./pp $< > $@
-	chmod a-w $@
-
-%.bnf: %.tex transf
-	rm -f $@
-	./transf $< > $@
-	chmod a-w $@
-
-%_modern.bnf: %.tex transf
-	rm -f $@
-	./transf -modern $< > $@
-	chmod a-w $@
-
-%.ml: %.mll
-	ocamllex $<
-
-%.pdf: %.tex
-	pdflatex $*
-	makeindex $*
-	bibtex $*
-	pdflatex $*
-	pdflatex $*
-
-%.cmo: %.ml
-	ocamlc -c $<

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

@@ -124,7 +124,7 @@ in \lstinline|\\at|}
     {
 \section{Changes in \eacsl Implementation}
 
-\subsection*{Version \eacslversion}
+\subsection*{Version \eacslpluginversion}
 
 \begin{itemize}
 \item \changeinsection{reals}{support of rational numbers and operations}

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\eacslversion) of the \framac framework~\cite{framac}.}%
+  (version\eacslpluginversion) of the \framac framework~\cite{framac}.}%
 {E-ACSL.}
 \eacsl is an acronym for ``Executable ANSI/ISO C
 Specification Language''. It is an ``executable'' subset of

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

@@ -24,8 +24,8 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.14\xspace}
-\newcommand{\version}{\acslversion\xspace}
+\newcommand{\eacsllangversion}{1.14\xspace}
+\newcommand{\version}{\eacsllangversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
 \renewcommand{\topfraction}{0.99}
@@ -36,9 +36,9 @@
 \hbadness=10000
 
 \ifthenelse{\boolean{PrintImplementationRq}}%
-  {\coverpage{\vbox{\mbox{E-ACSL Version \version}\\[5mm]
+  {\coverpage{\vbox{\mbox{E-ACSL Version \eacsllangversion}\\[5mm]
 \mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
-\mbox{\huge{version \eacslversion{}}}}}}%
+\mbox{\huge{version \eacslpluginversion{}}}}}}%
   {\coverpage{\vbox{\mbox{E-ACSL}\\[2mm]\vbox{\mbox{\huge{Executable ANSI/ISO C
           Specification Language}}}\\[2mm]
         \mbox{Version \version}}}}
@@ -48,7 +48,7 @@
 \vfill
 \title{E-ACSL\\[5mm]\huge{Executable ANSI/ISO C Specification Language}}%
 {Version \version{}\ifthenelse{\boolean{PrintImplementationRq}}%
-{~--~Frama-C plug-in E-ACSL version \eacslversion}{}}
+{~--~Frama-C plug-in E-ACSL version \eacslpluginversion}{}}
 
 \author{Julien Signoles}
 

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

+default: main.pdf
+
+EACSL_DIR=../..
+include $(EACSL_DIR)/doc/Makefile.common
+
 MAIN=main
 
 C_CODE=$(wildcard examples/*.[ci])
-VERSION_FILE=../../../../../VERSION
-FC_VERSION=$(shell cat $(VERSION_FILE))
-EACSL_VERSION= $(shell cat $(VERSION_FILE))
 
 DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
 	introduction.tex \
@@ -17,75 +19,7 @@ default: main.pdf
 
 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
-
-include $(EACSL_DIR)/doc/support/MakeLaTeXModern
-
-eacslversion.tex: Makefile
-	rm -f $@
-	printf '\\newcommand{\\eacslversion}{$(EACSL_VERSION)\\xspace}\n' > $@
-	printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
-	chmod a-w $@
-
-%.1: %.mp
-	mpost -interaction=batchmode $<
-
-%.mps: %.1
-	mv $< $@
-
-%.pp: %.tex pp
-	./pp -utf8 $< > $@
-
-%.pp: %.c pp
-	./pp -utf8 -c $< > $@
-
-%.tex: %.ctex pp
-	rm -f $@
-	./pp $< > $@
-	chmod a-w $@
-
-%.bnf: %.tex transf
-	rm -f $@
-	./transf $< > $@
-	chmod a-w $@
-
-%_modern.bnf: %.tex transf
-	rm -f $@
-	./transf -modern $< > $@
-	chmod a-w $@
-
-%.ml: %.mll
-	ocamllex $<
-
-%.pdf: %.tex
-	pdflatex $*
-	makeindex $*
-	bibtex $*
-	pdflatex $*
-	pdflatex $*
-
-%.cmo: %.ml
-	ocamlc -c $<
-
-pp: pp.ml
-	ocamlopt -o $@ str.cmxa $^
-
-transf: transf.cmo transfmain.cmo
-	ocamlc -o $@ $^
-
-transfmain.cmo: transf.cmo
-
-.PHONY: clean
-
-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
-	rm -f eacslversion.tex

src/plugins/e-acsl/doc/userman/changes.tex

@@ -3,7 +3,7 @@
 This chapter summarizes the changes in this documentation between each \eacsl
 release. First we list changes of the last release.
 
-\section*{E-ACSL \eacslversion}
+\section*{E-ACSL \eacslpluginversion}
 
 \begin{itemize}
 \item \textbf{Runtime Monitor Behavior}: Document global variable

src/plugins/e-acsl/doc/userman/introduction.tex

@@ -3,7 +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 \eacslversion. The \eacsl version you are using is indicated by the
+version \eacslpluginversion. The \eacsl version you are using is indicated by the
 command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \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

src/plugins/e-acsl/doc/userman/main.tex

@@ -17,8 +17,8 @@
 \includegraphics[height=14mm]{cealistlogo.jpg}
 \end{flushleft}
 \vfill
-\title{\eacsl Plug-in}{Release \eacslversion
- \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{%
+\title{\eacsl Plug-in}{Release \eacslpluginversion
+ \ifthenelse{\equal{\eacslpluginversion}{\fcversion}}{}{%
    \\[1em] compatible with \framac \fcversion}}
 \author{Julien Signoles and Kostyantyn Vorobyov}
 \begin{center}
@@ -42,7 +42,7 @@ CEA LIST\\ Software Reliability \& Security Laboratory
 
 This is the user manual of the \framac plug-in
 \eacsl\footnote{\url{https://frama-c.com/eacsl.html}}. The contents of this
-document correspond to its version \eacslversion compatible with
+document correspond to its version \eacslpluginversion compatible with
 \fcversion version of \framac~\cite{userman,fac15}.  The development of
 the \eacsl plug-in is still ongoing.  Features described by this document may
 evolve in the future.