From 6d3f12f50b33a1e10a57434ec3f6383bef5c0004 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 14 May 2020 10:50:59 +0200
Subject: [PATCH] [E-ACSL/Doc] refactor Makefiles of userman/refman
---
src/plugins/e-acsl/doc/Makefile.common | 57 ++++++++++++++
src/plugins/e-acsl/doc/refman/Makefile | 59 ++------------
.../e-acsl/doc/refman/changes_modern.tex | 2 +-
.../e-acsl/doc/refman/intro_modern.tex | 2 +-
src/plugins/e-acsl/doc/refman/main.tex | 10 +--
src/plugins/e-acsl/doc/userman/Makefile | 76 ++-----------------
src/plugins/e-acsl/doc/userman/changes.tex | 2 +-
.../e-acsl/doc/userman/introduction.tex | 2 +-
src/plugins/e-acsl/doc/userman/main.tex | 6 +-
9 files changed, 79 insertions(+), 137 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/Makefile.common
diff --git a/src/plugins/e-acsl/doc/Makefile.common b/src/plugins/e-acsl/doc/Makefile.common
new file mode 100644
index 00000000000..2fdcb5e52a3
--- /dev/null
+++ b/src/plugins/e-acsl/doc/Makefile.common
@@ -0,0 +1,57 @@
+# 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 $<
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 282220d94f0..43227e29838 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -1,10 +1,12 @@
+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 $<
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 70b99aa30c0..e532cf02b0f 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index 472b6cf40aa..8be890311bc 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\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
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 8f53a75d66c..4b6ad34ce83 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 8f6298dc37c..558ae875bed 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,9 +1,11 @@
+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
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index fa7302da6bc..c69ab6038c6 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/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
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 1f263c145d1..08956a9c61a 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/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
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index c70e1a72607..172397d5d40 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/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.
--
GitLab