[doc] New Frama-C manual theme

.gitignore

@@ -82,7 +82,6 @@ _build
 /doc/*/*.fls
 /doc/*/*.fdb_latexmk
 /doc/*/*.synctex.gz
-/doc/*/frama-c-affiliation.tex
 
 /doc/acsl/
 

doc/MakeLaTeXModern

 FRAMAC_DOC_ROOT_DIR?=..
-FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf frama-c-affiliation.tex eu-flag.jpg anr-logo.png
+FRAMAC_MODERN=frama-c-book.cls fc-macros.tex eu-flag.jpg anr-logo.png logos
 
 frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
 	@rm -f $@
@@ -7,38 +7,26 @@ frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
 	@chmod a-w $@
 	@echo "import $<"
 
-frama-c-cover.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-cover.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-right.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-right.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-left.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-left.pdf
+eu-flag.jpg: $(FRAMAC_DOC_ROOT_DIR)/eu-flag.jpg
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-frama-c-affiliation.tex: $(FRAMAC_DOC_ROOT_DIR)/frama-c-affiliation.tex
+anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-eu-flag.jpg: $(FRAMAC_DOC_ROOT_DIR)/eu-flag.jpg
+fc-macros.tex: $(FRAMAC_DOC_ROOT_DIR)/fc-macros.tex
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png
+logos: $(FRAMAC_DOC_ROOT_DIR)/logos
 	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
+	@ln -s $< $@
+	@chmod a-w $@/*
 	@echo "import $<"

doc/developer/.gitignore

@@ -2,10 +2,8 @@
 /developer.pdf
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/frama-c-affiliation.tex
+/fc-macros.tex
+/logos
 /hello_world/
 /tutorial/viewcfg/generated/
 /examples/generated/

doc/developer/Makefile.config

@@ -22,5 +22,5 @@
 
 MAKECONFIG_DIR=../../share
 include $(MAKECONFIG_DIR)/Makefile.common
-MAKEPDF ?= latexmk -pdf -quiet
+MAKEPDF ?= latexmk -pdf
 FRAMAC_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' ../../VERSION)

doc/developer/developer.tex

@@ -2,7 +2,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%MODERN \documentclass[a4paper,11pt,twoside,openright]{report}
-\documentclass[web,svgnames]{frama-c-book}
+\documentclass[svgnames]{frama-c-book}
 
 \usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim,spverbatim}
 \usepackage{amsmath}
@@ -15,7 +15,6 @@
 \usepackage{framed}
 \usepackage{makeidx}
 \usepackage{graphicx}
-\usepackage{enumerate}
 \usepackage{longtable}
 \usepackage{varwidth}
 \usepackage{tikz}
@@ -30,36 +29,48 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \input{./macros.sty}
-\input{./frama-c-affiliation.tex}
 \makeindex
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
-\sloppy
-\hbadness=10000
-
-\coverpage{Developer Manual}
-\begin{titlepage}
-\includegraphics[height=14mm]{../images/cealistlogo.jpg}
-\hfill~
-\vfill
-\title{Plug-in Development Guide}%
-{Release \framacversion}
+\title{Plug-in Development Guide}
 \author{Julien~Signoles with Thibaud~Antignac, Loïc~Correnson, Matthieu~Lemerre
 and Virgile~Prevosto}
-\begin{center}
-  \fcaffiliationen
-\end{center}
-\vfill
-\begin{flushleft}
-  \textcopyright 2009-{\the\year} CEA LIST
-\end{flushleft}
-\end{titlepage}
-
-%%Contents should open on right
-\cleardoublepage
-\markright{}
+
+\acknowledge{Michele Alberti}
+\acknowledge{Gergö Barany}
+\acknowledge{Patrick Baudin}
+\acknowledge{Allan Blanchard}
+\acknowledge{Richard Bonichon}
+\acknowledge{David B\"uhler}
+\acknowledge{Pascal Cuoq}
+\acknowledge{Zaynah Dargaye}
+\acknowledge{Basile Desloges}
+\acknowledge{Florent Garnier}
+\acknowledge{Pierre-Loïc Garoche}
+\acknowledge{Philippe Herrmann}
+\acknowledge{Boris Hollas}
+\acknowledge{Nikolaï Kosmatov}
+\acknowledge{Jean-Christophe Léchenet}
+\acknowledge{Romain Maliach-Auguste}
+\acknowledge{André Maroneze}
+\acknowledge{Benjamin Monate}
+\acknowledge{Yannick Moy}
+\acknowledge{Anne Pacalet}
+\acknowledge{Valentin Perrelle}
+\acknowledge{Armand Puccetti}
+\acknowledge{Muriel Roger}
+\acknowledge{Boris Yakobowski}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+
+\copyrightstarts{2009}
+
+\begin{document}
+
+\maketitle
 \tableofcontents
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -90,48 +101,26 @@ and Virgile~Prevosto}
 
 This is the documentation of the \framac
 implementation\footnote{\url{http://frama-c.com}} which aims at
-helping developers integrate new plug-ins inside this platform. It started as
-a deliverable of the task 2.3 of the ANR RNTL project
-CAT\footnote{\url{http://www.rntl.org/projet/resume2005/cat.htm}}.
+helping developers integrate new plug-ins inside this platform.
 
-The content of this document corresponds to the version \framacversion,
-released on \today,
-of \framac. However the development of \framac is still ongoing: features
+The content of this document corresponds to the version \framacversion,released on \today,of \framac. However the development of \framac is still ongoing: features
 described here may still evolve in the future.
 
 \section*{Acknowledgements}
 %\addcontentsline{toc}{chapter}{Acknowledgements}
 
-We gratefully thank all the people who contributed to this document:
-Michele Alberti,
-Gergö Barany,
-Patrick Baudin,
-Allan Blanchard,
-Richard Bonichon,
-David B\"uhler,
-Pascal Cuoq,
-Zaynah Dargaye,
-Basile Desloges,
-Florent Garnier,
-Pierre-Loïc Garoche,
-Philippe Herrmann,
-Boris Hollas,
-Nikolaï Kosmatov,
-Jean-Christophe Léchenet,
-Romain Maliach-Auguste,
-André Maroneze,
-Benjamin Monate,
-Yannick Moy,
-Anne Pacalet,
-Valentin Perrelle,
-Armand Puccetti,
-Muriel Roger and
-Boris Yakobowski.
+\insertpeople
 
 We also thank Johannes Kanig for his \langage{Mlpost}
 support\footnote{\url{http://mlpost.lri.fr}}, the tool formerly used for
 making figures of this document.
 
+\medskip
+
+\acknowledgeANR{
+  the French ANR projects CAT~(ANR-05-RNTL-00301)
+}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \include{introduction}

doc/developer/tutorial.tex

@@ -52,8 +52,8 @@ platform. This tutorial focuses on specific parts of this figure.
 \savebox{\designbox}{\begin{varwidth}{\textwidth}\centering Design\\(GUI extension point)\end{varwidth}}
 \newlength{\designheight}
 \setlength{\designheight}{\totalheightof{\usebox\designbox}}
-\newsavebox{\captionbox}\savebox{\captionbox}{\textbf{Caption:}}
-\newlength{\captionheight}\settototalheight{\captionheight}{\captionbox}
+\newsavebox{\capbox}\savebox{\capbox}{\textbf{Caption:}}
+\newlength{\captionheight}\settototalheight{\captionheight}{\capbox}
 \begin{tikzpicture}[remember picture,txt/.style={inner xsep=3pt}]
   \node[inner sep=0pt] (implem) {
     \tikztitleboxbig{Plug-in\\implementation}{darkgreen}{
@@ -113,7 +113,7 @@ platform. This tutorial focuses on specific parts of this figure.
    \draw[Latex-] ($(registration.west)+(-\padding,0)$) -- +(-\bigpadding,0);
 
    \node[anchor=south east,xshift=-\padding] at (registration.north west)
-   {\usebox{\captionbox}};
+   {\usebox{\capbox}};
 
    \newlength{\kernelwidth}
    \setlength{\kernelwidth}{\widthof{Dynamic}}%TODO:compute dynamically

doc/eva/.gitignore

 /anr-logo.png
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/frama-c-affiliation.tex
 /main.pdf
-
+/logos
+/fc-macros.tex

doc/eva/main.tex

-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 
 \usepackage{microtype}
 \usepackage{lmodern}
@@ -6,6 +6,8 @@
 \usepackage{calc}
 \usepackage{multirow}
 
+\input{fc-macros.tex}
+
 % Commandes pour mettre des ref dans l'index :
 \newcommand{\idb}[1]{\textbf{#1}}
 \newcommand{\indextxt}[1]{\index{#1}{\bf #1}}
@@ -23,52 +25,51 @@
 \definecolor{gris}{gray}{0.85}
 
 \makeatletter
-\newenvironment{important}%
-{\hspace{5pt plus \linewidth minus \marginparsep}%
- \begin{lrbox}{\@tempboxa}%
-   \begin{minipage}{\linewidth - 2\fboxsep}\itshape}
-{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
+\newenvironment{important}{\begin{colbox}{gris}}{\end{colbox}}
 \makeatother
 
 \newcommand{\framacversion}%
            {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
 \newcommand{\isoc}{\textsf{C99}}
 
-\newcommand{\Eva}{\textsf{Eva}}
-
-\input{./frama-c-affiliation.tex}
-
 \lstset{literate=%
 {∈}{{$\in$ }}1
 }
 
+\title{The \Eva{} plug-in}
+\author{David Bühler, Pascal Cuoq and Boris Yakobowski. \\
+With Matthieu Lemerre, André Maroneze,
+Valentin Perrelle and Virgile Prevosto}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+\copyrightstarts{2011}
+
 %==============================================================================
 \begin{document}
 
-\coverpage{Eva – The Evolved Value Analysis plug-in}
+\maketitle
+\tableofcontents
 
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{The \Eva{} plug-in}{\framacversion}
-\author{David Bühler, Pascal Cuoq and Boris Yakobowski. \\
-  With Matthieu Lemerre, André Maroneze,
-  Valentin Perrelle and Virgile Prevosto}
-\begin{tabular}{l}
-  \fcaffiliationen
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2011-\the\year{} CEA LIST
-
-  This work has been supported by the ANR project U3CAT
-  (ANR-08-SEGI-021-01).
-\end{flushleft}
-\end{titlepage}
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
 
-\tableofcontents
+This is the documentation of the \FramaC plug-in \Eva.
+
+The content of this document corresponds to the version \framacversion, released
+on \today, of \FramaC. However the development of \FramaC is still ongoing:
+features described here may still evolve in the future.
+
+\section*{Acknowledgements}
+%\addcontentsline{toc}{chapter}{Acknowledgements}
+
+\medskip
+
+\acknowledgeANR{
+the French ANR projects U3CAT~(08-SEGI-021-01)
+}
 
 \chapter{Introduction}\label{introduction}
 \vspace{2cm}
@@ -673,7 +674,7 @@ We can then Ctrl+click on the loop condition in the original source view
   can be defined via the menu {\em File - Preferences}.} centered on the loop, and
 then add the loop unroll annotation, as follows:
 
-\begin{lstlisting}
+\begin{lstlisting}[style=c]
   //@ loop unroll 4;
   for (i=0;i < WCNT; i++)
       {
@@ -2288,7 +2289,7 @@ developing a custom plug-in.
 
 \chapter{Graphical interface (GUI)}\label{gui}
 \vspace{2cm}
-\include{gui}
+\input{gui}
 
 \chapter{Limitations and specificities}\label{limitations_specificities}
 \vspace{2cm}

doc/fc-macros.tex

+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Date
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Useful for today's short date
+\def\shorttoday{\leavevmode\hbox{\the\year-\twodigits\month-\twodigits\day}}
+\def\twodigits#1{\ifnum#1<10 0\fi\the#1}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Indexed Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Frama-C plug-in names (e.g., \plugin{Eva})
+\newcommand{\plugin}[1]{\textsf{#1}\xspace}
+
+% Tools (e.g., \tool{Why3})
+\newcommand{\tool}[1]{\textsf{#1}\xspace}
+
+% Languages (e.g., \lang{ACSL}, \lang{C})
+\newcommand{\lang}[1]{\textsf{#1}\xspace}
+
+% Libraries (e.g., \library{Gmp})
+\newcommand{\library}[1]{\textsf{#1}\xspace}
+
+% Benchmarks (e.g, \benchmark{SpecCPU})
+\newcommand{\benchmark}[1]{\textsf{#1}\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frama-C Related Names
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\FramaC}{\tool{Frama-C}}
+\newcommand{\acsl}{\lang{ACSL}}
+\newcommand{\eacsllang}{\lang{E-ACSL}}
+
+% plug-ins
+\newcommand{\aorai}{\plugin{Aora\"i}}
+\newcommand{\cafe}{\plugin{CaFE}}
+\newcommand{\callgraph}{\plugin{Callgraph}}
+\newcommand{\constfold}{\plugin{Consfold}}
+\newcommand{\dive}{\plugin{Dive}}
+\newcommand{\dominators}{\plugin{Dominators}}
+\newcommand{\eacsl}{\plugin{E-ACSL}}
+\newcommand{\Eva}{\plugin{Eva}}
+\newcommand{\framaclang}{\plugin{Frama-Clang}}
+\newcommand{\from}{\plugin{From}}
+\newcommand{\GUI}{\plugin{GUI}}
+\newcommand{\impact}{\plugin{Impact}}
+\newcommand{\inout}{\plugin{InOut}}
+\newcommand{\instantiate}{\plugin{Instantiate}}
+\newcommand{\ltest}{\plugin{LTest}}
+\newcommand{\mdr}{\plugin{MdR}}
+\newcommand{\metacsl}{\plugin{MetAcsl}}
+\newcommand{\metrics}{\plugin{Metrics}}
+\newcommand{\nonterm}{\plugin{NonTerm}}
+\newcommand{\obfuscator}{\plugin{Obfuscator}}
+\newcommand{\occurrence}{\plugin{Occurrence}}
+\newcommand{\pathcrawler}{\plugin{PathCrawler}}
+\newcommand{\pdg}{\plugin{Pdg}}
+\newcommand{\pilat}{\plugin{Pilat}}
+\newcommand{\postdominators}{\plugin{Postdominators}}
+\newcommand{\printinterface}{\plugin{PrintInterface}}
+\newcommand{\reduction}{\plugin{Reduction}}
+\newcommand{\report}{\plugin{Report}}
+\newcommand{\rpp}{\plugin{RPP}}
+\newcommand{\rte}{\plugin{Rte}}
+\newcommand{\scope}{\plugin{Scope}}
+\newcommand{\secureflow}{\plugin{SecureFlow}}
+\newcommand{\securityslicing}{\plugin{SecuritySlicing}}
+\newcommand{\server}{\plugin{Server}}
+\newcommand{\slicing}{\plugin{Slicing}}
+\newcommand{\sparecode}{\plugin{SpareCode}}
+\newcommand{\stady}{\plugin{StaDy}}
+\newcommand{\studia}{\plugin{Studia}}
+\newcommand{\users}{\plugin{Users}}
+\newcommand{\variadic}{\plugin{Variadic}}
+\newcommand{\Wp}{\plugin{WP}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Standard Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Some programming languages
+\newcommand{\ada}{\lang{Ada}}
+\newcommand{\awk}{\lang{Awk}}
+\newcommand{\C}{\lang{C}}
+\newcommand{\coq}{\lang{Coq}}
+\newcommand{\Cpp}{\lang{C++}}
+\newcommand{\csharp}{\lang{C\#}}
+\newcommand{\dafny}{\lang{Dafny}}
+\newcommand{\dotnet}{\lang{.NET}}
+\newcommand{\eiffel}{\lang{Eiffel}}
+\newcommand{\fortran}{\lang{Fortran}}
+\newcommand{\isabelle}{\lang{Isabelle}}
+\newcommand{\java}{\lang{Java}}
+\newcommand{\javacard}{\lang{JavaCard}}
+\newcommand{\K}{\ensuremath{\mathbb{K}}}
+\newcommand{\ocaml}{\lang{OCaml}}
+\newcommand{\php}{\lang{PHP}}
+\newcommand{\python}{\lang{Python}}
+\newcommand{\smalltalk}{\lang{Smalltalk}}
+\newcommand{\spark}{\lang{Spark2014}}
+\newcommand{\vbnet}{\lang{VB.NET}}
+
+% Some modeling languages
+\newcommand{\lustre}{\lang{Lustre}}
+\newcommand{\scade}{\lang{Scade}}
+\newcommand{\simulink}{\lang{Simulink}}
+
+% Some specification languages
+\newcommand{\codecontract}{\lang{Code Contract}}
+\newcommand{\ltl}{\lang{LTL}}
+\newcommand{\jml}{\lang{JML}}
+\newcommand{\specsharp}{\lang{Spec\#}}
+\newcommand{\vcc}{\lang{VCC}}
+
+% Some libraries
+\newcommand{\cil}{\library{Cil}}
+\newcommand{\gtk}{\library{Gtk2}}
+\newcommand{\gtkt}{\library{Gtk3}}
+\newcommand{\gmp}{\library{Gmp}}
+\newcommand{\lablgtk}{\library{LablGtk2}}
+\newcommand{\lablgtkt}{\library{LablGtk3}}
+\newcommand{\libc}{\library{libc}}
+\newcommand{\libtomcrypt}{\library{LibTomCrypt}}
+
+% Some analysis and verification tools
+\newcommand{\addresssanitizer}{\tool{AddressSanitizer}}
+\newcommand{\aiT}{\tool{aiT}}
+\newcommand{\astree}{\tool{Astr\'ee}}
+\newcommand{\caduceus}{\tool{Caduceus}}
+\newcommand{\drmemory}{\tool{Dr.~Memory}}
+\newcommand{\insurepp}{\tool{Insure++}}
+\newcommand{\memcheck}{\tool{MemCheck}}
+\newcommand{\memorysanitizer}{\tool{MemorySanitizer}}
+\newcommand{\memsanitizer}{\tool{MemorySanitizer}}
+\newcommand{\openjml}{\tool{OpenJML}}
+\newcommand{\polyspace}{\tool{PolySpace}}
+\newcommand{\purify}{\tool{Purify}}
+\newcommand{\rvmatch}{\tool{RV-Match}}
+\newcommand{\stackanalyzer}{\tool{Stackanalyzer}}
+\newcommand{\threadsanitizer}{\tool{ThreadSanitizer}}
+\newcommand{\undefsanitizer}{\tool{UndefinedBehaviorSanitizer}}
+\newcommand{\valgrind}{\tool{Valgrind}}
+\newcommand{\verasco}{\tool{Verasco}}
+\newcommand{\why}{\tool{Why}}
+\newcommand{\whyt}{\tool{Why3}}
+
+% Some other tools
+\newcommand{\altergo}{\tool{Alt-Ergo}}
+\newcommand{\clang}{\tool{Clang}}
+\newcommand{\clousot}{\tool{Clousot}}
+\newcommand{\compcert}{\tool{CompCert}}
+\newcommand{\gcc}{\tool{Gcc}}
+\newcommand{\gdb}{\tool{gdb}}
+\newcommand{\git}{\tool{Git}}
+\newcommand{\llvm}{\tool{LLVM}}
+\newcommand{\opam}{\tool{opam}}